From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Thu, 3 Mar 2011 03:51:48 +0000 (+0000)
Subject: Improvement. Only create possible values if it can help.
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=daa360ae52b9b0d5bf814838c24db36ebfab5c32;p=francis%2Fstp.git

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 78eff91..1cffce5 100644
--- 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)