From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Sat, 7 Apr 2012 00:20:57 +0000 (+0000)
Subject: Improvement. Change how the bitblast equivalence checking is enabled.
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=3b9437426b0eada93abd0f1f7dce3098647501b1;p=francis%2Fstp.git

Improvement. Change how the bitblast equivalence checking is enabled.

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

diff --git a/src/STPManager/UserDefinedFlags.h b/src/STPManager/UserDefinedFlags.h
index 179b851..1653bc3 100644
--- a/src/STPManager/UserDefinedFlags.h
+++ b/src/STPManager/UserDefinedFlags.h
@@ -294,8 +294,6 @@ namespace BEEV
       // If the bit-blaster discovers new constants, should the term simplifier be re-run.
       simplify_during_BB_flag=false;
 
-      set("bb-equiv","1");
-
     } //End of constructor for UserDefinedFlags
 
   }; //End of struct UserDefinedFlags
diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp
index 25a6a9f..edcefae 100644
--- a/src/simplifier/simplifier.cpp
+++ b/src/simplifier/simplifier.cpp
@@ -219,7 +219,7 @@ namespace BEEV
     // leaves just one instance of the constraint, so it we replace it with true/false
     // the constraint is lost. This is subsumed by constant bit propagation, so I suspect
     // it's not a big loss.
-    if (!_bm->UserFlags.isSet("bb-equiv",""))
+    if (!_bm->UserFlags.isSet("bb-equiv","1"))
       AlwaysTrueHashSet.insert(key.GetNodeNum());
   }
 
diff --git a/src/to-sat/BitBlaster.cpp b/src/to-sat/BitBlaster.cpp
index 9595663..8083007 100644
--- a/src/to-sat/BitBlaster.cpp
+++ b/src/to-sat/BitBlaster.cpp
@@ -167,7 +167,7 @@ namespace BEEV
           fromTo.insert(make_pair(n, r));
         }
 
-      if (form.GetSTPMgr()->UserFlags.isSet("bb-equiv",""))
+      if (form.GetSTPMgr()->UserFlags.isSet("bb-equiv","1"))
       {
         HASHMAP <intptr_t ,ASTNode> nodeToFn;
         typename map<ASTNode, BBNode>::iterator it;
@@ -203,7 +203,7 @@ namespace BEEV
       }
 
       typedef HASHMAP<vector<BBNode>, ASTNode,BBVecHasher <BBNode>, BBVecEquals<BBNode> > M;
-      if (form.GetSTPMgr()->UserFlags.isSet("bb-equiv",""))
+      if (form.GetSTPMgr()->UserFlags.isSet("bb-equiv","1"))
         {
           M lookup;
           typename std::map<ASTNode, vector<BBNode> >::iterator it;
@@ -791,7 +791,7 @@ namespace BEEV
             results.push_back(BBTerm(term[i], support));
 
           const int bitWidth = term[0].GetValueWidth();
-          std::vector<list<BBNode> > products(bitWidth);
+          std::vector<list<BBNode> > products(bitWidth+1);
           for (int i = 0; i < bitWidth; i++)
             {
             for (int j = 0; j < results.size(); j++)