From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Sat, 28 Aug 2010 03:01:26 +0000 (+0000)
Subject: Fix. I thought the code I checked-in just now wasn't active. But it was. This patch... 
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=89ccd9b4e56b854a9e6a104d36ffdbc82627f7be;p=francis%2Fstp.git

Fix. I thought the code I checked-in just now wasn't active. But it was. This patch adds a flag to disable the prior patch.




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

diff --git a/src/STPManager/UserDefinedFlags.h b/src/STPManager/UserDefinedFlags.h
index 3417ff7..1efeb89 100644
--- a/src/STPManager/UserDefinedFlags.h
+++ b/src/STPManager/UserDefinedFlags.h
@@ -119,6 +119,8 @@ namespace BEEV
 
     bool enable_AIG_rewrites_flag;
 
+    bool simplify_during_BB_flag;
+
     // Available back-end SAT solvers.
     enum SATSolvers
       {
@@ -235,6 +237,9 @@ namespace BEEV
 
       enable_AIG_rewrites_flag = false;
 
+      // If the bit-blaster discovers new constants, should the term simplifier be re-run.
+      simplify_during_BB_flag=false;
+
     } //End of constructor for UserDefinedFlags
 
   }; //End of struct UserDefinedFlags
diff --git a/src/to-sat/BitBlaster.cpp b/src/to-sat/BitBlaster.cpp
index 46cc4cf..7494aae 100644
--- a/src/to-sat/BitBlaster.cpp
+++ b/src/to-sat/BitBlaster.cpp
@@ -269,7 +269,7 @@ const BBNodeVec BitBlaster<BBNode,BBNodeManagerT>::BBTerm(const ASTNode& _term,
 	// call SimplifyTerm on ite(true,y,z), which will do the expected simplification.
 	// Then the term that we bitblast will by "y".
 
-	if (uf !=NULL && uf->optimize_flag)
+	if (uf !=NULL && uf->optimize_flag && uf->simplify_during_BB_flag)
 	{
           const int numberOfChildren = term.Degree();
           vector<BBNodeVec> ch;