Turning off aggressive arith ite simplifications during incremental solving.

2 files changed, 11 insertions, 2 deletions

diff --git a/src/theory/arith/arith_ite_utils.cpp b/src/theory/arith/arith_ite_utils.cpp
index 757dab8fb..2b31831e2 100644
--- a/src/theory/arith/arith_ite_utils.cpp
+++ b/src/theory/arith/arith_ite_utils.cpp
@@ -15,6 +15,7 @@
  ** \todo document this file
  **/
 
+#include "smt/options.h"
 #include "theory/arith/arith_ite_utils.h"
 #include "theory/arith/normal_form.h"
 #include "theory/arith/arith_utilities.h"
@@ -272,6 +273,7 @@ void ArithIteUtils::addSubstitution(TNode f, TNode t){
 }
 
 Node ArithIteUtils::applySubstitutions(TNode f){
+  AlwaysAssert(!options::incrementalSolving());
   return d_subs->apply(f);
 }
 
@@ -285,6 +287,7 @@ Node ArithIteUtils::selectForCmp(Node n) const{
 }
 
 void ArithIteUtils::learnSubstitutions(const std::vector<Node>& assertions){
+  AlwaysAssert(!options::incrementalSolving());
   for(size_t i=0, N=assertions.size(); i < N; ++i){
     collectAssertions(assertions[i]);
   }
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index a70f84b76..ecc2259dd 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -1531,7 +1531,12 @@ void TheoryEngine::mkAckermanizationAsssertions(std::vector<Node>& assertions) {
 
 Node TheoryEngine::ppSimpITE(TNode assertion)
 {
-  if(!d_iteRemover.containsTermITE(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
+    return assertion;
+  } else if(!d_iteRemover.containsTermITE(assertion)){
     return assertion;
   }else{
 
@@ -1576,7 +1581,8 @@ bool TheoryEngine::donePPSimpITE(std::vector<Node>& assertions){
   }
 
   // Do theory specific preprocessing passes
-  if(d_logicInfo.isTheoryEnabled(theory::THEORY_ARITH)){
+  if(d_logicInfo.isTheoryEnabled(theory::THEORY_ARITH)
+     && !options::incrementalSolving() ){
     if(!simpDidALotOfWork){
       ContainsTermITEVisitor& contains = *d_iteRemover.getContainsVisitor();
       arith::ArithIteUtils aiteu(contains, d_userContext, getModel());