Turning off aggressive arith ite simplifications during incremental solving.

diff --git a/src/theory/arith/arith_ite_utils.cpp b/src/theory/arith/arith_ite_utils.cpp
index 757dab8fb1449b0a99de2a7220661ce152a219f7..2b31831e2515b8bb43b9e2aefb53765102f9c184 100644 (file)
--- 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 8d36d9e05cb57df427092cc7ce1e7a151106fb37..d34f0cd12cf767a88ab9b1ab1f3d20712ca4c1d4 100644 (file)
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -1530,7 +1530,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{
 
@@ -1575,7 +1580,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());