From 7d3af70a6320c30d43e8785b71b79a3cd664bdb4 Mon Sep 17 00:00:00 2001
From: Nuno Lopes <nlopes@microsoft.com>
Date: Fri, 19 Feb 2016 11:08:01 +0000
Subject: [PATCH] ctx-simplify: fix mem leak of simplifier

---
 src/tactic/core/ctx_simplify_tactic.cpp | 11 +++++++----
 src/tactic/core/ctx_simplify_tactic.h   |  5 +----
 2 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/src/tactic/core/ctx_simplify_tactic.cpp b/src/tactic/core/ctx_simplify_tactic.cpp
index f0e0b0059..3bcadb03d 100644
--- a/src/tactic/core/ctx_simplify_tactic.cpp
+++ b/src/tactic/core/ctx_simplify_tactic.cpp
@@ -180,6 +180,7 @@ struct ctx_simplify_tactic::imp {
         pop(scope_level());
         SASSERT(scope_level() == 0);
         restore_cache(0);
+        dealloc(m_simp);
         DEBUG_CODE({
             for (unsigned i = 0; i < m_cache.size(); i++) {
                 CTRACE("ctx_simplify_tactic_bug", m_cache[i].m_from, 
@@ -572,13 +573,15 @@ struct ctx_simplify_tactic::imp {
 
 ctx_simplify_tactic::ctx_simplify_tactic(ast_manager & m, simplifier* simp, params_ref const & p):
     m_imp(alloc(imp, m, simp, p)),
-    m_params(p),
-    m_simp(simp) {
+    m_params(p) {
+}
+
+tactic * ctx_simplify_tactic::translate(ast_manager & m) {
+    return alloc(ctx_simplify_tactic, m, m_imp->m_simp->translate(m), m_params);
 }
 
 ctx_simplify_tactic::~ctx_simplify_tactic() {
     dealloc(m_imp);
-    dealloc(m_simp);
 }
 
 void ctx_simplify_tactic::updt_params(params_ref const & p) {
@@ -606,7 +609,7 @@ void ctx_simplify_tactic::operator()(goal_ref const & in,
 
 void ctx_simplify_tactic::cleanup() {
     ast_manager & m   = m_imp->m;
-    imp * d = alloc(imp, m, m_simp->translate(m), m_params);
+    imp * d = alloc(imp, m, m_imp->m_simp->translate(m), m_params);
     std::swap(d, m_imp);    
     dealloc(d);
 }
diff --git a/src/tactic/core/ctx_simplify_tactic.h b/src/tactic/core/ctx_simplify_tactic.h
index 3c95ca554..5689a64b7 100644
--- a/src/tactic/core/ctx_simplify_tactic.h
+++ b/src/tactic/core/ctx_simplify_tactic.h
@@ -42,13 +42,10 @@ protected:
     struct      imp;
     imp *       m_imp;
     params_ref  m_params;
-    simplifier* m_simp;
 public:
     ctx_simplify_tactic(ast_manager & m, simplifier* simp, params_ref const & p = params_ref());
 
-    virtual tactic * translate(ast_manager & m) {
-        return alloc(ctx_simplify_tactic, m, m_simp->translate(m), m_params);
-    }
+    virtual tactic * translate(ast_manager & m);
 
     virtual ~ctx_simplify_tactic();