This commit is a fix for a bug in removeITEs(). The check that the then branch is...

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 476091723bc17f18f45d8e905e3e6f361ceb57bb..1a0b25ade4dbf2d4609f5a8a1142bc23b8f7caf0 100644 (file)
--- 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);