Fix some small leaks when performing division by zero, and in the smtlib1 parser.

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

diff --git a/src/parser/smtlib.y b/src/parser/smtlib.y
index a18dceb85b4c993ab80b58928d1b845b9e80e4e7..d92fef518f98a87f132d4b63c9fce65379795498 100644 (file)
--- a/src/parser/smtlib.y
+++ b/src/parser/smtlib.y
@@ -373,6 +373,7 @@ user_value:
 USER_VAL_TOK
 {
   //cerr << "Printing user_value: " << *$1 << endl;
+  delete $1;
 }
 ;
 
@@ -681,6 +682,7 @@ an_term:
 BVCONST_TOK
 {
   $$ = new ASTNode(parserInterface->CreateBVConst($1, 10, 32));
+  delete $1;
 }
 | BVCONST_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK
 {
@@ -688,6 +690,9 @@ BVCONST_TOK
   delete $1;
 }
 | an_nonbvconst_term
+{
+$$ = $1;
+}
 ;
 
 an_nonbvconst_term: 
@@ -1024,6 +1029,7 @@ BITCONST_TOK { $$ = $1; }
       {
          n = parserInterface->nf->CreateTerm(BVCONCAT,w*(i+1),n,*$5);
       }
+       delete $5;
       $$ = new ASTNode(n);
     }
 |  BVSX_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK an_term 

diff --git a/src/simplifier/consteval.cpp b/src/simplifier/consteval.cpp
index 9b804fcc9a5ee81ced31c9b47353c19990db3bfb..b30fd7a001c5e5e9b9e7a029c0d95d22a81e0b23 100644 (file)
--- a/src/simplifier/consteval.cpp
+++ b/src/simplifier/consteval.cpp
@@ -281,6 +281,8 @@ namespace BEEV
             {
               // Expecting a division by zero. Just return one.
               OutputNode = _bm->CreateOneConst(outputwidth);
+              CONSTANTBV::BitVector_Destroy(remainder);
+              CONSTANTBV::BitVector_Destroy(quotient);
             }
           else
             {
@@ -338,7 +340,7 @@ namespace BEEV
             {
               // Expecting a division by zero. Just return one.
               OutputNode = _bm->CreateOneConst(outputwidth);
-
+              CONSTANTBV::BitVector_Destroy(remainder);
             }
           else
             {