diff options
| -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; |