From 4d1acadabbe9f218681bb8c6228dc97dd337cf9b Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 15 Oct 2017 09:56:21 -0700
Subject: [PATCH] fix leaks reported in #1309

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/sat/sat_simplifier.cpp | 5 +----
 src/smt/theory_str.cpp     | 5 +++++
 src/smt/theory_str.h       | 6 ++++--
 3 files changed, 10 insertions(+), 6 deletions(-)

diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp
index 67101b4d8..84534bf3f 100644
--- a/src/sat/sat_simplifier.cpp
+++ b/src/sat/sat_simplifier.cpp
@@ -1311,7 +1311,6 @@ namespace sat {
         clause_use_list & neg_occs = m_use_list.get(neg_l);
         unsigned num_pos = pos_occs.size() + num_bin_pos;
         unsigned num_neg = neg_occs.size() + num_bin_neg;
-        m_elim_counter -= num_pos + num_neg;
 
         TRACE("resolution", tout << v << " num_pos: " << num_pos << " neg_pos: " << num_neg << "\n";);
 
@@ -1352,8 +1351,6 @@ namespace sat {
         collect_clauses(pos_l, m_pos_cls);
         collect_clauses(neg_l, m_neg_cls);
 
-        m_elim_counter -= num_pos * num_neg + before_lits;
-
         TRACE("resolution_detail", tout << "collecting number of after_clauses\n";);
         unsigned before_clauses = num_pos + num_neg;
         unsigned after_clauses  = 0;
@@ -1376,7 +1373,7 @@ namespace sat {
             }
         }
         TRACE("resolution", tout << "found var to eliminate, before: " << before_clauses << " after: " << after_clauses << "\n";);
-
+        m_elim_counter -= num_pos * num_neg + before_lits;
 
         // eliminate variable
         model_converter::entry & mc_entry = s.m_mc.mk(model_converter::ELIM_VAR, v);
diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index 8a141665c..97c8db125 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -315,6 +315,7 @@ namespace smt {
         m_trail.push_back(node);
         if (!cut_var_map.contains(baseNode)) {
             T_cut * varInfo = alloc(T_cut);
+            m_cut_allocs.push_back(varInfo);
             varInfo->level = slevel;
             varInfo->vars[node] = 1;
             cut_var_map.insert(baseNode, std::stack<T_cut*>());
@@ -323,6 +324,7 @@ namespace smt {
         } else {
             if (cut_var_map[baseNode].empty()) {
                 T_cut * varInfo = alloc(T_cut);
+                m_cut_allocs.push_back(varInfo);
                 varInfo->level = slevel;
                 varInfo->vars[node] = 1;
                 cut_var_map[baseNode].push(varInfo);
@@ -330,6 +332,7 @@ namespace smt {
             } else {
                 if (cut_var_map[baseNode].top()->level < slevel) {
                     T_cut * varInfo = alloc(T_cut);
+                    m_cut_allocs.push_back(varInfo);
                     varInfo->level = slevel;
                     cut_vars_map_copy(varInfo->vars, cut_var_map[baseNode].top()->vars);
                     varInfo->vars[node] = 1;
@@ -359,6 +362,7 @@ namespace smt {
 
         if (!cut_var_map.contains(destNode)) {
             T_cut * varInfo = alloc(T_cut);
+            m_cut_allocs.push_back(varInfo);
             varInfo->level = slevel;
             cut_vars_map_copy(varInfo->vars, cut_var_map[srcNode].top()->vars);
             cut_var_map.insert(destNode, std::stack<T_cut*>());
@@ -367,6 +371,7 @@ namespace smt {
         } else {
             if (cut_var_map[destNode].empty() || cut_var_map[destNode].top()->level < slevel) {
                 T_cut * varInfo = alloc(T_cut);
+                m_cut_allocs.push_back(varInfo);
                 varInfo->level = slevel;
                 cut_vars_map_copy(varInfo->vars, cut_var_map[destNode].top()->vars);
                 cut_vars_map_copy(varInfo->vars, cut_var_map[srcNode].top()->vars);
diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h
index 686fcdd57..acac8cad1 100644
--- a/src/smt/theory_str.h
+++ b/src/smt/theory_str.h
@@ -18,9 +18,12 @@
 #define _THEORY_STR_H_
 
 #include "util/trail.h"
+#include "util/union_find.h"
+#include "util/scoped_ptr_vector.h"
 #include "ast/ast_pp.h"
 #include "ast/arith_decl_plugin.h"
 #include "ast/rewriter/th_rewriter.h"
+#include "ast/seq_decl_plugin.h"
 #include "smt/smt_theory.h"
 #include "smt/params/theory_str_params.h"
 #include "smt/proto_model/value_factory.h"
@@ -29,8 +32,6 @@
 #include<stack>
 #include<vector>
 #include<map>
-#include "ast/seq_decl_plugin.h"
-#include "util/union_find.h"
 
 namespace smt {
 
@@ -292,6 +293,7 @@ protected:
     bool avoidLoopCut;
     bool loopDetected;
     obj_map<expr, std::stack<T_cut*> > cut_var_map;
+    scoped_ptr_vector<T_cut> m_cut_allocs;
     expr_ref m_theoryStrOverlapAssumption_term;
 
     obj_hashtable<expr> variable_set;