From d53af187bea9162beb5f97ad9ed7251f45f81bbe Mon Sep 17 00:00:00 2001
From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Thu, 9 Apr 2015 15:48:25 -0400
Subject: [PATCH] DE requests respect requirePhase

---
 src/prop/minisat/core/Solver.cc | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index ea370ac08..e54a03435 100644
--- 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;
-- 
2.30.2