diff options
Diffstat (limited to 'src/theory/bv/bitblast/eager_bitblaster.cpp')
| -rw-r--r-- | src/theory/bv/bitblast/eager_bitblaster.cpp | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/src/theory/bv/bitblast/eager_bitblaster.cpp b/src/theory/bv/bitblast/eager_bitblaster.cpp index 01437cb64..33d5a1c80 100644 --- a/src/theory/bv/bitblast/eager_bitblaster.cpp +++ b/src/theory/bv/bitblast/eager_bitblaster.cpp @@ -19,7 +19,6 @@ #include "theory/bv/bitblast/eager_bitblaster.h" #include "options/bv_options.h" -#include "proof/bitvector_proof.h" #include "prop/cnf_stream.h" #include "prop/sat_solver_factory.h" #include "smt/smt_statistics_registry.h" @@ -37,6 +36,7 @@ EagerBitblaster::EagerBitblaster(TheoryBV* theory_bv, context::Context* c) d_satSolver(), d_bitblastingRegistrar(new BitblastingRegistrar(this)), d_cnfStream(), + d_bvp(nullptr), d_bv(theory_bv), d_bbAtoms(), d_variables(), @@ -268,10 +268,11 @@ bool EagerBitblaster::collectModelInfo(TheoryModel* m, bool fullModel) return true; } -void EagerBitblaster::setProofLog(BitVectorProof* bvp) { - d_bvp = bvp; - d_satSolver->setProofLog(bvp); - bvp->initCnfProof(d_cnfStream.get(), d_nullContext.get()); +void EagerBitblaster::setResolutionProofLog( + proof::ResolutionBitVectorProof* bvp) +{ + THEORY_PROOF(d_bvp = bvp; d_satSolver->setProofLog(bvp); + bvp->initCnfProof(d_cnfStream.get(), d_nullContext.get());) } bool EagerBitblaster::isSharedTerm(TNode node) { |