From fd54408629264c4d321626104464b36551d60a3d Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 17 Mar 2020 13:01:46 -0700
Subject: [PATCH] fix leaks exposed by #3383

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/math/simplex/simplex.h          |  2 ++
 src/math/simplex/simplex_def.h      | 11 +++++++++++
 src/util/small_object_allocator.cpp |  1 +
 3 files changed, 14 insertions(+)

diff --git a/src/math/simplex/simplex.h b/src/math/simplex/simplex.h
index 5c412e356..5e922f488 100644
--- a/src/math/simplex/simplex.h
+++ b/src/math/simplex/simplex.h
@@ -117,6 +117,8 @@ namespace simplex {
             m_bland(false),
             m_blands_rule_threshold(1000) {}
 
+        ~simplex();
+
         typedef typename matrix::row row;
         typedef typename matrix::row_iterator row_iterator;
         typedef typename matrix::col_iterator col_iterator;
diff --git a/src/math/simplex/simplex_def.h b/src/math/simplex/simplex_def.h
index 89af0b3ad..082c1c301 100644
--- a/src/math/simplex/simplex_def.h
+++ b/src/math/simplex/simplex_def.h
@@ -28,6 +28,11 @@ namespace simplex {
     template<typename Ext>
     const typename simplex<Ext>::var_t simplex<Ext>::null_var = UINT_MAX; 
 
+    template<typename Ext>
+    simplex<Ext>::~simplex() {
+        reset();
+    }
+
     template<typename Ext>
     typename simplex<Ext>::row 
     simplex<Ext>::add_row(var_t base_var, unsigned num_vars, var_t const* vars, numeral const* coeffs) {
@@ -314,6 +319,12 @@ namespace simplex {
     void simplex<Ext>::reset() {
         M.reset();
         m_to_patch.reset();
+        for (var_info& v : m_vars) {
+            em.del(v.m_value);
+            em.del(v.m_lower);
+            em.del(v.m_upper);
+            m.del(v.m_base_coeff);
+        }
         m_vars.reset();
         m_row2base.reset();
         m_left_basis.reset();
diff --git a/src/util/small_object_allocator.cpp b/src/util/small_object_allocator.cpp
index 9f15aadaf..b74b094ef 100644
--- a/src/util/small_object_allocator.cpp
+++ b/src/util/small_object_allocator.cpp
@@ -97,6 +97,7 @@ void small_object_allocator::deallocate(size_t size, void * p) {
 void * small_object_allocator::allocate(size_t size) {
     if (size == 0) return nullptr;
 
+
 #if defined(Z3DEBUG) && !defined(_WINDOWS)
     // Valgrind friendly
     return memory::allocate(size);