diff options
author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2015-04-09 15:48:25 -0400 |
---|---|---|
committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2015-04-09 15:48:25 -0400 |
commit | d53af187bea9162beb5f97ad9ed7251f45f81bbe (patch) | |
tree | b8b6fe1d60b64f37c850e02ef5663f1621b6531a /src/prop | |
parent | 9350915de95c1b569eea8262c4602708dfa6c3fa (diff) |
DE requests respect requirePhase
Diffstat (limited to 'src/prop')
-rw-r--r-- | src/prop/minisat/core/Solver.cc | 8 |
1 files changed, 7 insertions, 1 deletions
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; |