Fix. I thought the code I checked-in just now wasn't active. But it was. This 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 3417ff7b7bf405a904cee8100422e434de241b99..1efeb89c17a705c7083307c6fb470d64a38d62a5 100644 (file)
--- 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 46cc4cf8f9476951d81097910eea8fa5c7be9ed0..7494aae938be2d621f1cfa74b598eb061250aa97 100644 (file)
--- 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;