From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Wed, 9 Sep 2009 02:51:38 +0000 (+0000)
Subject: * Delete the bvsolver object as soon as we're finished with it. This frees any refere... 
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=0c44689f53708ed27ad266e493076b9e3f18c74a;p=francis%2Fstp.git

* Delete the bvsolver object as soon as we're finished with it. This frees any references it might hold to otherwise dead objects before the SAT solving starts.
* Returns were missing on some helper functions.


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

diff --git a/src/AST/printer/AssortedPrinters.cpp b/src/AST/printer/AssortedPrinters.cpp
index 1594b05..b6455de 100644
--- a/src/AST/printer/AssortedPrinters.cpp
+++ b/src/AST/printer/AssortedPrinters.cpp
@@ -29,17 +29,17 @@ namespace BEEV
 
   ostream &ASTNode::LispPrint(ostream &os, int indentation) const
   {
-    printer::Lisp_Print(os, *this, indentation);
+    return printer::Lisp_Print(os, *this, indentation);
   }
 
   ostream &ASTNode::LispPrint_indent(ostream &os, int indentation) const
   {
-    printer::Lisp_Print_indent(os, *this, indentation);
+    return printer::Lisp_Print_indent(os, *this, indentation);
   }
 
   ostream& ASTNode::PL_Print(ostream &os,  int indentation) const
   {
-    printer::PL_Print(os, *this, indentation);
+    return printer::PL_Print(os, *this, indentation);
   }
 
   //This is the IO manipulator.  It builds an object of class
diff --git a/src/to-sat/ToSAT.cpp b/src/to-sat/ToSAT.cpp
index 24c0599..cf6029c 100644
--- a/src/to-sat/ToSAT.cpp
+++ b/src/to-sat/ToSAT.cpp
@@ -923,7 +923,7 @@ namespace BEEV
     //round of substitution, solving, and simplification. ensures that
     //DAG is minimized as much as possibly, and ideally should
     //garuntee that all liketerms in BVPLUSes have been combined.
-    BVSolver bvsolver(this);
+    BVSolver* bvsolver = new BVSolver(this);
     SimplifyWrites_InPlace_Flag = false;
     Begin_RemoveWrites = false;
     start_abstracting = false;
@@ -939,7 +939,7 @@ namespace BEEV
           SimplifyFormula_TopLevel(simplified_solved_InputToSAT, false);
         ASTNodeStats("after simplification: ", simplified_solved_InputToSAT);
         simplified_solved_InputToSAT = 
-          bvsolver.TopLevelBVSolve(simplified_solved_InputToSAT);
+          bvsolver->TopLevelBVSolve(simplified_solved_InputToSAT);
         ASTNodeStats("after solving: ", simplified_solved_InputToSAT);
       } while (inputToSAT != simplified_solved_InputToSAT);
 
@@ -958,11 +958,14 @@ namespace BEEV
           SimplifyFormula_TopLevel(simplified_solved_InputToSAT, false);
         ASTNodeStats("after simplification: ", simplified_solved_InputToSAT);
         simplified_solved_InputToSAT = 
-          bvsolver.TopLevelBVSolve(simplified_solved_InputToSAT);
+          bvsolver->TopLevelBVSolve(simplified_solved_InputToSAT);
         ASTNodeStats("after solving: ", simplified_solved_InputToSAT);
       } while (inputToSAT != simplified_solved_InputToSAT);
     ASTNodeStats("After SimplifyWrites_Inplace: ", simplified_solved_InputToSAT);
 
+    delete bvsolver;
+    bvsolver = NULL;
+
     start_abstracting = (arraywrite_refinement_flag) ? true : false;
     SimplifyWrites_InPlace_Flag = false;
     Begin_RemoveWrites = (start_abstracting) ? false : true;