From 5d0a5a729680a1db3f44e31037955390e86440ce Mon Sep 17 00:00:00 2001 From: Alex Ozdemir Date: Fri, 15 Mar 2019 18:51:47 -0700 Subject: Enable CryptoMiniSat-backed BV proofs (#2847) * 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. --- src/proof/bitvector_proof.cpp | 8 ++++++++ 1 file changed, 8 insertions(+) (limited to 'src/proof/bitvector_proof.cpp') diff --git a/src/proof/bitvector_proof.cpp b/src/proof/bitvector_proof.cpp index 90c0c9b30..b42a464ab 100644 --- a/src/proof/bitvector_proof.cpp +++ b/src/proof/bitvector_proof.cpp @@ -221,6 +221,14 @@ void BitVectorProof::printOwnedTerm(Expr term, } } +void BitVectorProof::printEmptyClauseProof(std::ostream& os, + std::ostream& paren) +{ + Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER, + "the BV theory should only be proving bottom directly in the eager " + "bitblasting mode"); +} + void BitVectorProof::printBitOf(Expr term, std::ostream& os, const ProofLetMap& map) -- cgit v1.2.3