19 files changed, 107 insertions, 41 deletions

diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp
index de44d717e..a16e7f899 100644
--- a/src/options/options_template.cpp
+++ b/src/options/options_template.cpp
@@ -557,6 +557,8 @@ ${all_modules_option_handlers}
 
   Debug("options") << "returning " << nonOptions.size() << " non-option arguments." << std::endl;
 
+  free(extra_argv);
+
   return nonOptions;
 }
 
@@ -573,7 +575,7 @@ std::string Options::suggestCommandLineOptions(const std::string& optionName) th
 
 static const char* smtOptions[] = {
   ${all_modules_smt_options},
-#line 577 "${template}"
+#line 579 "${template}"
   NULL
 };/* smtOptions[] */
 
@@ -595,7 +597,7 @@ SExpr Options::getOptions() const throw() {
 
   ${all_modules_get_options}
 
-#line 599 "${template}"
+#line 601 "${template}"
 
   return SExpr(opts);
 }
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 2a2a60391..cb4a32ee7 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -69,7 +69,9 @@ PropEngine::PropEngine(TheoryEngine* te, DecisionEngine *de, Context* satContext
   d_theoryEngine(te),
   d_decisionEngine(de),
   d_context(satContext),
+  d_theoryProxy(NULL),
   d_satSolver(NULL),
+  d_registrar(NULL),
   d_cnfStream(NULL),
   d_satTimer(*this),
   d_interrupted(false) {
@@ -78,16 +80,17 @@ PropEngine::PropEngine(TheoryEngine* te, DecisionEngine *de, Context* satContext
 
   d_satSolver = SatSolverFactory::createDPLLMinisat(); 
 
-  theory::TheoryRegistrar* registrar = new theory::TheoryRegistrar(d_theoryEngine);
+  d_registrar = new theory::TheoryRegistrar(d_theoryEngine);
   d_cnfStream = new CVC4::prop::TseitinCnfStream
-    (d_satSolver, registrar, 
+    (d_satSolver, d_registrar,
      userContext,
      // fullLitToNode Map = 
      options::threads() > 1 || 
      options::decisionMode() == decision::DECISION_STRATEGY_RELEVANCY
      );
 
-  d_satSolver->initialize(d_context, new TheoryProxy(this, d_theoryEngine, d_decisionEngine, d_context, d_cnfStream));
+  d_theoryProxy = new TheoryProxy(this, d_theoryEngine, d_decisionEngine, d_context, d_cnfStream);
+  d_satSolver->initialize(d_context, d_theoryProxy);
 
   d_decisionEngine->setSatSolver(d_satSolver);
   d_decisionEngine->setCnfStream(d_cnfStream);
@@ -97,7 +100,9 @@ PropEngine::PropEngine(TheoryEngine* te, DecisionEngine *de, Context* satContext
 PropEngine::~PropEngine() {
   Debug("prop") << "Destructing the PropEngine" << endl;
   delete d_cnfStream;
+  delete d_registrar;
   delete d_satSolver;
+  delete d_theoryProxy;
 }
 
 void PropEngine::assertFormula(TNode node) {
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index 39182204c..753890087 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -32,6 +32,10 @@ namespace CVC4 {
 class DecisionEngine;
 class TheoryEngine;
 
+namespace theory {
+  class TheoryRegistrar;
+}/* CVC4::theory namespace */
+
 namespace prop {
 
 class CnfStream;
@@ -132,12 +136,18 @@ class PropEngine {
   /** The context */
   context::Context* d_context;
 
+  /** SAT solver's proxy back to theories; kept around for dtor cleanup */
+  TheoryProxy* d_theoryProxy;
+
   /** The SAT solver proxy */
   DPLLSatSolverInterface* d_satSolver;
 
   /** List of all of the assertions that need to be made */
   std::vector<Node> d_assertionList;
 
+  /** Theory registrar; kept around for destructor cleanup */
+  theory::TheoryRegistrar* d_registrar;
+
   /** The CNF converter in use */
   CnfStream* d_cnfStream;
 
diff --git a/src/prop/registrar.h b/src/prop/registrar.h
index 0cb3accf1..4fe04f062 100644
--- a/src/prop/registrar.h
+++ b/src/prop/registrar.h
@@ -5,7 +5,7 @@
  ** Major contributors: Tim King, Morgan Deters
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
@@ -32,13 +32,11 @@ public:
 
 };/* class Registrar */
 
-class NullRegistrar: public Registrar {
+class NullRegistrar : public Registrar {
 public:
-  void preRegister(Node n) {};
-
-};/* class Registrar */
-
+  void preRegister(Node n) {}
 
+};/* class NullRegistrar */
 
 }/* CVC4::prop namespace */
 }/* CVC4 namespace */
diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h
index f84aecbac..92c81616b 100644
--- a/src/prop/theory_proxy.h
+++ b/src/prop/theory_proxy.h
@@ -139,6 +139,10 @@ inline TheoryProxy::TheoryProxy(PropEngine* propEngine,
   d_queue(context)
 {}
 
+inline TheoryProxy::~TheoryProxy() {
+  /* nothing to do for now */
+}
+
 }/* CVC4::prop namespace */
 
 }/* CVC4 namespace */
diff --git a/src/theory/bv/bitblaster.cpp b/src/theory/bv/bitblaster.cpp
index cbe550f96..552f3b448 100644
--- a/src/theory/bv/bitblaster.cpp
+++ b/src/theory/bv/bitblaster.cpp
@@ -61,10 +61,12 @@ Bitblaster::Bitblaster(context::Context* c, bv::TheoryBV* bv) :
     d_statistics()
   {
     d_satSolver = prop::SatSolverFactory::createMinisat(c);
-    d_cnfStream = new TseitinCnfStream(d_satSolver, new NullRegistrar(), new Context());
+    d_nullRegistrar = new NullRegistrar();
+    d_nullContext = new Context();
+    d_cnfStream = new TseitinCnfStream(d_satSolver, d_nullRegistrar, d_nullContext);
 
-    MinisatNotify* notify = new MinisatNotify(d_cnfStream, bv);
-    d_satSolver->setNotify(notify);
+    d_notify = new MinisatNotify(d_cnfStream, bv);
+    d_satSolver->setNotify(d_notify);
     // initializing the bit-blasting strategies
     initAtomBBStrategies();
     initTermBBStrategies();
@@ -72,7 +74,10 @@ Bitblaster::Bitblaster(context::Context* c, bv::TheoryBV* bv) :
 
 Bitblaster::~Bitblaster() {
   delete d_cnfStream;
+  delete d_nullContext;
+  delete d_nullRegistrar;
   delete d_satSolver;
+  delete d_notify;
 }
 
 
diff --git a/src/theory/bv/bitblaster.h b/src/theory/bv/bitblaster.h
index 2dc82bddc..34345086b 100644
--- a/src/theory/bv/bitblaster.h
+++ b/src/theory/bv/bitblaster.h
@@ -37,6 +37,7 @@
 #include "bitblast_strategies.h"
 
 #include "prop/sat_solver.h"
+#include "prop/registrar.h"
 
 namespace CVC4 {
 
@@ -92,8 +93,11 @@ class Bitblaster {
 
   // sat solver used for bitblasting and associated CnfStream
   theory::OutputChannel*             d_bvOutput;
+  MinisatNotify*                     d_notify;
   prop::BVSatSolverInterface*        d_satSolver;
   prop::CnfStream*                   d_cnfStream;
+  prop::NullRegistrar*               d_nullRegistrar;
+  context::Context*                  d_nullContext;
 
   // caches and mappings
   TermDefMap                   d_termCache;
diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index 098a7819a..509c00bb6 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -545,6 +545,12 @@ FirstOrderModel(qe, c, name){
 
 }
 
+FirstOrderModelFmc::~FirstOrderModelFmc() {
+  for(std::map<Node, Def*>::iterator i = d_models.begin(); i != d_models.end(); ++i) {
+    delete (*i).second;
+  }
+}
+
 Node FirstOrderModelFmc::getUsedRepresentative(Node n, bool strict) {
   //Assert( fm->hasTerm(n) );
   TypeNode tn = n.getType();
diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h
index 2ac9dadcf..63d8ffcce 100644
--- a/src/theory/quantifiers/first_order_model.h
+++ b/src/theory/quantifiers/first_order_model.h
@@ -26,14 +26,16 @@ namespace theory {
 
 class QuantifiersEngine;
 
-namespace quantifiers{
+namespace quantifiers {
 
 class TermDb;
 
 class FirstOrderModelIG;
+
 namespace fmcheck {
   class FirstOrderModelFmc;
-}
+}/* CVC4::theory::quantifiers::fmcheck namespace */
+
 class FirstOrderModelQInt;
 
 struct IsStarAttributeId {};
@@ -69,7 +71,7 @@ public: //for Theory Quantifiers:
   virtual void processInitializeQuantifier( Node q ) {}
 public:
   FirstOrderModel(QuantifiersEngine * qe, context::Context* c, std::string name );
-  virtual ~FirstOrderModel(){}
+  virtual ~FirstOrderModel() {}
   virtual FirstOrderModelIG * asFirstOrderModelIG() { return NULL; }
   virtual fmcheck::FirstOrderModelFmc * asFirstOrderModelFmc() { return NULL; }
   virtual FirstOrderModelQInt * asFirstOrderModelQInt() { return NULL; }
@@ -134,7 +136,7 @@ private:
   void clearEvalFailed( int index );
   std::map< Node, bool > d_eval_failed;
   std::map< int, std::vector< Node > > d_eval_failed_lits;
-};
+};/* class FirstOrderModelIG */
 
 
 namespace fmcheck {
@@ -156,6 +158,7 @@ private:
   void processInitializeModelForTerm(Node n);
 public:
   FirstOrderModelFmc(QuantifiersEngine * qe, context::Context* c, std::string name);
+  virtual ~FirstOrderModelFmc();
   FirstOrderModelFmc * asFirstOrderModelFmc() { return this; }
   // initialize the model
   void processInitialize( bool ispre );
@@ -169,9 +172,9 @@ public:
   bool isInterval(Node n);
   Node getInterval( Node lb, Node ub );
   bool isInRange( Node v, Node i );
-};
+};/* class FirstOrderModelFmc */
 
-}
+}/* CVC4::theory::quantifiers::fmcheck namespace */
 
 
 class QIntDef;
@@ -215,7 +218,7 @@ public:
   unsigned getOrderedNumVars( Node q );
   TypeNode getOrderedVarType( Node q, int i );
   int getOrderedVarNumToVarNum( Node q, int i );
-};
+};/* class FirstOrderModelQInt */
 
 
 }/* CVC4::theory::quantifiers namespace */
diff --git a/src/theory/quantifiers/full_model_check.h b/src/theory/quantifiers/full_model_check.h
index db5abb01e..372868ad7 100644
--- a/src/theory/quantifiers/full_model_check.h
+++ b/src/theory/quantifiers/full_model_check.h
@@ -5,7 +5,7 @@
  ** Major contributors: Morgan Deters
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef FULL_MODEL_CHECK
-#define FULL_MODEL_CHECK
+#ifndef __CVC4__THEORY__QUANTIFIERS__FULL_MODEL_CHECK_H
+#define __CVC4__THEORY__QUANTIFIERS__FULL_MODEL_CHECK_H
 
 #include "theory/quantifiers/model_builder.h"
 #include "theory/quantifiers/first_order_model.h"
@@ -45,7 +45,7 @@ public:
 
   void collectIndices(Node c, int index, std::vector< int >& indices );
   bool isComplete(FirstOrderModelFmc * m, Node c, int index);
-};
+};/* class EntryTrie */
 
 
 class Def
@@ -79,7 +79,7 @@ public:
   int getGeneralizationIndex( FirstOrderModelFmc * m, std::vector<Node>& inst );
   void simplify( FullModelChecker * mc, FirstOrderModelFmc * m );
   void debugPrint(const char * tr, Node op, FullModelChecker * m);
-};
+};/* class Def */
 
 
 class FullModelChecker : public QModelBuilder
@@ -151,11 +151,11 @@ public:
   Node getCurrentUfModelValue( FirstOrderModelFmc* fm, Node n, std::vector< Node > & args, bool partial );
 
   bool useSimpleModels();
-};
+};/* class FullModelChecker */
 
-}
-}
-}
-}
+}/* CVC4::theory::quantifiers::fmcheck namespace */
+}/* CVC4::theory::quantifiers namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
 
-#endif
+#endif /* __CVC4__THEORY__QUANTIFIERS__FULL_MODEL_CHECK_H */
diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp
index e5705882a..c8a08dad9 100644
--- a/src/theory/quantifiers/instantiation_engine.cpp
+++ b/src/theory/quantifiers/instantiation_engine.cpp
@@ -31,10 +31,15 @@ using namespace CVC4::theory::quantifiers;
 using namespace CVC4::theory::inst;
 
 InstantiationEngine::InstantiationEngine( QuantifiersEngine* qe, bool setIncomplete ) :
-QuantifiersModule( qe ), d_setIncomplete( setIncomplete ), d_ierCounter( 0 ), d_performCheck( false ){
+QuantifiersModule( qe ), d_isup(NULL), d_i_ag(NULL), d_setIncomplete( setIncomplete ), d_ierCounter( 0 ), d_performCheck( false ){
 
 }
 
+InstantiationEngine::~InstantiationEngine() {
+  delete d_i_ag;
+  delete d_isup;
+}
+
 void InstantiationEngine::finishInit(){
   //for UF terms
   if( !options::finiteModelFind() || options::fmfInstEngine() ){
@@ -48,14 +53,14 @@ void InstantiationEngine::finishInit(){
     }else{
       d_isup = NULL;
     }
-    InstStrategyAutoGenTriggers* i_ag = new InstStrategyAutoGenTriggers( d_quantEngine, Trigger::TS_ALL, 3 );
-    i_ag->setGenerateAdditional( true );
-    addInstStrategy( i_ag );
+    d_i_ag = new InstStrategyAutoGenTriggers( d_quantEngine, Trigger::TS_ALL, 3 );
+    d_i_ag->setGenerateAdditional( true );
+    addInstStrategy( d_i_ag );
     //addInstStrategy( new InstStrategyAddFailSplits( this, ie ) );
     if( !options::finiteModelFind() && options::fullSaturateQuant() ){
       addInstStrategy( new InstStrategyFreeVariable( d_quantEngine ) );
     }
-    //d_isup->setPriorityOver( i_ag );
+    //d_isup->setPriorityOver( d_i_ag );
     //d_isup->setPriorityOver( i_agm );
     //i_ag->setPriorityOver( i_agm );
   }
diff --git a/src/theory/quantifiers/instantiation_engine.h b/src/theory/quantifiers/instantiation_engine.h
index 394d53d42..53777d362 100644
--- a/src/theory/quantifiers/instantiation_engine.h
+++ b/src/theory/quantifiers/instantiation_engine.h
@@ -25,6 +25,7 @@ namespace theory {
 namespace quantifiers {
 
 class InstStrategyUserPatterns;
+class InstStrategyAutoGenTriggers;
 
 /** instantiation strategy class */
 class InstStrategy {
@@ -79,6 +80,8 @@ private:
   std::map< InstStrategy*, bool > d_instStrategyActive;
   /** user-pattern instantiation strategy */
   InstStrategyUserPatterns* d_isup;
+  /** auto gen triggers; only kept for destructor cleanup */
+  InstStrategyAutoGenTriggers* d_i_ag;
   /** is instantiation strategy active */
   bool isActiveStrategy( InstStrategy* is ) {
     return d_instStrategyActive.find( is )!=d_instStrategyActive.end() && d_instStrategyActive[is];
@@ -123,7 +126,7 @@ private:
   void debugSat( int reason );
 public:
   InstantiationEngine( QuantifiersEngine* qe, bool setIncomplete = true );
-  ~InstantiationEngine(){}
+  ~InstantiationEngine();
   /** initialize */
   void finishInit();
 
diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index d7b074acc..3a4879b42 100644
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -53,6 +53,10 @@ QuantifiersModule( qe ){
   }
 }
 
+ModelEngine::~ModelEngine() {
+  delete d_builder;
+}
+
 void ModelEngine::check( Theory::Effort e ){
   if( e==Theory::EFFORT_LAST_CALL && !d_quantEngine->hasAddedLemma() ){
     int addedLemmas = 0;
diff --git a/src/theory/quantifiers/model_engine.h b/src/theory/quantifiers/model_engine.h
index 3b34f7504..79bdcd19b 100644
--- a/src/theory/quantifiers/model_engine.h
+++ b/src/theory/quantifiers/model_engine.h
@@ -48,7 +48,7 @@ private:
   int d_totalLemmas;
 public:
   ModelEngine( context::Context* c, QuantifiersEngine* qe );
-  ~ModelEngine(){}
+  virtual ~ModelEngine();
   //get the builder
   QModelBuilder* getModelBuilder() { return d_builder; }
 public:
diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h
index 8a0d956ac..71e967653 100755
--- a/src/theory/quantifiers/quant_conflict_find.h
+++ b/src/theory/quantifiers/quant_conflict_find.h
@@ -125,6 +125,7 @@ private: //for completing match
   std::vector< int > d_una_eqc_count;

 public:

   QuantInfo() : d_mg( NULL ) {}

+  ~QuantInfo() { delete d_mg; }

   std::vector< TNode > d_vars;

   std::map< TNode, int > d_var_num;

   std::map< TNode, bool > d_nbeneathQuant;

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index be011cdb6..b79c0da69 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -113,11 +113,20 @@ d_lemmas_produced_c(u){
 }
 
 QuantifiersEngine::~QuantifiersEngine(){
+  delete d_rr_engine;
+  delete d_bint;
   delete d_model_engine;
   delete d_inst_engine;
+  delete d_qcf;
+  delete d_quant_rel;
+  delete d_rel_dom;
   delete d_model;
+  delete d_tr_trie;
   delete d_term_db;
   delete d_eq_query;
+  for(std::map< Node, QuantPhaseReq* >::iterator i = d_phase_reqs.begin(); i != d_phase_reqs.end(); ++i) {
+    delete (*i).second;
+  }
 }
 
 EqualityQueryQuantifiersEngine* QuantifiersEngine::getEqualityQuery() {
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index f207bdb8e..7187a373f 100644
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -27,7 +27,7 @@ using namespace CVC4::kind;
 using namespace CVC4::context;
 using namespace CVC4::theory;
 
-TheoryModel::TheoryModel( context::Context* c, std::string name, bool enableFuncModels) :
+TheoryModel::TheoryModel(context::Context* c, std::string name, bool enableFuncModels) :
   d_substitutions(c, false), d_modelBuilt(c, false), d_enableFuncModels(enableFuncModels)
 {
   d_true = NodeManager::currentNM()->mkConst( true );
@@ -46,6 +46,12 @@ TheoryModel::TheoryModel( context::Context* c, std::string name, bool enableFunc
   d_eeContext->push();
 }
 
+TheoryModel::~TheoryModel() {
+  d_eeContext->pop();
+  delete d_equalityEngine;
+  delete d_eeContext;
+}
+
 void TheoryModel::reset(){
   d_reps.clear();
   d_rep_set.clear();
diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h
index 598db2683..65b09befc 100644
--- a/src/theory/theory_model.h
+++ b/src/theory/theory_model.h
@@ -38,7 +38,7 @@ protected:
   SubstitutionMap d_substitutions;
 public:
   TheoryModel(context::Context* c, std::string name, bool enableFuncModels);
-  virtual ~TheoryModel(){}
+  virtual ~TheoryModel();
 
   /** special local context for our equalityEngine so we can clear it independently of search context */
   context::Context* d_eeContext;
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index b9ca17154..938fc4f67 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -183,6 +183,7 @@ public:
         ++i) {
       delete i->second;
     }
+    delete d_thss;
   }
 
   void setMasterEqualityEngine(eq::EqualityEngine* eq);