From 70a1786061d84db297b86d6db7d5c4a8242fe6f7 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 22 Mar 2020 14:14:45 -0700
Subject: [PATCH] scoping th solver to avoid memory leak during cancellation
 exposed by #3431

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/ast.cpp                     | 1 +
 src/ast/rewriter/rewriter_def.h     | 2 +-
 src/qe/qe.cpp                       | 6 +++---
 src/smt/smt_conflict_resolution.cpp | 5 ++++-
 src/smt/smt_conflict_resolution.h   | 2 +-
 5 files changed, 10 insertions(+), 6 deletions(-)

diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp
index 5ba9504ed..24157d428 100644
--- a/src/ast/ast.cpp
+++ b/src/ast/ast.cpp
@@ -1824,6 +1824,7 @@ ast * ast_manager::register_node_core(ast * n) {
     }
 
     n->m_id = is_decl(n) ? m_decl_id_gen.mk() : m_expr_id_gen.mk();
+
     TRACE("ast", tout << "Object " << n->m_id << " was created.\n";);
     TRACE("mk_var_bug", tout << "mk_ast: " << n->m_id << "\n";);
     // increment reference counters
diff --git a/src/ast/rewriter/rewriter_def.h b/src/ast/rewriter/rewriter_def.h
index c80a0b2ca..fdfb6023f 100644
--- a/src/ast/rewriter/rewriter_def.h
+++ b/src/ast/rewriter/rewriter_def.h
@@ -275,7 +275,7 @@ void rewriter_tpl<Config>::process_app(app * t, frame & fr) {
 
         unsigned new_num_args   = result_stack().size() - fr.m_spos;
         expr * const * new_args = result_stack().c_ptr() + fr.m_spos;
-        app * new_t;
+        app_ref new_t(m());
         if (ProofGen) {
             elim_reflex_prs(fr.m_spos);
             unsigned num_prs    = result_pr_stack().size() - fr.m_spos;
diff --git a/src/qe/qe.cpp b/src/qe/qe.cpp
index d40cc1586..320d1c474 100644
--- a/src/qe/qe.cpp
+++ b/src/qe/qe.cpp
@@ -2152,12 +2152,12 @@ namespace qe {
             
             expr_ref fml0(fml, m);
             
-            quant_elim_plugin* th;
+            scoped_ptr<quant_elim_plugin> th;
             pop_context(th);                      
             
             th->check(num_vars, vars, m_assumption, fml, get_first, free_vars, defs);
             
-            push_context(th);
+            push_context(th.detach());
             TRACE("qe", 
                   for (unsigned i = 0; i < num_vars; ++i) {
                       tout << mk_ismt2_pp(vars[i], m) << " ";
@@ -2175,7 +2175,7 @@ namespace qe {
             return l_undef;
         }
 
-        void pop_context(quant_elim_plugin*& th) {
+        void pop_context(scoped_ptr<quant_elim_plugin>& th) {
             if (m_plugins.empty()) {
                 th = alloc(quant_elim_plugin, m, *this, m_fparams);
                 th->add_plugin(mk_bool_plugin(*th));
diff --git a/src/smt/smt_conflict_resolution.cpp b/src/smt/smt_conflict_resolution.cpp
index 43ef8e6d1..6723d26a8 100644
--- a/src/smt/smt_conflict_resolution.cpp
+++ b/src/smt/smt_conflict_resolution.cpp
@@ -51,6 +51,9 @@ namespace smt {
     {
     }
 
+    conflict_resolution::~conflict_resolution() {
+    }
+
     /**
        \brief Mark all enodes in a 'proof' tree branch starting at n
        n -> ... -> root
@@ -1044,7 +1047,7 @@ namespace smt {
             TRACE("proof_gen_bug", tout << "js2pr_cached: #" << js << "\n";);
             return pr;
         }
-        SASSERT(js != 0);
+        SASSERT(js != nullptr);
         TRACE("proof_gen_bug", tout << js << "\n";);
         m_todo_pr.push_back(tp_elem(js));
         return nullptr;
diff --git a/src/smt/smt_conflict_resolution.h b/src/smt/smt_conflict_resolution.h
index e88a8c6ae..0647c629a 100644
--- a/src/smt/smt_conflict_resolution.h
+++ b/src/smt/smt_conflict_resolution.h
@@ -208,7 +208,7 @@ namespace smt {
                             vector<watch_list> & watches
                             );
 
-        virtual ~conflict_resolution() {}
+        virtual ~conflict_resolution();
 
         virtual bool resolve(b_justification conflict, literal not_l);