From f7e5977b9e1edf9f15d2d078e5991ecd61c25a73 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Mon, 25 Dec 2017 22:48:37 +0100
Subject: [PATCH] fix memleak

---
 src/ast/recfun_decl_plugin.cpp | 6 ++++++
 src/ast/recfun_decl_plugin.h   | 1 +
 src/smt/theory_recfun.cpp      | 2 +-
 3 files changed, 8 insertions(+), 1 deletion(-)

diff --git a/src/ast/recfun_decl_plugin.cpp b/src/ast/recfun_decl_plugin.cpp
index 3ebd888c7..f4b237f9a 100644
--- a/src/ast/recfun_decl_plugin.cpp
+++ b/src/ast/recfun_decl_plugin.cpp
@@ -342,6 +342,12 @@ namespace recfun {
         m_plugin = dynamic_cast<decl::plugin*>(m.get_plugin(m_family_id));
     }
 
+    util::~util() {
+        for (auto & kv : m_dlimit_map) {
+            dealloc(kv.m_value);
+        }
+    }
+
     def * util::decl_fun(symbol const& name, unsigned n, sort *const * domain, sort * range) {
         return alloc(def, m(), m_family_id, name, n, domain, range);
     }
diff --git a/src/ast/recfun_decl_plugin.h b/src/ast/recfun_decl_plugin.h
index 272ab43c4..206b2c951 100644
--- a/src/ast/recfun_decl_plugin.h
+++ b/src/ast/recfun_decl_plugin.h
@@ -233,6 +233,7 @@ namespace recfun {
         void set_definition(promise_def & d, unsigned n_vars, var * const * vars, expr * rhs);
     public:
         util(ast_manager &m, family_id);
+        virtual ~util();
 
         ast_manager & m() { return m_manager; }
         th_rewriter & get_th_rewriter() { return m_th_rw; }
diff --git a/src/smt/theory_recfun.cpp b/src/smt/theory_recfun.cpp
index f9e032c87..3bafaf925 100644
--- a/src/smt/theory_recfun.cpp
+++ b/src/smt/theory_recfun.cpp
@@ -62,7 +62,7 @@ namespace smt {
         for (auto & kv : m_guards) {
             m().dec_ref(kv.m_key);
         }
-        m_guards.reset();   
+        m_guards.reset();
     }
 
     char const * theory_recfun::get_name() const { return "recfun"; }