From 1885451c89bd1fd117fa473347b75ac797f2a92a Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Mon, 21 Feb 2011 06:14:33 +0000 Subject: [PATCH] Bugfix. r1152 was broken. It got the widths wrong. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1154 e59a4935-1847-0410-ae03-e826735625c1 --- src/simplifier/simplifier.cpp | 15 +++++++++++---- 1 file changed, 11 insertions(+), 4 deletions(-) diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp index 7cb493e..bfa21cd 100644 --- a/src/simplifier/simplifier.cpp +++ b/src/simplifier/simplifier.cpp @@ -964,7 +964,9 @@ namespace BEEV ASTNode lhs = nf->CreateTerm(BVEXTRACT,newWidth, in1,_bm->CreateBVConst(32,newWidth-1) ,zero); ASTNode rhs = nf->CreateTerm(BVEXTRACT,newWidth, in2,_bm->CreateBVConst(32,newWidth-1) ,zero); - return nf->CreateNode(EQ, lhs,rhs); + ASTNode r= nf->CreateNode(EQ, lhs,rhs); + assert(BVTypeCheck(r)); + return r; } // If both the children are concats split them apart. @@ -983,10 +985,15 @@ namespace BEEV ASTNode zero = _bm->CreateZeroConst(32); // split the constant. - ASTNode top = nf->CreateTerm(BVEXTRACT,bottomW, in1,_bm->CreateBVConst(32,width-1) ,_bm->CreateBVConst(32,bottomW)); - ASTNode bottom = nf->CreateTerm(BVEXTRACT,width-bottomW, in1,_bm->CreateBVConst(32,bottomW-1) ,zero); + ASTNode top = nf->CreateTerm(BVEXTRACT,width-bottomW, in1,_bm->CreateBVConst(32,width-1) ,_bm->CreateBVConst(32,bottomW)); + ASTNode bottom = nf->CreateTerm(BVEXTRACT,bottomW, in1,_bm->CreateBVConst(32,bottomW-1) ,zero); + assert(BVTypeCheck(top)); + assert(BVTypeCheck(bottom)); + + ASTNode r = nf->CreateNode(AND, nf->CreateNode(EQ, top, in2[0]), nf->CreateNode(EQ, bottom, in2[1])); + + return r; - return nf->CreateNode(AND, nf->CreateNode(EQ, top, in2[0]), nf->CreateNode(EQ, bottom, in2[1])); } -- 2.47.3