1 files changed, 3 insertions, 19 deletions
diff --git a/src/decision/decision_engine.h b/src/decision/decision_engine.h
index 28b15c9e0..c4eb29284 100644
--- a/src/decision/decision_engine.h
+++ b/src/decision/decision_engine.h
@@ -38,7 +38,7 @@ using namespace CVC4::decision;
 namespace CVC4 {
 
 class DecisionEngine {
-  vector<std::unique_ptr<ITEDecisionStrategy>> d_enabledITEStrategies;
+  std::unique_ptr<ITEDecisionStrategy> d_enabledITEStrategy;
   vector <ITEDecisionStrategy* > d_needIteSkolemMap;
   RelevancyStrategy* d_relevancyStrategy;
 
@@ -85,7 +85,7 @@ public:
     d_cnfStream = cs;
   }
 
-  /* enables decision stragies based on options */
+  /* Enables decision strategy based on options. */
   void init();
 
   /**
@@ -98,23 +98,7 @@ public:
   // Interface for External World to use our services
 
   /** Gets the next decision based on strategies that are enabled */
-  SatLiteral getNext(bool &stopSearch) {
-    NodeManager::currentResourceManager()->spendResource(
-        ResourceManager::Resource::DecisionStep);
-    Assert(d_cnfStream != NULL)
-        << "Forgot to set cnfStream for decision engine?";
-    Assert(d_satSolver != NULL)
-        << "Forgot to set satSolver for decision engine?";
-
-    SatLiteral ret = undefSatLiteral;
-    for (unsigned i = 0; i < d_enabledITEStrategies.size()
-                         and ret == undefSatLiteral and stopSearch == false;
-         ++i)
-    {
-      ret = d_enabledITEStrategies[i]->getNext(stopSearch);
-    }
-    return ret;
-  }
+  SatLiteral getNext(bool& stopSearch);
 
   /** Is a sat variable relevant */
   bool isRelevant(SatVariable var);