Bugfix. Arithmetic shifts by constants that didn't fit in 32-bits would cause an...

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1323 e59a4935-1847-0410-ae03-e826735625c1

diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp
index f3f06a5b6b99bf5c9f0ff514a5cd21cff3cb59b5..0a648dfad0770a2e4c15bed501425876080a5e7e 100644 (file)
--- a/src/simplifier/simplifier.cpp
+++ b/src/simplifier/simplifier.cpp
@@ -1739,13 +1739,20 @@ namespace BEEV
 
     assert(b.isConstant());
     assert(k == BVSRSHIFT);
-    const unsigned int shift = b.GetUnsignedConst();
 
-    if (CONSTANTBV::Set_Max(b.GetBVConst()) > 1 + log2(width) || (shift >= width))
+    if (CONSTANTBV::Set_Max(b.GetBVConst()) > 1 + log2(width))
       {
         ASTNode top = bm.CreateBVConst(32,width-1);
         return nf->CreateTerm(BVSX, width, nf->CreateTerm(BVEXTRACT,1, children[0], top,top ), bm.CreateBVConst(32,width));
       }
+    else
+    {
+        if  (b.GetUnsignedConst() >= width)
+          {
+            ASTNode top = bm.CreateBVConst(32,width-1);
+            return nf->CreateTerm(BVSX, width, nf->CreateTerm(BVEXTRACT,1, children[0], top,top ), bm.CreateBVConst(32,width));
+          }
+    }
 
     return ASTNode();
   }