diff options
Diffstat (limited to 'src/proof/resolution_bitvector_proof.cpp')
| -rw-r--r-- | src/proof/resolution_bitvector_proof.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/proof/resolution_bitvector_proof.cpp b/src/proof/resolution_bitvector_proof.cpp index f4ced1748..8d4b56d54 100644 --- a/src/proof/resolution_bitvector_proof.cpp +++ b/src/proof/resolution_bitvector_proof.cpp @@ -129,7 +129,7 @@ void ResolutionBitVectorProof::endBVConflict( void ResolutionBitVectorProof::finalizeConflicts(std::vector<Expr>& conflicts) { - if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) + if (options::bitblastMode() == options::BitblastMode::EAGER) { Debug("pf::bv") << "Construct full proof." << std::endl; d_resolutionProof->constructProof(); @@ -513,7 +513,7 @@ void LfscResolutionBitVectorProof::printBBDeclarationAndCnf(std::ostream& os, void LfscResolutionBitVectorProof::printEmptyClauseProof(std::ostream& os, std::ostream& paren) { - Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) + Assert(options::bitblastMode() == options::BitblastMode::EAGER) << "the BV theory should only be proving bottom directly in the eager " "bitblasting mode"; proof::LFSCProofPrinter::printResolutionEmptyClause( |