From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Sun, 12 Sep 2010 14:21:38 +0000 (+0000)
Subject: Bugfix. r1018 caused wrong answers. It left out a case needed for booth recoding.
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=809a12feddf01f61d307651000dfa5167d34ca08;p=francis%2Fstp.git

Bugfix. r1018 caused wrong answers. It left out a case needed for booth recoding.

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

diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp
index 958377e..800706a 100644
--- a/src/STPManager/STP.cpp
+++ b/src/STPManager/STP.cpp
@@ -291,7 +291,6 @@ namespace BEEV {
                                        &toSATAIG
                                        );
 
-    delete cb;
     }
     else
       {
diff --git a/src/to-sat/AIG/ToSATAIG.cpp b/src/to-sat/AIG/ToSATAIG.cpp
index 7774d6a..1578115 100644
--- a/src/to-sat/AIG/ToSATAIG.cpp
+++ b/src/to-sat/AIG/ToSATAIG.cpp
@@ -13,13 +13,27 @@ namespace BEEV
         return false;
 
       BBNodeManagerAIG mgr;
-      Simplifier simp(bm);
-      BitBlaster<BBNodeAIG, BBNodeManagerAIG> bb(&mgr,cb,&simp,bm->defaultNodeFactory,&bm->UserFlags);
+      Simplifier *simp = new Simplifier(bm);
+      BitBlaster<BBNodeAIG, BBNodeManagerAIG> *bb = new BitBlaster<BBNodeAIG, BBNodeManagerAIG>(&mgr,cb,simp,bm->defaultNodeFactory,&bm->UserFlags);
+
+      // Even if we cleared the tables we could still have the hash table's buckets sitting around.
+      delete simp;
+      simp = NULL;
 
       bm->GetRunTimes()->start(RunTimes::BitBlasting);
-      BBNodeAIG BBFormula = bb.BBForm(input);
+      BBNodeAIG BBFormula = bb->BBForm(input);
       bm->GetRunTimes()->stop(RunTimes::BitBlasting);
-      bb.ClearAllTables();
+      delete bb;
+      bb = NULL;
+
+      //Clear out all the constant bit stuff before sending the SAT.
+      if (cb != NULL)
+        {
+          delete cb;
+          cb = NULL;
+        }
+
+
 
       assert(satSolver.nVars() ==0);
 
@@ -37,10 +51,6 @@ namespace BEEV
       BBFormula = BBNodeAIG(); // null node
       mgr.stop();
 
-      //Clear out all the constant bit stuff before sending the SAT.
-      if (cb != NULL)
-    	  cb->clearTables();
-
       bm->GetRunTimes()->start(RunTimes::SendingToSAT);
 
       for (int i = 0; i < cnfData->nVars; i++)
diff --git a/src/to-sat/BitBlaster.cpp b/src/to-sat/BitBlaster.cpp
index 0e08da0..10e46b7 100644
--- a/src/to-sat/BitBlaster.cpp
+++ b/src/to-sat/BitBlaster.cpp
@@ -1277,7 +1277,8 @@ void BitBlaster<BBNode,BBNodeManagerT>::mult_Booth(const BBNodeVec& x_i, const B
 			 pushP(products,i,y,x[i],nf);
 		 }
 
-		 else if (xt[i] == MINUS_ONE_MT)
+		 // A bit can not be true or false, as well as one of these two.
+		 if (xt[i] == MINUS_ONE_MT)
 		 {
 			 pushP(products,i,notY,BBTrue,nf);
 			 products[i].push(BBTrue);
@@ -1288,7 +1289,7 @@ void BitBlaster<BBNode,BBNodeManagerT>::mult_Booth(const BBNodeVec& x_i, const B
 			 pushP(products,i,y,BBTrue,nf);
 		 }
 
-		 else if (products[i].size() == 0)
+		 if (products[i].size() == 0)
 		   products[i].push(BBFalse);
 	 }
   }