diff options
Diffstat (limited to 'src/theory/bv/lazy_bitblaster.cpp')
| -rw-r--r-- | src/theory/bv/lazy_bitblaster.cpp | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/src/theory/bv/lazy_bitblaster.cpp b/src/theory/bv/lazy_bitblaster.cpp index 9268e2152..ca21e98c4 100644 --- a/src/theory/bv/lazy_bitblaster.cpp +++ b/src/theory/bv/lazy_bitblaster.cpp @@ -56,13 +56,13 @@ TLazyBitblaster::TLazyBitblaster(context::Context* c, bv::TheoryBV* bv, d_cnfStream = new prop::TseitinCnfStream(d_satSolver, d_nullRegistrar, d_nullContext, - d_bv->globals(), options::proof(), "LazyBitblaster"); d_satSolverNotify = d_emptyNotify ? (prop::BVSatSolverInterface::Notify*) new MinisatEmptyNotify() : - (prop::BVSatSolverInterface::Notify*) new MinisatNotify(d_cnfStream, bv, this); + (prop::BVSatSolverInterface::Notify*) new MinisatNotify(d_cnfStream, bv, + this); d_satSolver->setNotify(d_satSolverNotify); } @@ -526,11 +526,12 @@ void TLazyBitblaster::clearSolver() { d_satSolver = prop::SatSolverFactory::createMinisat( d_ctx, smtStatisticsRegistry()); d_cnfStream = new prop::TseitinCnfStream(d_satSolver, d_nullRegistrar, - d_nullContext, d_bv->globals()); + d_nullContext); d_satSolverNotify = d_emptyNotify ? (prop::BVSatSolverInterface::Notify*) new MinisatEmptyNotify() : - (prop::BVSatSolverInterface::Notify*) new MinisatNotify(d_cnfStream, d_bv, this); + (prop::BVSatSolverInterface::Notify*) new MinisatNotify(d_cnfStream, d_bv, + this); d_satSolver->setNotify(d_satSolverNotify); } |