This commit is a fix for a bug in removeITEs(). The check that the then branch is a boolean should now be working. This fixes bug 138.

1 files changed, 10 insertions, 4 deletions

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 476091723..1a0b25ade 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -98,10 +98,9 @@ Node TheoryEngine::removeITEs(TNode node) {
   }
 
   if(node.getKind() == kind::ITE){
-    if(theoryOf(node[1]) != &d_bool && node[1].getKind() != kind::EQUAL) {
-      Assert( node.getNumChildren() == 3 );
-
-      Debug("ite") << theoryOf(node[1]) << " " << &d_bool <<endl;
+    Assert( node.getNumChildren() == 3 );
+    TypeNode nodeType = node[1].getType();
+    if(!nodeType.isBoolean()){
 
       Node skolem = nodeManager->mkVar(node.getType());
       Node newAssertion =
@@ -112,6 +111,13 @@ Node TheoryEngine::removeITEs(TNode node) {
                             nodeManager->mkNode(kind::EQUAL, skolem, node[2]));
       nodeManager->setAttribute(node, theory::IteRewriteAttr(), skolem);
 
+      if(debugTagIsOn("ite")){
+        Debug("ite") << "removeITEs([" << node.getId() << "," << node << "])"
+                     << "->"
+                     << "["<<newAssertion.getId() << "," << newAssertion << "]"
+                     << endl;
+      }
+
       Node preprocessed = rewrite(newAssertion);
       d_propEngine->assertFormula(preprocessed);