diff options
-rw-r--r-- | src/prop/minisat/core/Solver.cc | 5 | ||||
-rw-r--r-- | src/prop/minisat/core/Solver.h | 3 |
2 files changed, 8 insertions, 0 deletions
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index a5774ee7b..7ca117c2e 100644 --- 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 8eb82d9f1..1141e53c4 100644 --- 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); |