Alternative lazier heuristic for assertion rewriting.

diff --git a/src/theory/arith/arith_ite_utils.cpp b/src/theory/arith/arith_ite_utils.cpp
index d3702ccd8017084396f07430bc1ff0c081b8d1a2..fa631a5276069bcbf1ce7808a717a49a00ed06e3 100644 (file)
--- a/src/theory/arith/arith_ite_utils.cpp
+++ b/src/theory/arith/arith_ite_utils.cpp
@@ -308,9 +308,6 @@ void ArithIteUtils::addImplications(Node x, Node y){
   // (=> (not x) y)
   // (=> (not y) x)
 
-  x = Rewriter::rewrite(x);
-  y = Rewriter::rewrite(y);
-
   Node xneg = x.negate();
   Node yneg = y.negate();
   d_implies[xneg].insert(y);
@@ -431,7 +428,7 @@ bool ArithIteUtils::solveBinOr(TNode binor){
 
         NodeManager* nm = NodeManager::currentNM();
 
-        Node cnd = findIteCnd(l, r);
+        Node cnd = findIteCnd(binor[0], binor[1]);
 
         Node sk = nm->mkSkolem("deor", nm->booleanType());
         Node ite = sk.iteNode(otherL, otherR);