From f5c1d96a20dc4fc7adda134bd05bf1a8b1528785 Mon Sep 17 00:00:00 2001
From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Thu, 8 Jul 2010 05:16:17 +0000
Subject: [PATCH] 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
---
 src/parser/smtlib.y          | 6 ++++++
 src/simplifier/consteval.cpp | 4 +++-
 2 files changed, 9 insertions(+), 1 deletion(-)

diff --git a/src/parser/smtlib.y b/src/parser/smtlib.y
index a18dceb..d92fef5 100644
--- 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 9b804fc..b30fd7a 100644
--- 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
             {
-- 
2.47.3