diff options
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/bv/bitblast/eager_bitblaster.cpp | 13 | ||||
-rw-r--r-- | src/theory/bv/bitblast/lazy_bitblaster.cpp | 16 |
2 files changed, 16 insertions, 13 deletions
diff --git a/src/theory/bv/bitblast/eager_bitblaster.cpp b/src/theory/bv/bitblast/eager_bitblaster.cpp index c4e3513bf..bddde4cb7 100644 --- a/src/theory/bv/bitblast/eager_bitblaster.cpp +++ b/src/theory/bv/bitblast/eager_bitblaster.cpp @@ -63,12 +63,13 @@ EagerBitblaster::EagerBitblaster(TheoryBV* theory_bv, context::Context* c) default: Unreachable() << "Unknown SAT solver type"; } d_satSolver.reset(solver); - d_cnfStream.reset( - new prop::TseitinCnfStream(d_satSolver.get(), - d_bitblastingRegistrar.get(), - d_nullContext.get(), - options::proof(), - "EagerBitblaster")); + ResourceManager* rm = NodeManager::currentResourceManager(); + d_cnfStream.reset(new prop::TseitinCnfStream(d_satSolver.get(), + d_bitblastingRegistrar.get(), + d_nullContext.get(), + rm, + options::proof(), + "EagerBitblaster")); } EagerBitblaster::~EagerBitblaster() {} diff --git a/src/theory/bv/bitblast/lazy_bitblaster.cpp b/src/theory/bv/bitblast/lazy_bitblaster.cpp index 06afa126d..463ffae79 100644 --- a/src/theory/bv/bitblast/lazy_bitblaster.cpp +++ b/src/theory/bv/bitblast/lazy_bitblaster.cpp @@ -79,12 +79,13 @@ TLazyBitblaster::TLazyBitblaster(context::Context* c, d_satSolver.reset( prop::SatSolverFactory::createMinisat(c, smtStatisticsRegistry(), name)); - d_cnfStream.reset( - new prop::TseitinCnfStream(d_satSolver.get(), - d_nullRegistrar.get(), - d_nullContext.get(), - options::proof(), - "LazyBitblaster")); + ResourceManager* rm = NodeManager::currentResourceManager(); + d_cnfStream.reset(new prop::TseitinCnfStream(d_satSolver.get(), + d_nullRegistrar.get(), + d_nullContext.get(), + rm, + options::proof(), + "LazyBitblaster")); d_satSolverNotify.reset( d_emptyNotify @@ -578,8 +579,9 @@ void TLazyBitblaster::clearSolver() { // recreate sat solver d_satSolver.reset( prop::SatSolverFactory::createMinisat(d_ctx, smtStatisticsRegistry())); + ResourceManager* rm = NodeManager::currentResourceManager(); d_cnfStream.reset(new prop::TseitinCnfStream( - d_satSolver.get(), d_nullRegistrar.get(), d_nullContext.get())); + d_satSolver.get(), d_nullRegistrar.get(), d_nullContext.get(), rm)); d_satSolverNotify.reset( d_emptyNotify ? (prop::BVSatSolverNotify*)new MinisatEmptyNotify() |