merge from replay branch

1 files changed, 11 insertions, 0 deletions

diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index fd4b18222..10cd02f94 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -395,6 +395,13 @@ void Solver::popTrail() {
 
 Lit Solver::pickBranchLit()
 {
+#ifdef CVC4_REPLAY
+    Lit nextLit = proxy->getNextReplayDecision();
+    if (nextLit != lit_Undef) {
+      return nextLit;
+    }
+#endif /* CVC4_REPLAY */
+
     Var next = var_Undef;
 
     // Random decision:
@@ -1051,6 +1058,10 @@ lbool Solver::search(int nof_conflicts)
                     check_type = CHECK_WITHOUTH_PROPAGATION_FINAL;
                     continue;
                 }
+
+#ifdef CVC4_REPLAY
+                proxy->logDecision(next);
+#endif /* CVC4_REPLAY */
             }
 
             // Increase decision level and enqueue 'next'