From 495787793b07a05f384824c92eef4e26d92228fc Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Wed, 23 Jan 2019 10:08:11 -0800 Subject: [PATCH] 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. --- src/prop/cryptominisat.cpp | 22 ++++++++++++++++------ 1 file 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 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; -- 2.30.2