From: Tim King <taking@cs.nyu.edu>
Date: Wed, 23 Mar 2016 03:45:14 +0000 (-0700)
Subject: Garbage collecting the MinisatEmptyNotify for the EagerBitblaster.
X-Git-Tag: cvc5-1.0.0~6049^2~98
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d9afad0e10fade886a2b3e0076539740786bd6cb;p=cvc5.git

Garbage collecting the MinisatEmptyNotify for the EagerBitblaster.
---

diff --git a/src/theory/bv/bitblaster_template.h b/src/theory/bv/bitblaster_template.h
index 9c6c4af9b..10e30c5c7 100644
--- a/src/theory/bv/bitblaster_template.h
+++ b/src/theory/bv/bitblaster_template.h
@@ -266,6 +266,8 @@ class EagerBitblaster : public TBitblaster<Node> {
   TNodeSet d_bbAtoms;
   TNodeSet d_variables;
 
+  MinisatEmptyNotify d_notify;
+
   Node getModelFromSatSolver(TNode a, bool fullModel);
   bool isSharedTerm(TNode node);
 
diff --git a/src/theory/bv/eager_bitblaster.cpp b/src/theory/bv/eager_bitblaster.cpp
index dd561667c..77e75091d 100644
--- a/src/theory/bv/eager_bitblaster.cpp
+++ b/src/theory/bv/eager_bitblaster.cpp
@@ -36,9 +36,14 @@ void BitblastingRegistrar::preRegister(Node n) {
 
 EagerBitblaster::EagerBitblaster(TheoryBV* theory_bv)
   : TBitblaster<Node>()
+  , d_satSolver(NULL)
+  , d_bitblastingRegistrar(NULL)
+  , d_nullContext(NULL)
+  , d_cnfStream(NULL)
   , d_bv(theory_bv)
   , d_bbAtoms()
   , d_variables()
+  , d_notify()
 {
   d_bitblastingRegistrar = new BitblastingRegistrar(this);
   d_nullContext = new context::Context();
@@ -50,8 +55,7 @@ EagerBitblaster::EagerBitblaster(TheoryBV* theory_bv)
       d_satSolver, d_bitblastingRegistrar, d_nullContext, options::proof(),
       "EagerBitblaster");
 
-  MinisatEmptyNotify* notify = new MinisatEmptyNotify();
-  d_satSolver->setNotify(notify);
+  d_satSolver->setNotify(&d_notify);
   d_bvp = NULL;
 }