diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-11-07 17:24:35 -0500 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-11-07 17:37:09 -0500 |
commit | 89ed50fd35e6425ed7f1fa4ca5ec560acee1358e (patch) | |
tree | 5919417452041cc4ee1904e0cf77ba59e7dc9b10 /src/theory/bv/lazy_bitblaster.cpp | |
parent | 0b1e8fb1f4676a950f017319d76019876a39cffc (diff) |
Fix memory issues in bitvector theory, which is now valgrind-clean (mostly resolves bug #594).
Diffstat (limited to 'src/theory/bv/lazy_bitblaster.cpp')
-rw-r--r-- | src/theory/bv/lazy_bitblaster.cpp | 16 |
1 files changed, 10 insertions, 6 deletions
diff --git a/src/theory/bv/lazy_bitblaster.cpp b/src/theory/bv/lazy_bitblaster.cpp index f8927284f..b74506e4d 100644 --- a/src/theory/bv/lazy_bitblaster.cpp +++ b/src/theory/bv/lazy_bitblaster.cpp @@ -51,11 +51,11 @@ TLazyBitblaster::TLazyBitblaster(context::Context* c, bv::TheoryBV* bv, const st d_nullRegistrar, d_nullContext); - prop::BVSatSolverInterface::Notify* notify = d_emptyNotify ? + d_satSolverNotify = d_emptyNotify ? (prop::BVSatSolverInterface::Notify*) new MinisatEmptyNotify() : (prop::BVSatSolverInterface::Notify*) new MinisatNotify(d_cnfStream, bv, this); - d_satSolver->setNotify(notify); + d_satSolver->setNotify(d_satSolverNotify); } void TLazyBitblaster::setAbstraction(AbstractionModule* abs) { @@ -67,6 +67,9 @@ TLazyBitblaster::~TLazyBitblaster() { delete d_nullRegistrar; delete d_nullContext; delete d_satSolver; + delete d_satSolverNotify; + d_assertedAtoms->deleteSelf(); + d_explanations->deleteSelf(); } @@ -475,6 +478,7 @@ void TLazyBitblaster::collectModelInfo(TheoryModel* m, bool fullModel) { void TLazyBitblaster::clearSolver() { Assert (d_ctx->getLevel() == 0); delete d_satSolver; + delete d_satSolverNotify; delete d_cnfStream; d_assertedAtoms->deleteSelf(); d_assertedAtoms = new(true) context::CDList<prop::SatLiteral>(d_ctx); @@ -487,11 +491,11 @@ void TLazyBitblaster::clearSolver() { // recreate sat solver d_satSolver = prop::SatSolverFactory::createMinisat(d_ctx); d_cnfStream = new prop::TseitinCnfStream(d_satSolver, - new prop::NullRegistrar(), - new context::Context()); + d_nullRegistrar, + d_nullContext); - prop::BVSatSolverInterface::Notify* notify = d_emptyNotify ? + d_satSolverNotify = d_emptyNotify ? (prop::BVSatSolverInterface::Notify*) new MinisatEmptyNotify() : (prop::BVSatSolverInterface::Notify*) new MinisatNotify(d_cnfStream, d_bv, this); - d_satSolver->setNotify(notify); + d_satSolver->setNotify(d_satSolverNotify); } |