Fixin the SAT solver for Andy. Even if a SAT lemma is added, a FULL-CHECK will be...

diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index a5774ee7b62a7577e784f01b20ebcedb9c7189c8..7ca117c2ee519a4cf13c3c15e5b0c07565047f13 100644 (file)
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -579,6 +579,7 @@ void Solver::uncheckedEnqueue(Lit p, CRef from)
 CRef Solver::propagate(TheoryCheckType type)
 {
     CRef confl = CRef_Undef;
+    recheck = false;
 
     ScopedBool scoped_bool(minisat_busy, true);
 
@@ -597,6 +598,7 @@ CRef Solver::propagate(TheoryCheckType type)
       theoryCheck(CVC4::theory::Theory::FULL_EFFORT);
       // If there are lemmas (or conflicts) update them
       if (lemmas.size() > 0) {
+        recheck = true;
         return updateLemmas();
       }
     }
@@ -914,6 +916,9 @@ lbool Solver::search(int nof_conflicts)
               if (!order_heap.empty() || qhead < trail.size()) {
                 check_type = CHECK_WITH_PROPAGATION_STANDARD;
                 continue;
+              } else if (recheck) {
+                // There some additional stuff added, so we go for another full-check
+                continue;
               } else {
                 // Yes, we're truly satisfiable
                 return l_True;

diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h
index 8eb82d9f1a09270bf0e8f45778cf4dce038f3bb9..1141e53c4647e2aec2292166d027e27d8de5adba 100644 (file)
--- a/src/prop/minisat/core/Solver.h
+++ b/src/prop/minisat/core/Solver.h
@@ -71,6 +71,9 @@ protected:
   /** Is the lemma removable */
   vec<bool> lemmas_removable;
 
+  /** Do a another check if FULL_EFFORT was the last one */
+  bool recheck;
+
   /** Shrink 'cs' to contain only clauses below given level */
   void removeClausesAboveLevel(vec<CRef>& cs, int level);