3 files changed, 20 insertions, 13 deletions
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index c7f1780b6..6196ca357 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -458,9 +458,8 @@ Lit Solver::pickBranchLit()
     }
 #endif /* CVC4_REPLAY */
 
-    // Theory/DE requests
-    bool stopSearch = false;
-    nextLit = MinisatSatSolver::toMinisatLit(proxy->getNextDecisionRequest(stopSearch));
+    // Theory requests
+    nextLit = MinisatSatSolver::toMinisatLit(proxy->getNextTheoryDecisionRequest());
     while (nextLit != lit_Undef) {
       if(value(var(nextLit)) == l_Undef) {
         Debug("propagateAsDecision") << "propagateAsDecision(): now deciding on " << nextLit << std::endl;
@@ -469,12 +468,21 @@ Lit Solver::pickBranchLit()
       } else {
         Debug("propagateAsDecision") << "propagateAsDecision(): would decide on " << nextLit << " but it already has an assignment" << std::endl;
       }
-      nextLit = MinisatSatSolver::toMinisatLit(proxy->getNextDecisionRequest(stopSearch));
+      nextLit = MinisatSatSolver::toMinisatLit(proxy->getNextTheoryDecisionRequest());
     }
+    Debug("propagateAsDecision") << "propagateAsDecision(): decide on another literal" << std::endl;
+
+    // DE requests
+    bool stopSearch = false;
+    nextLit = MinisatSatSolver::toMinisatLit(proxy->getNextDecisionEngineRequest(stopSearch));
     if(stopSearch) {
       return lit_Undef;
     }
-    Debug("propagateAsDecision") << "propagateAsDecision(): decide on another literal" << std::endl;
+    if(nextLit != lit_Undef) {
+      Assert(value(var(nextLit)) == l_Undef, "literal to decide already has value");
+      decisions++;
+      return nextLit;
+    }
 
     Var next = var_Undef;
 
diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp
index a6908ff52..c9f19b42e 100644
--- a/src/prop/theory_proxy.cpp
+++ b/src/prop/theory_proxy.cpp
@@ -79,15 +79,12 @@ void TheoryProxy::enqueueTheoryLiteral(const SatLiteral& l) {
   d_queue.push(literalNode);
 }
 
-SatLiteral TheoryProxy::getNextDecisionRequest(bool &stopSearch) {
+SatLiteral TheoryProxy::getNextTheoryDecisionRequest() {
   TNode n = d_theoryEngine->getNextDecisionRequest();
-  if(not n.isNull()) {
-    return d_cnfStream->getLiteral(n);
-  }
+  return n.isNull() ? undefSatLiteral : d_cnfStream->getLiteral(n);
+}
 
-  // If theory doesn't give us a deicsion ask the decision engine. It
-  // may return in undefSatLiteral in which case the sat solver uses
-  // whatever default heuristic it has.
+SatLiteral TheoryProxy::getNextDecisionEngineRequest(bool &stopSearch) {
   Assert(d_decisionEngine != NULL);
   Assert(stopSearch != true);
   SatLiteral ret = d_decisionEngine->getNext(stopSearch);
diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h
index 5f1ea0e23..7b0aa2058 100644
--- a/src/prop/theory_proxy.h
+++ b/src/prop/theory_proxy.h
@@ -93,7 +93,9 @@ public:
 
   void enqueueTheoryLiteral(const SatLiteral& l);
 
-  SatLiteral getNextDecisionRequest(bool& stopSearch);
+  SatLiteral getNextTheoryDecisionRequest();
+
+  SatLiteral getNextDecisionEngineRequest(bool& stopSearch);
 
   bool theoryNeedCheck() const;