From af85f9839426a5672182902b3e094e5fb0b90a4f Mon Sep 17 00:00:00 2001
From: Tim King <taking@cs.nyu.edu>
Date: Tue, 24 Jun 2014 19:19:58 -0400
Subject: [PATCH] Alternative lazier heuristic for assertion rewriting.

---
 src/theory/arith/arith_ite_utils.cpp | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

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