From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Wed, 11 May 2011 03:34:42 +0000 (+0000)
Subject: Bugfix. Arithmetic shifts by constants that didn't fit in 32-bits would cause an... 
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=e6b57f37722186d71e493fdce5ca54b68d48e4cb;p=francis%2Fstp.git

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

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 f3f06a5..0a648df 100644
--- 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();
   }