From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Thu, 9 Apr 2015 19:48:25 +0000 (-0400)
Subject: DE requests respect requirePhase
X-Git-Tag: cvc5-1.0.0~6353^2~1
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d53af187bea9162beb5f97ad9ed7251f45f81bbe;p=cvc5.git

DE requests respect requirePhase
---

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;