small bug fix and performance fix in ite simplifier

diff --git a/src/theory/ite_simplifier.cpp b/src/theory/ite_simplifier.cpp
index bf031fc946491e28143d7b127f470b8fa4b8905d..ab8f159a9d67e8bb068dad5d9fe0e0c567e42c86 100644 (file)
--- a/src/theory/ite_simplifier.cpp
+++ b/src/theory/ite_simplifier.cpp
@@ -447,10 +447,7 @@ Node ITESimplifier::simplifyWithCare(TNode e)
         if (done) break;
 
         Assert(v.getNumChildren() > 1);
-        cs2 = getNewSet();
-        cs2.getCareSet() = css;
-        cs2.getCareSet().insert(v[1]);
-        updateQueue(queue, v[0], cs2);
+        updateQueue(queue, v[0], cs);
         cs2 = getNewSet();
         cs2.getCareSet() = css;
         cs2.getCareSet().insert(v[0]);
@@ -473,10 +470,7 @@ Node ITESimplifier::simplifyWithCare(TNode e)
         if (done) break;
 
         Assert(v.getNumChildren() > 1);
-        cs2 = getNewSet();
-        cs2.getCareSet() = css;
-        cs2.getCareSet().insert(v[1].negate());
-        updateQueue(queue, v[0], cs2);
+        updateQueue(queue, v[0], cs);
         cs2 = getNewSet();
         cs2.getCareSet() = css;
         cs2.getCareSet().insert(v[0].negate());

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 161d0febde5a9a0b8a3fc07cde71b2fccdc4105b..0e7d7d51ce9fa41fa62aa6170b31bd6fa5c1eabc 100644 (file)
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -1172,7 +1172,7 @@ void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) {
 Node TheoryEngine::ppSimpITE(TNode assertion)
 {
   Node result = d_iteSimplifier.simpITE(assertion);
-  result = d_iteSimplifier.simplifyWithCare(result);
+  result = d_iteSimplifier.simplifyWithCare(Rewriter::rewrite(result));
   result = Rewriter::rewrite(result);
   return result;
 }