diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2019-01-23 10:08:11 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-01-23 10:08:11 -0800 |
commit | 495787793b07a05f384824c92eef4e26d92228fc (patch) | |
tree | 5410648130deb815fca70d302e8fde4d6cef1414 /src/prop | |
parent | 03e5936c2e265a85d5a98d8cd4c4015da3b508f2 (diff) |
Avoid using ProofManager in non-proof CMS build (#2814)
PR #2786 changed `CryptoMinisatSolver::addClause()` to register clauses
with the bit-vector proof if proofs are turned on. The new code
requested the `ProofManager` even when proofs were turned off, which
made the `eager-inc-cryptominisat.smt2` regression and our nightlies
fail. This commit guards the access to the `ProofManager`, restoring the
semantics of the original code when proofs are turned off.
Diffstat (limited to 'src/prop')
-rw-r--r-- | src/prop/cryptominisat.cpp | 22 |
1 files changed, 16 insertions, 6 deletions
diff --git a/src/prop/cryptominisat.cpp b/src/prop/cryptominisat.cpp index c04fb8b56..970ba13cf 100644 --- a/src/prop/cryptominisat.cpp +++ b/src/prop/cryptominisat.cpp @@ -119,13 +119,23 @@ ClauseId CryptoMinisatSolver::addClause(SatClause& clause, bool removable){ std::vector<CMSat::Lit> internal_clause; toInternalClause(clause, internal_clause); bool nowOkay = d_solver->add_clause(internal_clause); - ClauseId freshId = ClauseId(ProofManager::currentPM()->nextId()); - THEORY_PROOF( - // If this clause results in a conflict, then `nowOkay` may be false, but - // we still need to register this clause as used. Thus, we look at - // `d_okay` instead - if (d_bvp && d_okay) { d_bvp->registerUsedClause(freshId, clause); }) + ClauseId freshId; + if (THEORY_PROOF_ON()) + { + freshId = ClauseId(ProofManager::currentPM()->nextId()); + // If this clause results in a conflict, then `nowOkay` may be false, but + // we still need to register this clause as used. Thus, we look at + // `d_okay` instead + if (d_bvp && d_okay) + { + d_bvp->registerUsedClause(freshId, clause); + } + } + else + { + freshId = ClauseIdError; + } d_okay &= nowOkay; return freshId; |