From: Tim King <taking@cs.nyu.edu>
Date: Tue, 24 Jun 2014 23:19:58 +0000 (-0400)
Subject: Alternative lazier heuristic for assertion rewriting.
X-Git-Tag: cvc5-1.0.0~6700^2~5
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=af85f9839426a5672182902b3e094e5fb0b90a4f;p=cvc5.git

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 d3702ccd8..fa631a527 100644
--- 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);