Fixin the bug Clark found. In final check, enqueued propagations were not discharged.

diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index 9f3285ffff06ace606e69490ed1a02d864052529..1e31e354b43a7516215f81017cfe58e019d27319 100644 (file)
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -667,6 +667,8 @@ CRef Solver::propagate(TheoryCheckType type)
     if (type == CHECK_FINAL) {
       // Do the theory check
       theoryCheck(CVC4::theory::Theory::EFFORT_FULL);
+      // Pick up the theory propagated literals (there could be some, if new lemmas are added)
+      propagateTheory();
       // If there are lemmas (or conflicts) update them
       if (lemmas.size() > 0) {
         recheck = true;