DE requests respect requirePhase

diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index ea370ac0819ebe1eadb3197ba6612f8eda43e3df..e54a03435f9f3c1faeade1870d2d949488fb81f4 100644 (file)
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -482,6 +482,7 @@ Lit Solver::pickBranchLit()
     Lit nextLit;
 
 #ifdef CVC4_REPLAY
+
     nextLit = MinisatSatSolver::toMinisatLit(proxy->getNextReplayDecision());
 
     if (nextLit != lit_Undef) {
@@ -512,7 +513,12 @@ Lit Solver::pickBranchLit()
     if(nextLit != lit_Undef) {
       Assert(value(var(nextLit)) == l_Undef, "literal to decide already has value");
       decisions++;
-      return nextLit;
+      Var next = var(nextLit);
+      if(polarity[next] & 0x2) {
+        return mkLit(next, polarity[next] & 0x1);
+      } else {
+        return nextLit;
+      }
     }
 
     Var next = var_Undef;