From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Fri, 18 Jun 2010 05:46:17 +0000 (+0000)
Subject: Bugfix. Fix rotate_left and rotate_right to take the modulus of the shift amount... 
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=5a8e58a6c29246e91af2dd45de4c4785d122e0fb;p=francis%2Fstp.git

Bugfix. Fix rotate_left and rotate_right to take the modulus of the shift amount. I'd misinterpreted the specification.





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

diff --git a/src/parser/smtlib2.y b/src/parser/smtlib2.y
index ffe850a..a94bd6c 100644
--- a/src/parser/smtlib2.y
+++ b/src/parser/smtlib2.y
@@ -861,12 +861,12 @@ TERMID_TOK
 {
   ASTNode *n;
   unsigned width = $6->GetValueWidth();
-  unsigned rotate = $4;
+  unsigned rotate = $4 % width;
   if (0 == rotate)
     {
       n = $6;
     }
-  else if (rotate < width)
+  else 
     {
       ASTNode high = parserInterface->CreateBVConst(32,width-1);
       ASTNode zero = parserInterface->CreateBVConst(32,0);
@@ -878,11 +878,6 @@ TERMID_TOK
       n =  new ASTNode(parserInterface->nf->CreateTerm(BVCONCAT,width,bottom,top));
       delete $6;
     }
-  else
-    {
-      n = NULL; // remove gcc warning.
-      yyerror("Rotate must be strictly less than the width.");
-    }
       
   $$ = n;
 }
@@ -890,12 +885,12 @@ TERMID_TOK
 {
   ASTNode *n;
   unsigned width = $6->GetValueWidth();
-  unsigned rotate = $4;
+  unsigned rotate = $4 % width;
   if (0 == rotate)
     {
       n = $6;
     }
-  else if (rotate < width)
+  else 
     {
       ASTNode high = parserInterface->CreateBVConst(32,width-1);
       ASTNode zero = parserInterface->CreateBVConst(32,0);
@@ -907,11 +902,6 @@ TERMID_TOK
       n =  new ASTNode(parserInterface->nf->CreateTerm(BVCONCAT,width,bottom,top));
       delete $6;
     }
-  else
-    {
-      n = NULL; // remove gcc warning.
-      yyerror("Rotate must be strictly less than the width.");
-    }
       
   $$ = n;
 }