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.

diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index 19f1bff97884c7da21c55063aa4ecda26f05ceea..971fb95d2d3a3cc5a5483f793a24e7cbf7cbb6c8 100644 (file)
--- 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();