Clear the contents of the BBTermMemo and BBFormMemo before calling the SAT solver.

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

diff --git a/src/to-sat/ToSAT.cpp b/src/to-sat/ToSAT.cpp
index 794a8331b31a5ab495bb89d64350fb42d6b92e63..02db33fb9175551e94e76c8def46b1bbe2d0b4d2 100644 (file)
--- a/src/to-sat/ToSAT.cpp
+++ b/src/to-sat/ToSAT.cpp
@@ -260,11 +260,13 @@ namespace BEEV
   {
     bm->GetRunTimes()->start(RunTimes::BitBlasting);
 
-
-    BitBlasterNew BB(bm);
-    BBNodeSet set;
-    ASTNode BBFormula = BB.BBForm(input,set);
-    assert(set.size() == 0); // doesn't yet work.
+    ASTNode BBFormula;
+    {
+       BitBlasterNew BB(bm);
+       BBNodeSet set;
+       BBFormula = BB.BBForm(input,set);
+       assert(set.size() == 0); // doesn't yet work.
+    }
 
     bm->ASTNodeStats("after bitblasting: ", BBFormula);
     bm->GetRunTimes()->stop(RunTimes::BitBlasting);