From: Tim King <taking@cs.nyu.edu>
Date: Tue, 1 Jun 2010 21:34:43 +0000 (+0000)
Subject: This commit is a fix for a bug in removeITEs().  The check that the then branch is... 
X-Git-Tag: cvc5-1.0.0~9013
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=acc653383ea5dbb3a4e9cffa5c2735a9d2f22dca;p=cvc5.git

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.
---

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);