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/bitblaster_template.h | |
| parent | 0b1e8fb1f4676a950f017319d76019876a39cffc (diff) | |
Fix memory issues in bitvector theory, which is now valgrind-clean (mostly resolves bug #594).
Diffstat (limited to 'src/theory/bv/bitblaster_template.h')
| -rw-r--r-- | src/theory/bv/bitblaster_template.h | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/theory/bv/bitblaster_template.h b/src/theory/bv/bitblaster_template.h index ea31e3821..0ff12da95 100644 --- a/src/theory/bv/bitblaster_template.h +++ b/src/theory/bv/bitblaster_template.h @@ -143,8 +143,9 @@ class TLazyBitblaster : public TBitblaster<Node> { prop::NullRegistrar* d_nullRegistrar; context::Context* d_nullContext; // sat solver used for bitblasting and associated CnfStream - prop::BVSatSolverInterface* d_satSolver; - prop::CnfStream* d_cnfStream; + prop::BVSatSolverInterface* d_satSolver; + prop::BVSatSolverInterface::Notify* d_satSolverNotify; + prop::CnfStream* d_cnfStream; AssertionList* d_assertedAtoms; /**< context dependent list storing the atoms currently asserted by the DPLL SAT solver. */ |