From: Clark Barrett <barrett@cs.nyu.edu>
Date: Mon, 9 May 2016 22:21:22 +0000 (-0700)
Subject: Re-enabling ite simplification in incremental mode - no reason why
X-Git-Tag: cvc5-1.0.0~6049^2~51
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c15ff43597b41ea457befecb1b0e2402e28cb523;p=cvc5.git

Re-enabling ite simplification in incremental mode - no reason why
it should be a problem.
---

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index f2231ff7a..1ab4c228b 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -1558,15 +1558,9 @@ void TheoryEngine::mkAckermanizationAsssertions(std::vector<Node>& assertions) {
 
 Node TheoryEngine::ppSimpITE(TNode assertion)
 {
-  if(options::incrementalSolving()){
-    // disabling the d_iteUtilities->simpITE(assertion) pass for incremental solving.
-    // This is paranoia. We do not actually know of a bug coming from this.
-    // TODO re-enable
+  if (!d_iteRemover.containsTermITE(assertion)) {
     return assertion;
-  } else if(!d_iteRemover.containsTermITE(assertion)){
-    return assertion;
-  }else{
-
+  } else {
     Node result = d_iteUtilities->simpITE(assertion);
     Node res_rewritten = Rewriter::rewrite(result);
 
@@ -1576,10 +1570,9 @@ Node TheoryEngine::ppSimpITE(TNode assertion)
       Chat() << "ending simplifyWithCare()"
              << " post simplifyWithCare()" << postSimpWithCare.getId() << endl;
       result = Rewriter::rewrite(postSimpWithCare);
-    }else{
+    } else {
       result = res_rewritten;
     }
-
     return result;
   }
 }