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 7cb493ef2937ce8fad375f2f368c5fc91a403ab2..bfa21cdf9b34c4ed852fce0decab2b0ce4dec9e3 100644 (file)
--- 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]));
     }