Disabled donePPSimpITE when unsat-cores are enabled (fixes bug648)

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 48f8b257c9376247996b9d1daae1e821fdffcf55..b5a2a1390b5db97a06360166ac5ec687b1118d99 100644 (file)
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -1559,6 +1559,12 @@ Node TheoryEngine::ppSimpITE(TNode assertion)
 }
 
 bool TheoryEngine::donePPSimpITE(std::vector<Node>& assertions){
+  // This pass does not support dependency tracking yet
+  // (learns substitutions from all assertions so just
+  // adding addDependence is not enough)
+  if (options::unsatCores()) {
+    return true;
+  }
   bool result = true;
   bool simpDidALotOfWork = d_iteUtilities->simpIteDidALotOfWorkHeuristic();
   if(simpDidALotOfWork){