Improvement. Only create possible values if it can help.

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

diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp
index 78eff9166be56cbd6c078263704ef54a49fc277c..1cffce5da3663baf56a7e7143595879d13dbb02d 100644 (file)
--- a/src/simplifier/simplifier.cpp
+++ b/src/simplifier/simplifier.cpp
@@ -995,6 +995,7 @@ namespace BEEV
         return r;
     }
 
+    if ((k1 == ITE || k1 == BVCONST) &&  (k2 == ITE || k2 == BVCONST))
     {
       // 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)