projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 03e5936) | patch
Avoid using ProofManager in non-proof CMS build (#2814)
authorAndres Noetzli <andres.noetzli@gmail.com>
Wed, 23 Jan 2019 18:08:11 +0000 (10:08 -0800)
committerGitHub <noreply@github.com>
Wed, 23 Jan 2019 18:08:11 +0000 (10:08 -0800)
commit495787793b07a05f384824c92eef4e26d92228fc
tree5410648130deb815fca70d302e8fde4d6cef1414tree
parent03e5936c2e265a85d5a98d8cd4c4015da3b508f2commit | 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.
src/prop/cryptominisat.cpp diff | blob | history