From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Mon, 21 Feb 2011 06:14:33 +0000 (+0000)
Subject: Bugfix. r1152 was broken. It got the widths wrong.
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=1885451c89bd1fd117fa473347b75ac797f2a92a;p=francis%2Fstp.git

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
---

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]));
     }