diff options
| author | Alex Ozdemir <aozdemir@hmc.edu> | 2019-03-02 13:00:45 -0800 |
|---|---|---|
| committer | Alex Ozdemir <aozdemir@hmc.edu> | 2019-03-02 13:00:45 -0800 |
| commit | 482786287aaab687639bf70673572f221047dbdc (patch) | |
| tree | fbf8b3b9f09b22b05c36027da835835bc801f021 /src/proof/proof_manager.cpp | |
| parent | f93a68fdf2b62a40dd74bdb04aafb60ea7f1a69a (diff) | |
Enable CryptoMiniSat-backed BV proofs
* Connect the plumbing so that BV proofs are enabled when using
CryptoMiniSat
* Also fixed a bug in CNF-proof generation
* Specifically, CNF proofs broke when proving tautological clauses.
Now they don't.
Diffstat (limited to 'src/proof/proof_manager.cpp')
| -rw-r--r-- | src/proof/proof_manager.cpp | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp index 9878972bf..42396cd6a 100644 --- a/src/proof/proof_manager.cpp +++ b/src/proof/proof_manager.cpp @@ -730,8 +730,7 @@ void LFSCProof::toStream(std::ostream& out) const out << ";; Printing final unsat proof \n"; if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER && ProofManager::getBitVectorProof()) { - proof::LFSCProofPrinter::printResolutionEmptyClause( - ProofManager::getBitVectorProof()->getSatProof(), out, paren); + ProofManager::getBitVectorProof()->printEmptyClauseProof(out, paren); } else { // print actual resolution proof proof::LFSCProofPrinter::printResolutions(d_satProof, out, paren); |