2 files changed, 32 insertions, 10 deletions
diff --git a/src/decision/decision_engine.cpp b/src/decision/decision_engine.cpp
index 7d31d930f..dc798626e 100644
--- a/src/decision/decision_engine.cpp
+++ b/src/decision/decision_engine.cpp
@@ -56,21 +56,20 @@ void DecisionEngine::init()
   {
     ITEDecisionStrategy* ds =
       new decision::JustificationHeuristic(this, d_userContext, d_satContext);
-    d_enabledStrategies.push_back(ds);
+    enableStrategy(ds);
     d_needIteSkolemMap.push_back(ds);
   }
 }
 
-void DecisionEngine::shutdown()
-{
-  Trace("decision") << "Shutting down decision engine" << std::endl;
 
-  Assert(d_engineState == 1);
-  d_engineState = 2;
+void DecisionEngine::enableStrategy(DecisionStrategy* ds)
+{
+  d_enabledStrategies.push_back(ds);
+}
 
-  for (DecisionStrategy* s : d_enabledStrategies)
-  {
-    delete s;
+void DecisionEngine::clearStrategies(){
+  for(unsigned i = 0; i < d_enabledStrategies.size(); ++i){
+    delete d_enabledStrategies[i];
   }
   d_enabledStrategies.clear();
   d_needIteSkolemMap.clear();
diff --git a/src/decision/decision_engine.h b/src/decision/decision_engine.h
index afa306325..5ebcda8fe 100644
--- a/src/decision/decision_engine.h
+++ b/src/decision/decision_engine.h
@@ -96,12 +96,22 @@ public:
   /* enables decision stragies based on options */
   void init();
 
+  /* clears all of the strategies */
+  void clearStrategies();
+
+
   /**
    * This is called by SmtEngine, at shutdown time, just before
    * destruction.  It is important because there are destruction
    * ordering issues between some parts of the system.
    */
-  void shutdown();
+  void shutdown() {
+    Assert(d_engineState == 1);
+    d_engineState = 2;
+
+    Trace("decision") << "Shutting down decision engine" << std::endl;
+    clearStrategies();
+  }
 
   // Interface for External World to use our services
 
@@ -160,6 +170,11 @@ public:
 
   // External World helping us help the Strategies
 
+  /** If one of the enabled strategies needs them  */
+  /* bool needIteSkolemMap() { */
+  /*   return d_needIteSkolemMap.size() > 0; */
+  /* } */
+
   /**
    * Add a list of assertions from an AssertionPipeline.
    */
@@ -193,6 +208,14 @@ public:
   Node getNode(SatLiteral l) {
     return d_cnfStream->getNode(l);
   }
+
+private:
+  /**
+   * Enable a particular decision strategy, also updating
+   * corresponding vector<DecisionStrategy*>-s is the engine
+   */
+  void enableStrategy(DecisionStrategy* ds);
+
 };/* DecisionEngine class */
 
 }/* CVC4 namespace */