When using the SMT parser (x % 0) and (x /0) both evaluate to 1. This isn't in keepin...

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

diff --git a/src/AST/AST.cpp b/src/AST/AST.cpp
index fa975c9b26adf32992eed15ef3c4cac28668a020..04651b120b86f314215136cec74049d260b0ecee 100644 (file)
--- a/src/AST/AST.cpp
+++ b/src/AST/AST.cpp
@@ -55,6 +55,9 @@ bool smtlib_parser_flag = false;
 //print the input back
 bool print_STPinput_back_flag = false;
 
+// If enabled. division, mod and remainder by zero will evaluate to 1.
+bool division_by_zero_returns_one = false;
+
 enum inputStatus input_status = NOT_DECLARED;
 
 // Used only in smtlib lexer/parser

diff --git a/src/AST/ASTUtil.h b/src/AST/ASTUtil.h
index 8e0cf13cb315ac17ddfa4412f17c123ea2a20ef5..e0c8827ea162b102bdfac920a0b6c5191cfee986 100644 (file)
--- a/src/AST/ASTUtil.h
+++ b/src/AST/ASTUtil.h
@@ -25,7 +25,7 @@
 
 #include <cstring>
 
-using namespace std; 
+using namespace std;
 namespace BEEV {
 #ifdef EXT_HASH_MAP
   using namespace __gnu_cxx;
@@ -61,7 +61,7 @@ namespace BEEV {
   extern bool print_output_flag;
   //print the variable order chosen by the sat solver while it is
   //solving.
-  extern bool print_sat_varorder_flag; 
+  extern bool print_sat_varorder_flag;
   //turn on word level bitvector solver
   extern bool wordlevel_solve_flag;
   //XOR flattening optimizations.
@@ -73,6 +73,8 @@ namespace BEEV {
   //Flag to switch on the smtlib parser
   extern bool smtlib_parser_flag;
 
+  extern bool division_by_zero_returns_one;
+
   enum inputStatus
     {
          NOT_DECLARED =0, // Not included in the input file / stream
@@ -107,10 +109,10 @@ namespace BEEV {
 
   // Table for storing function count stats.
 #ifdef TR1_UNORDERED_MAP
-  typedef tr1::unordered_map<const char*,int, 
+  typedef tr1::unordered_map<const char*,int,
                              tr1::hash<const char *>,eqstr> function_counters;
 #else
-  typedef hash_map<const char*,int, 
+  typedef hash_map<const char*,int,
                   hash<char *>,eqstr> function_counters;
 #endif
 
@@ -118,7 +120,7 @@ namespace BEEV {
 
   //global function which accepts an integer and looks up the
   //corresponding ASTNode and prints a char* of that ASTNode
-  void Convert_MINISATVar_To_ASTNode_Print(int minisat_var, 
+  void Convert_MINISATVar_To_ASTNode_Print(int minisat_var,
                                           int decision, int polarity=0);
 }; // end namespace.
 #endif

diff --git a/src/AST/Transform.cpp b/src/AST/Transform.cpp
index e8f6accfdffa3aa36fecd376c11b2de6bcdf0ead..52a1c8bc939912b045071cb06c6f46be3ee80962 100644 (file)
--- a/src/AST/Transform.cpp
+++ b/src/AST/Transform.cpp
@@ -40,7 +40,7 @@ ASTNode BeevMgr::TranslateSignedDivModRem(const ASTNode& in)
 
                //Take absolute value.
                ASTNode pos_dividend = CreateTerm(ITE, len, cond_dividend, CreateTerm(BVUMINUS, len, dividend), dividend);
-               ASTNode pos_divisor =  CreateTerm(ITE, len, cond_divisor,  CreateTerm(BVUMINUS, len, divisor), divisor);
+               ASTNode pos_divisor = CreateTerm(ITE, len, cond_divisor, CreateTerm(BVUMINUS, len, divisor), divisor);
 
                //create the modulus term
                ASTNode modnode = CreateTerm(BVMOD, len, pos_dividend, pos_divisor);
@@ -69,12 +69,12 @@ ASTNode BeevMgr::TranslateSignedDivModRem(const ASTNode& in)
 
                //Take absolute value.
                ASTNode pos_dividend = CreateTerm(ITE, len, cond_dividend, CreateTerm(BVUMINUS, len, dividend), dividend);
-               ASTNode pos_divisor =  CreateTerm(ITE, len, cond_divisor,  CreateTerm(BVUMINUS, len, divisor), divisor);
+               ASTNode pos_divisor = CreateTerm(ITE, len, cond_divisor, CreateTerm(BVUMINUS, len, divisor), divisor);
 
                ASTNode urem_node = CreateTerm(BVMOD, len, pos_dividend, pos_divisor);
 
                // If the dividend is <0, then we negate the whole thing.
-               ASTNode rev_node =  CreateTerm(ITE, len, cond_dividend, CreateTerm(BVUMINUS, len, urem_node), urem_node);
+               ASTNode rev_node = CreateTerm(ITE, len, cond_dividend, CreateTerm(BVUMINUS, len, urem_node), urem_node);
 
                // if It's XOR <0 then add t (not its absolute value).
                ASTNode xor_node = CreateNode(XOR, cond_dividend, cond_divisor);
@@ -101,7 +101,7 @@ ASTNode BeevMgr::TranslateSignedDivModRem(const ASTNode& in)
 
                //Take absolute value.
                ASTNode pos_dividend = CreateTerm(ITE, len, cond_dividend, CreateTerm(BVUMINUS, len, dividend), dividend);
-               ASTNode pos_divisor =  CreateTerm(ITE, len, cond_divisor,  CreateTerm(BVUMINUS, len, divisor), divisor);
+               ASTNode pos_divisor = CreateTerm(ITE, len, cond_divisor, CreateTerm(BVUMINUS, len, divisor), divisor);
 
                ASTNode divnode = CreateTerm(BVDIV, len, pos_dividend, pos_divisor);
 
@@ -305,14 +305,16 @@ ASTNode BeevMgr::TransformTerm(const ASTNode& inputterm)
                                        result = TranslateSignedDivModRem(result);
                                }
 
-                               ////// Temporary hack so we don't get killed on the Spear benchmarks in SMTCOMP-2009
-                               // This is a difficult rule to introduce in other places because it's recursive. i.e.
-                               // result is imbedded unchanged inside the result. It's not
+                               if (division_by_zero_returns_one)
+                               {
+                                       // This is a difficult rule to introduce in other places because it's recursive. i.e.
+                                       // result is embedded unchanged inside the result.
 
-                               unsigned inputValueWidth = result.GetValueWidth();
-                               ASTNode zero = CreateZeroConst(inputValueWidth);
-                               ASTNode one = CreateOneConst(inputValueWidth);
-                               result = CreateTerm(ITE, inputValueWidth, CreateNode(EQ, zero, bottom), one, result);
+                                       unsigned inputValueWidth = result.GetValueWidth();
+                                       ASTNode zero = CreateZeroConst(inputValueWidth);
+                                       ASTNode one = CreateOneConst(inputValueWidth);
+                                       result = CreateTerm(ITE, inputValueWidth, CreateNode(EQ, zero, bottom), one, result);
+                               }
                        }
                }
                        ////////////////////////////////////////////////////////////////////////////////////

diff --git a/src/bitvec/consteval.cpp b/src/bitvec/consteval.cpp
index daa42724c45223997fc983ca997021d6dd241076..12860c9a200d65b0fa57c3790bbf2db69d134af1 100644 (file)
--- a/src/bitvec/consteval.cpp
+++ b/src/bitvec/consteval.cpp
@@ -143,9 +143,9 @@ ASTNode BeevMgr::BVConstEvaluator(const ASTNode& t)
                        {
                                // signed shift, and the number was originally negative.
                                // Shift may be larger than the inputwidth.
-                               for (unsigned int i =0; i < min(shift,inputwidth);i++)
+                               for (unsigned int i = 0; i < min(shift, inputwidth); i++)
                                {
-                                       CONSTANTBV::BitVector_Bit_On(output,(inputwidth-1 -i));
+                                       CONSTANTBV::BitVector_Bit_On(output, (inputwidth - 1 - i));
                                }
                                assert(CONSTANTBV::BitVector_Sign(output) == -1); //must be negative.
                        }
@@ -261,26 +261,33 @@ ASTNode BeevMgr::BVConstEvaluator(const ASTNode& t)
                        CBV quotient = CONSTANTBV::BitVector_Create(inputwidth, true);
                        CBV remainder = CONSTANTBV::BitVector_Create(inputwidth, true);
 
-                       CONSTANTBV::ErrCode e = CONSTANTBV::BitVector_Divide(quotient, tmp0, tmp1, remainder);
-
-                       if (e != 0)
-                       {
-                               cerr << "WARNING" << endl;
-                               FatalError((const char*) CONSTANTBV::BitVector_Error(e));
-                       }
-
-                       if (SBVDIV == k)
+                       if (division_by_zero_returns_one && CONSTANTBV::BitVector_is_empty(tmp1))
                        {
-                               OutputNode = CreateBVConst(quotient, outputwidth);
-                               CONSTANTBV::BitVector_Destroy(remainder);
+                               // Expecting a division by zero. Just return one.
+                               OutputNode = CreateOneConst(outputwidth);
                        }
                        else
                        {
-                               OutputNode = CreateBVConst(remainder, outputwidth);
-                               CONSTANTBV::BitVector_Destroy(quotient);
+                               CONSTANTBV::ErrCode e = CONSTANTBV::BitVector_Divide(quotient, tmp0, tmp1, remainder);
 
-                       }
+                               if (e != 0)
+                               {
+                                       cerr << "WARNING" << endl;
+                                       FatalError((const char*) CONSTANTBV::BitVector_Error(e));
+                               }
+
+                               if (SBVDIV == k)
+                               {
+                                       OutputNode = CreateBVConst(quotient, outputwidth);
+                                       CONSTANTBV::BitVector_Destroy(remainder);
+                               }
+                               else
+                               {
+                                       OutputNode = CreateBVConst(remainder, outputwidth);
+                                       CONSTANTBV::BitVector_Destroy(quotient);
 
+                               }
+                       }
                        break;
                }
 
@@ -309,87 +316,90 @@ ASTNode BeevMgr::BVConstEvaluator(const ASTNode& t)
                        tmp0 = CONSTANTBV::BitVector_Clone(tmp0);
                        tmp1 = CONSTANTBV::BitVector_Clone(tmp1);
 
-                       if (CONSTANTBV::BitVector_is_empty(tmp1))
+                       if (division_by_zero_returns_one && CONSTANTBV::BitVector_is_empty(tmp1))
                        {
-                               // If t is zero
-                               FatalError("Dividing by zero");
-                       }
+                               // Expecting a division by zero. Just return one.
+                               OutputNode = CreateOneConst(outputwidth);
 
-                       if (!isNegativeS && !isNegativeT)
+                       }
+                       else
                        {
-                               // Signs are both positive
-                               CONSTANTBV::ErrCode e = CONSTANTBV::BitVector_Div_Pos(quotient, tmp0, tmp1, remainder);
-                               if (e != CONSTANTBV::ErrCode_Ok)
+                               if (!isNegativeS && !isNegativeT)
                                {
-                                       cerr << "Error code was:" << e << endl;
-                                       assert(e == CONSTANTBV::ErrCode_Ok);
+                                       // Signs are both positive
+                                       CONSTANTBV::ErrCode e = CONSTANTBV::BitVector_Div_Pos(quotient, tmp0, tmp1, remainder);
+                                       if (e != CONSTANTBV::ErrCode_Ok)
+                                       {
+                                               cerr << "Error code was:" << e << endl;
+                                               assert(e == CONSTANTBV::ErrCode_Ok);
+                                       }
+                                       OutputNode = CreateBVConst(remainder, outputwidth);
                                }
-                               OutputNode = CreateBVConst(remainder, outputwidth);
-                       }
-                       else if (isNegativeS && !isNegativeT)
-                       {
-                               // S negative, T positive.
-                               CBV tmp0b = CONSTANTBV::BitVector_Create(inputwidth, true);
-                               CONSTANTBV::BitVector_Negate(tmp0b, tmp0);
+                               else if (isNegativeS && !isNegativeT)
+                               {
+                                       // S negative, T positive.
+                                       CBV tmp0b = CONSTANTBV::BitVector_Create(inputwidth, true);
+                                       CONSTANTBV::BitVector_Negate(tmp0b, tmp0);
 
-                               CONSTANTBV::ErrCode e = CONSTANTBV::BitVector_Div_Pos(quotient, tmp0b, tmp1, remainder);
+                                       CONSTANTBV::ErrCode e = CONSTANTBV::BitVector_Div_Pos(quotient, tmp0b, tmp1, remainder);
 
-                               assert(e == CONSTANTBV::ErrCode_Ok);
+                                       assert(e == CONSTANTBV::ErrCode_Ok);
 
-                               CBV remb = CONSTANTBV::BitVector_Create(inputwidth, true);
-                               CONSTANTBV::BitVector_Negate(remb, remainder);
+                                       CBV remb = CONSTANTBV::BitVector_Create(inputwidth, true);
+                                       CONSTANTBV::BitVector_Negate(remb, remainder);
 
-                               bool carry = false;
-                               CBV res = CONSTANTBV::BitVector_Create(inputwidth, true);
-                               CONSTANTBV::BitVector_add(res, remb, tmp1, &carry);
+                                       bool carry = false;
+                                       CBV res = CONSTANTBV::BitVector_Create(inputwidth, true);
+                                       CONSTANTBV::BitVector_add(res, remb, tmp1, &carry);
 
-                               OutputNode = CreateBVConst(res, outputwidth);
+                                       OutputNode = CreateBVConst(res, outputwidth);
 
-                               CONSTANTBV::BitVector_Destroy(tmp0b);
-                               CONSTANTBV::BitVector_Destroy(remb);
-                               CONSTANTBV::BitVector_Destroy(remainder);
-                       }
-                       else if (!isNegativeS && isNegativeT)
-                       {
-                               // If s is positive and t is negative
-                               CBV tmp1b = CONSTANTBV::BitVector_Create(inputwidth, true);
-                               CONSTANTBV::BitVector_Negate(tmp1b, tmp1);
+                                       CONSTANTBV::BitVector_Destroy(tmp0b);
+                                       CONSTANTBV::BitVector_Destroy(remb);
+                                       CONSTANTBV::BitVector_Destroy(remainder);
+                               }
+                               else if (!isNegativeS && isNegativeT)
+                               {
+                                       // If s is positive and t is negative
+                                       CBV tmp1b = CONSTANTBV::BitVector_Create(inputwidth, true);
+                                       CONSTANTBV::BitVector_Negate(tmp1b, tmp1);
 
-                               CONSTANTBV::ErrCode e = CONSTANTBV::BitVector_Div_Pos(quotient, tmp0, tmp1b, remainder);
+                                       CONSTANTBV::ErrCode e = CONSTANTBV::BitVector_Div_Pos(quotient, tmp0, tmp1b, remainder);
 
-                               assert(e == CONSTANTBV::ErrCode_Ok);
+                                       assert(e == CONSTANTBV::ErrCode_Ok);
 
-                               bool carry = false;
-                               CBV res = CONSTANTBV::BitVector_Create(inputwidth, true);
-                               CONSTANTBV::BitVector_add(res, remainder, tmp1, &carry);
+                                       bool carry = false;
+                                       CBV res = CONSTANTBV::BitVector_Create(inputwidth, true);
+                                       CONSTANTBV::BitVector_add(res, remainder, tmp1, &carry);
 
-                               OutputNode = CreateBVConst(res, outputwidth);
+                                       OutputNode = CreateBVConst(res, outputwidth);
 
-                               CONSTANTBV::BitVector_Destroy(tmp1b);
-                               CONSTANTBV::BitVector_Destroy(remainder);
-                       }
-                       else if (isNegativeS && isNegativeT)
-                       {
-                               // Signs are both negative
-                               CBV tmp0b = CONSTANTBV::BitVector_Create(inputwidth, true);
-                               CBV tmp1b = CONSTANTBV::BitVector_Create(inputwidth, true);
-                               CONSTANTBV::BitVector_Negate(tmp0b, tmp0);
-                               CONSTANTBV::BitVector_Negate(tmp1b, tmp1);
-
-                               CONSTANTBV::ErrCode e = CONSTANTBV::BitVector_Div_Pos(quotient, tmp0b, tmp1b, remainder);
-                               assert(e == CONSTANTBV::ErrCode_Ok);
-
-                               CBV remb = CONSTANTBV::BitVector_Create(inputwidth, true);
-                               CONSTANTBV::BitVector_Negate(remb, remainder);
-
-                               OutputNode = CreateBVConst(remb, outputwidth);
-                               CONSTANTBV::BitVector_Destroy(tmp0b);
-                               CONSTANTBV::BitVector_Destroy(tmp1b);
-                               CONSTANTBV::BitVector_Destroy(remainder);
-                       }
-                       else
-                       {
-                               FatalError("never get called");
+                                       CONSTANTBV::BitVector_Destroy(tmp1b);
+                                       CONSTANTBV::BitVector_Destroy(remainder);
+                               }
+                               else if (isNegativeS && isNegativeT)
+                               {
+                                       // Signs are both negative
+                                       CBV tmp0b = CONSTANTBV::BitVector_Create(inputwidth, true);
+                                       CBV tmp1b = CONSTANTBV::BitVector_Create(inputwidth, true);
+                                       CONSTANTBV::BitVector_Negate(tmp0b, tmp0);
+                                       CONSTANTBV::BitVector_Negate(tmp1b, tmp1);
+
+                                       CONSTANTBV::ErrCode e = CONSTANTBV::BitVector_Div_Pos(quotient, tmp0b, tmp1b, remainder);
+                                       assert(e == CONSTANTBV::ErrCode_Ok);
+
+                                       CBV remb = CONSTANTBV::BitVector_Create(inputwidth, true);
+                                       CONSTANTBV::BitVector_Negate(remb, remainder);
+
+                                       OutputNode = CreateBVConst(remb, outputwidth);
+                                       CONSTANTBV::BitVector_Destroy(tmp0b);
+                                       CONSTANTBV::BitVector_Destroy(tmp1b);
+                                       CONSTANTBV::BitVector_Destroy(remainder);
+                               }
+                               else
+                               {
+                                       FatalError("never get called");
+                               }
                        }
 
                        CONSTANTBV::BitVector_Destroy(tmp0);
@@ -404,45 +414,53 @@ ASTNode BeevMgr::BVConstEvaluator(const ASTNode& t)
                        CBV quotient = CONSTANTBV::BitVector_Create(inputwidth, true);
                        CBV remainder = CONSTANTBV::BitVector_Create(inputwidth, true);
 
-                       // tmp0 is dividend, tmp1 is the divisor
-                       //All parameters to BitVector_Div_Pos must be distinct unlike BitVector_Divide
-                       //FIXME the contents of the second parameter to Div_Pos is destroyed
-                       //As tmp0 is currently the same as the copy belonging to an ASTNode t[0]
-                       //this must be copied.
-                       tmp0 = CONSTANTBV::BitVector_Clone(tmp0);
-                       CONSTANTBV::ErrCode e = CONSTANTBV::BitVector_Div_Pos(quotient, tmp0, tmp1, remainder);
-                       CONSTANTBV::BitVector_Destroy(tmp0);
-
-                       if (0 != e)
+                       if (division_by_zero_returns_one && CONSTANTBV::BitVector_is_empty(tmp1))
+                       {
+                               // Expecting a division by zero. Just return one.
+                               OutputNode = CreateOneConst(outputwidth);
+                       }
+                       else
                        {
-                               //error printing
-                               if (counterexample_checking_during_refinement)
-                               {
-                                       output = CONSTANTBV::BitVector_Create(inputwidth, true);
-                                       OutputNode = CreateBVConst(output, outputwidth);
-                                       bvdiv_exception_occured = true;
 
-                                       //  CONSTANTBV::BitVector_Destroy(output);
-                                       break;
+                               // tmp0 is dividend, tmp1 is the divisor
+                               //All parameters to BitVector_Div_Pos must be distinct unlike BitVector_Divide
+                               //FIXME the contents of the second parameter to Div_Pos is destroyed
+                               //As tmp0 is currently the same as the copy belonging to an ASTNode t[0]
+                               //this must be copied.
+                               tmp0 = CONSTANTBV::BitVector_Clone(tmp0);
+                               CONSTANTBV::ErrCode e = CONSTANTBV::BitVector_Div_Pos(quotient, tmp0, tmp1, remainder);
+                               CONSTANTBV::BitVector_Destroy(tmp0);
+
+                               if (0 != e)
+                               {
+                                       //error printing
+                                       if (counterexample_checking_during_refinement)
+                                       {
+                                               output = CONSTANTBV::BitVector_Create(inputwidth, true);
+                                               OutputNode = CreateBVConst(output, outputwidth);
+                                               bvdiv_exception_occured = true;
+
+                                               //  CONSTANTBV::BitVector_Destroy(output);
+                                               break;
+                                       }
+                                       else
+                                       {
+                                               BVConstEvaluatorError(e, t);
+                                       }
+                               } //end of error printing
+
+                               //FIXME Not very standard in the current scheme
+                               if (BVDIV == k)
+                               {
+                                       OutputNode = CreateBVConst(quotient, outputwidth);
+                                       CONSTANTBV::BitVector_Destroy(remainder);
                                }
                                else
                                {
-                                       BVConstEvaluatorError(e, t);
+                                       OutputNode = CreateBVConst(remainder, outputwidth);
+                                       CONSTANTBV::BitVector_Destroy(quotient);
                                }
-                       } //end of error printing
-
-                       //FIXME Not very standard in the current scheme
-                       if (BVDIV == k)
-                       {
-                               OutputNode = CreateBVConst(quotient, outputwidth);
-                               CONSTANTBV::BitVector_Destroy(remainder);
                        }
-                       else
-                       {
-                               OutputNode = CreateBVConst(remainder, outputwidth);
-                               CONSTANTBV::BitVector_Destroy(quotient);
-                       }
-
                        break;
                }
                case ITE:

diff --git a/src/parser/main.cpp b/src/parser/main.cpp
index 9b2b6569d8ed5251b3a0c402f6e6f0f97acb7b72..e385850dfaba0d8c1801539cd67bf7bf2cd5ea2e 100644 (file)
--- a/src/parser/main.cpp
+++ b/src/parser/main.cpp
@@ -53,7 +53,7 @@ std::string helpstring = "\n\n";
 static const intptr_t INITIAL_MEMORY_PREALLOCATION_SIZE = 4000000;
 
 /******************************************************************************
- * MAIN FUNCTION: 
+ * MAIN FUNCTION:
  *
  * step 0. Parse the input into an ASTVec.
  * step 1. Do BV Rewrites
@@ -76,7 +76,7 @@ int main(int argc, char ** argv) {
     // FIXME: figure out how to get and print the real error message.
     BEEV::FatalError("Initial allocation of memory failed.");
   }
-  
+
   //populate the help string
   helpstring +=  "-r  : switch refinement off (optimizations are ON by default)\n";
   helpstring +=  "-w  : switch wordlevel solver off (optimizations are ON by default)\n";
@@ -116,9 +116,10 @@ int main(int argc, char ** argv) {
        break;
       case 'n':
        BEEV::print_output_flag = true;
-       break;  
+       break;
       case 'm':
        BEEV::smtlib_parser_flag=true;
+       BEEV::division_by_zero_returns_one = true;
        break;
       case 'p':
        BEEV::print_counterexample_flag = true;
@@ -170,7 +171,7 @@ int main(int argc, char ** argv) {
       if (BEEV::smtlib_parser_flag)
        {
          smtin = fopen(infile,"r");
-         if(smtin == NULL) 
+         if(smtin == NULL)
            {
              fprintf(stderr,"%s: Error: cannot open %s\n",prog,infile);
              BEEV::FatalError("");
@@ -179,7 +180,7 @@ int main(int argc, char ** argv) {
       else
        {
          cvcin = fopen(infile,"r");
-         if(cvcin == NULL) 
+         if(cvcin == NULL)
            {
              fprintf(stderr,"%s: Error: cannot open %s\n",prog,infile);
              BEEV::FatalError("");
@@ -188,19 +189,19 @@ int main(int argc, char ** argv) {
     }
   }
 
-  CONSTANTBV::ErrCode c = CONSTANTBV::BitVector_Boot(); 
+  CONSTANTBV::ErrCode c = CONSTANTBV::BitVector_Boot();
   if(0 != c) {
     cout << CONSTANTBV::BitVector_Error(c) << endl;
     return 0;
   }
 
-  //want to print the output always from the commandline. 
+  //want to print the output always from the commandline.
   BEEV::print_output_flag = true;
-  BEEV::globalBeevMgr_for_parser = new BEEV::BeevMgr();  
+  BEEV::globalBeevMgr_for_parser = new BEEV::BeevMgr();
 
   BEEV::SingleBitOne = BEEV::globalBeevMgr_for_parser->CreateOneConst(1);
   BEEV::SingleBitZero = BEEV::globalBeevMgr_for_parser->CreateZeroConst(1);
-  
+
   if (BEEV::smtlib_parser_flag)
     smtparse();
   else