* Delete the bvsolver object as soon as we're finished with it. This frees any refere...

* 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 1594b057b2c3c772f47bc29eb0219763a864fe4b..b6455de0adf38d0264106367c7b0bb48c691103c 100644 (file)
--- 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 24c059936c62bfb1f0e386601dfffd8d30f9a08f..cf6029cbbb7b5789c916c943459dd87cbcd51c7a 100644 (file)
--- 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;