Adding a missing delete to InstStrategyCegqi destructor.

diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp
index b26f24c6320a09339a528dfc81a32e23041b7554..eff1c0d9b6541c6c1f203aa256b5cdacd0079eee 100644 (file)
--- a/src/theory/quantifiers/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp
@@ -33,10 +33,13 @@ using namespace CVC4::theory::arith;
 
 #define ARITH_INSTANTIATOR_USE_MINUS_DELTA
 
-InstStrategyCbqi::InstStrategyCbqi( QuantifiersEngine * qe ) : QuantifiersModule( qe ), d_added_cbqi_lemma( qe->getUserContext() ){
-
+InstStrategyCbqi::InstStrategyCbqi( QuantifiersEngine * qe )
+  : QuantifiersModule( qe )
+  , d_added_cbqi_lemma( qe->getUserContext() ){
 }
 
+InstStrategyCbqi::~InstStrategyCbqi() throw(){}
+
 bool InstStrategyCbqi::needsCheck( Theory::Effort e ) {
   return e>=Theory::EFFORT_LAST_CALL;
 }
@@ -568,11 +571,16 @@ bool CegqiOutputInstStrategy::addLemma( Node lem ) {
 }
 
 
-InstStrategyCegqi::InstStrategyCegqi( QuantifiersEngine * qe ) : InstStrategyCbqi( qe ) {
+InstStrategyCegqi::InstStrategyCegqi( QuantifiersEngine * qe )
+  : InstStrategyCbqi( qe ) {
   d_out = new CegqiOutputInstStrategy( this );
   d_small_const = NodeManager::currentNM()->mkConst( Rational(1)/Rational(1000000) );
 }
 
+InstStrategyCegqi::~InstStrategyCegqi() throw () {
+  delete d_out;
+}
+
 void InstStrategyCegqi::processResetInstantiationRound( Theory::Effort effort ) {
   d_check_vts_lemma_lc = true;
 }

diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h
index 6619860e0ae4875057f56f680f3765f584bcd731..d14b85111ba176355b4ad324aaba3a22e76446c8 100644 (file)
--- a/src/theory/quantifiers/inst_strategy_cbqi.h
+++ b/src/theory/quantifiers/inst_strategy_cbqi.h
@@ -53,7 +53,7 @@ protected:
   virtual void process( Node q, Theory::Effort effort, int e ) = 0;
 public:
   InstStrategyCbqi( QuantifiersEngine * qe );
-  ~InstStrategyCbqi() throw() {}
+  ~InstStrategyCbqi() throw();
   /** whether to do CBQI for quantifier q */
   bool doCbqi( Node q );
   /** process functions */
@@ -139,7 +139,7 @@ protected:
   void registerCounterexampleLemma( Node q, Node lem );
 public:
   InstStrategyCegqi( QuantifiersEngine * qe );
-  ~InstStrategyCegqi() throw() {}
+  ~InstStrategyCegqi() throw(); 
 
   bool addInstantiation( std::vector< Node >& subs );
   bool isEligibleForInstantiation( Node n );