Fix assertions in SAT solver (#6443)

Due to our recent changes in the unsat core infrastructure we were doing a couple assertions wrong during conflict analysis. This commit fixes them.

1 files changed, 4 insertions, 4 deletions

diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index 19f1bff97..971fb95d2 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -2249,8 +2249,8 @@ CRef Solver::updateLemmas() {
   // Last index in the trail
   int backtrack_index = trail.size();
 
-  Assert(!options::unsatCores() || needProof()
-         || lemmas.size() == (int)lemmas_cnf_assertion.size());
+  Assert(options::unsatCoresMode() != options::UnsatCoresMode::OLD_PROOF
+         || lemmas.size() == static_cast<int>(lemmas_cnf_assertion.size()));
 
   // Attach all the clauses and enqueue all the propagations
   for (int j = 0; j < lemmas.size(); ++j)
@@ -2334,8 +2334,8 @@ CRef Solver::updateLemmas() {
     }
   }
 
-  Assert(!options::unsatCores() || needProof()
-         || lemmas.size() == (int)lemmas_cnf_assertion.size());
+  Assert(options::unsatCoresMode() != options::UnsatCoresMode::OLD_PROOF
+         || lemmas.size() == static_cast<int>(lemmas_cnf_assertion.size()));
   // Clear the lemmas
   lemmas.clear();
   lemmas_cnf_assertion.clear();