From 912833f0d95e61bead3b046ae694a86c3458d6cd Mon Sep 17 00:00:00 2001
From: Tim King <taking@google.com>
Date: Mon, 23 Nov 2015 13:28:52 -0800
Subject: [PATCH] Adding a missing delete to InstStrategyCegqi destructor.

---
 src/theory/quantifiers/inst_strategy_cbqi.cpp | 14 +++++++++++---
 src/theory/quantifiers/inst_strategy_cbqi.h   |  4 ++--
 2 files changed, 13 insertions(+), 5 deletions(-)

diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp
index b26f24c63..eff1c0d9b 100644
--- 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 6619860e0..d14b85111 100644
--- 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 );
-- 
2.30.2