From acc653383ea5dbb3a4e9cffa5c2735a9d2f22dca Mon Sep 17 00:00:00 2001
From: Tim King <taking@cs.nyu.edu>
Date: Tue, 1 Jun 2010 21:34:43 +0000
Subject: [PATCH] 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.

---
 src/theory/theory_engine.cpp | 14 ++++++++++----
 1 file 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);
 
-- 
2.30.2