Bugfix. Fix rotate_left and rotate_right to take the modulus of the shift amount...

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 ffe850ab69879055a718a1c130b8d7e2fcb75e68..a94bd6c74859a8c1500838a7ee60517f3f323d38 100644 (file)
--- 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;
 }