Improvement. Add a configuration option to remove a simplification, reduce its limit...

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

diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp
index 21fd657ca1c452323c1edb8f5785d164ab4b7285..25a6a9f0bf470b6832ceac4eddd1f38e5f3e2889 100644 (file)
--- a/src/simplifier/simplifier.cpp
+++ b/src/simplifier/simplifier.cpp
@@ -542,7 +542,7 @@ namespace BEEV
   }
 
   bool
-  getPossibleValues(const ASTNode&n, ASTNodeSet& visited, vector<ASTNode>& found, int maxCount = 45)
+  getPossibleValues(const ASTNode&n, ASTNodeSet& visited, vector<ASTNode>& found, int maxCount = 5)
   {
     if (maxCount <= 0)
       return false;
@@ -1005,7 +1005,7 @@ namespace BEEV
         return r;
       }
 
-    if ((k1 == ITE || k1 == BVCONST) && (k2 == ITE || k2 == BVCONST))
+    if ((k1 == ITE || k1 == BVCONST) && (k2 == ITE || k2 == BVCONST) && _bm->UserFlags.isSet("ite-const","1"))
       {
         // If it can only evaluate to constants on the LHS and the RHS, and those constants are never equal,
         // then it must be false. e.g.   ite( f, 10 , 20 ) = ite (g, 30 ,12)