From 9fc8a7885c89e488daeeaf73c9f099b9d906f3ca Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Fri, 25 May 2018 13:26:16 -0700 Subject: [PATCH] MiniSat: Be more careful about running proof code (#1982) In `addClause_()`, we were checking the condition `ca[confl].size() == 1` regardless if proofs were enabled or not, even though both branches of the if statement only do something when proofs are enabled. This lead to issue #1978 occurring even when not generating proofs. Note: This commit is *not* a fix for #1978 but it makes sure that the issue does not occur when not generating proofs/unsat cores. --- src/prop/minisat/core/Solver.cc | 18 +++++++++++++----- 1 file changed, 13 insertions(+), 5 deletions(-) diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index 0967f434c..2136f22df 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -421,11 +421,19 @@ bool Solver::addClause_(vec& ps, bool removable, ClauseId& id) ); CRef confl = propagate(CHECK_WITHOUT_THEORY); if(! (ok = (confl == CRef_Undef)) ) { - if(ca[confl].size() == 1) { - PROOF( id = ProofManager::getSatProof()->storeUnitConflict(ca[confl][0], LEARNT); ); - PROOF( ProofManager::getSatProof()->finalizeProof(CVC4::Minisat::CRef_Lazy); ) - } else { - PROOF( ProofManager::getSatProof()->finalizeProof(confl); ); + if (PROOF_ON()) + { + if (ca[confl].size() == 1) + { + id = ProofManager::getSatProof()->storeUnitConflict( + ca[confl][0], LEARNT); + ProofManager::getSatProof()->finalizeProof( + CVC4::Minisat::CRef_Lazy); + } + else + { + ProofManager::getSatProof()->finalizeProof(confl); + } } } return ok; -- 2.30.2