From: Dejan Jovanović <dejan.jovanovic@gmail.com>
Date: Thu, 8 Mar 2012 18:54:02 +0000 (+0000)
Subject: Fixin the bug Clark found. In final check, enqueued propagations were not discharged.
X-Git-Tag: cvc5-1.0.0~8280
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=84b8611466e01c6894ec5645cd805e849d70d423;p=cvc5.git

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 9f3285fff..1e31e354b 100644
--- 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;