From 8248ec879e19fd306ce625a390bc2cf1eea0b1eb Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 28 Nov 2018 15:35:46 -0800
Subject: [PATCH] fix qsat destructor memory allocation #1948

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/qe/qsat.cpp        | 26 +++++++++++++++++++-------
 src/smt/theory_lra.cpp |  3 ---
 2 files changed, 19 insertions(+), 10 deletions(-)

diff --git a/src/qe/qsat.cpp b/src/qe/qsat.cpp
index 2ad5b9b96..d1816d807 100644
--- a/src/qe/qsat.cpp
+++ b/src/qe/qsat.cpp
@@ -549,9 +549,15 @@ namespace qe {
         solver& s() { return *m_solver; }
         solver const& s() const { return *m_solver; }
 
-        void reset() {
+        void init() {
             m_solver = mk_smt_solver(m, m_params, symbol::null);
         }
+        void reset_statistics() {
+            init();
+        }
+        void clear() {
+            m_solver = nullptr;
+        }
         void assert_expr(expr* e) {
             m_solver->assert_expr(e);
         }
@@ -696,7 +702,7 @@ namespace qe {
             m_level -= num_scopes;
         }
         
-        void reset() override {
+        void clear() {
             m_st.reset();        
             m_fa.s().collect_statistics(m_st);
             m_ex.s().collect_statistics(m_st);        
@@ -707,9 +713,15 @@ namespace qe {
             m_pred_abs.reset();
             m_vars.reset();
             m_model = nullptr;
-            m_fa.reset();
-            m_ex.reset();        
             m_free_vars.reset();
+            m_fa.clear();
+            m_ex.clear();                    
+        }
+
+        void reset() override {
+            clear();
+            m_fa.init();
+            m_ex.init();                
         }    
         
         /**
@@ -1198,7 +1210,7 @@ namespace qe {
         }
         
         ~qsat() override {
-            reset();
+            clear();
         }
         
         void updt_params(params_ref const & p) override {
@@ -1294,8 +1306,8 @@ namespace qe {
         
         void reset_statistics() override {
             m_stats.reset();
-            m_fa.reset();
-            m_ex.reset();
+            m_fa.reset_statistics();
+            m_ex.reset_statistics();
         }
         
         void cleanup() override {
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 818a20d93..a62c82aeb 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -350,7 +350,6 @@ class theory_lra::imp {
         var = m_solver->add_var(v, true);
         m_theory_var2var_index.setx(v, var, UINT_MAX);
         m_var_index2theory_var.setx(var, v, UINT_MAX);
-        TRACE("arith", tout << v << " internal: " << var << "\n";);
         m_var_trail.push_back(v);
         add_def_constraint(m_solver->add_var_bound(var, lp::GE, rational(c)));
         add_def_constraint(m_solver->add_var_bound(var, lp::LE, rational(c)));
@@ -667,7 +666,6 @@ class theory_lra::imp {
             m_has_int |= is_int(v);
             m_theory_var2var_index.setx(v, result, UINT_MAX);
             m_var_index2theory_var.setx(result, v, UINT_MAX);
-            TRACE("arith", tout << v << " internal: " << result << "\n";);
             m_var_trail.push_back(v);
         }
         return result;
@@ -834,7 +832,6 @@ class theory_lra::imp {
                 SASSERT(!m_left_side.empty());
                 vi = m_solver->add_term(m_left_side);
                 m_theory_var2var_index.setx(v, vi, UINT_MAX);
-                TRACE("arith", tout << v << " internal: " << vi << "\n";);
                 if (m_solver->is_term(vi)) {
                     m_term_index2theory_var.setx(m_solver->adjust_term_index(vi), v, UINT_MAX);
                 }