Disables justification stop only for LRA if the problem contains no ites. This is a bandaid for constraints-tempo-width family of benchmarks.

1 files changed, 7 insertions, 0 deletions

diff --git a/src/decision/decision_engine.cpp b/src/decision/decision_engine.cpp
index 687515ff0..f634a28d9 100644
--- a/src/decision/decision_engine.cpp
+++ b/src/decision/decision_engine.cpp
@@ -82,6 +82,13 @@ void DecisionEngine::enableStrategy(DecisionStrategy* ds)
   d_enabledStrategies.push_back(ds);
 }
 
+void DecisionEngine::clearStrategies(){
+  for(unsigned i = 0; i < d_enabledStrategies.size(); ++i){
+    delete d_enabledStrategies[i];
+  }
+  d_enabledStrategies.clear();
+  d_needIteSkolemMap.clear();
+}
 
 bool DecisionEngine::isRelevant(SatVariable var)
 {