From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Mon, 26 Apr 2021 14:46:56 +0000 (-0300)
Subject: Fix assertions in SAT solver (#6443)
X-Git-Tag: cvc5-1.0.0~1834
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=bff297565a91e020c845d2984a3f0f921f887bba;p=cvc5.git

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 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();