From 2f3ab34dcf0c5bfefff2f40ec164b82dfdc66835 Mon Sep 17 00:00:00 2001
From: Liana Hadarean <lianahady@gmail.com>
Date: Wed, 7 Oct 2015 17:02:05 +0100
Subject: [PATCH] Disabled donePPSimpITE when unsat-cores are enabled (fixes
 bug648)

---
 src/theory/theory_engine.cpp | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 48f8b257c..b5a2a1390 100644
--- 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){
-- 
2.30.2