Mostly resolves bug #561 memory leaks, and more.

1 files changed, 7 insertions, 1 deletions

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();