diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-05-25 13:26:16 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-05-25 13:26:16 -0700 |
| commit | 9fc8a7885c89e488daeeaf73c9f099b9d906f3ca (patch) | |
| tree | 5dd07a570612b29b85f2b21899c36cf0a27fd3d8 | |
| parent | d7e4d90e547427f511dfabb66bf3686cb987324b (diff) | |
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.
| -rw-r--r-- | src/prop/minisat/core/Solver.cc | 18 |
1 files 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<Lit>& 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; |