From abd599f48ef74f2acd4324abbc2610eac9338ebc Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Thu, 17 Aug 2017 19:29:37 +0100
Subject: [PATCH] Fixed ref-counting bug in smt_model_checker. Fixes #1212.

---
 src/smt/smt_model_checker.cpp | 11 ++++++++---
 src/smt/smt_model_checker.h   |  2 +-
 2 files changed, 9 insertions(+), 4 deletions(-)

diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp
index 23e2589f9..875e7adf2 100644
--- a/src/smt/smt_model_checker.cpp
+++ b/src/smt/smt_model_checker.cpp
@@ -40,7 +40,7 @@ namespace smt {
         m_max_cexs(1),
         m_iteration_idx(0),
         m_curr_model(0),
-        m_new_instances_bindings(m) {
+        m_pinned_exprs(m) {
     }
 
     model_checker::~model_checker() {
@@ -200,8 +200,12 @@ namespace smt {
     }
 
     void model_checker::add_instance(quantifier* q, expr_ref_vector const& bindings, unsigned max_generation) {
+        SASSERT(q->get_num_decls() == bindings.size());
+
         for (unsigned i = 0; i < bindings.size(); i++)
-            m_new_instances_bindings.push_back(bindings[i]);
+            m_pinned_exprs.push_back(bindings[i]);
+        m_pinned_exprs.push_back(q);
+
         void * mem = m_new_instances_region.allocate(instance::get_obj_size(q->get_num_decls()));
         instance * new_inst = new (mem) instance(q, bindings.c_ptr(), max_generation);
         m_new_instances.push_back(new_inst);
@@ -469,8 +473,9 @@ namespace smt {
     }
 
     void model_checker::reset_new_instances() {
-        m_new_instances_region.reset();
+        m_pinned_exprs.reset();
         m_new_instances.reset();
+        m_new_instances_region.reset();
     }
 
     void model_checker::reset() {
diff --git a/src/smt/smt_model_checker.h b/src/smt/smt_model_checker.h
index 4a9c28aba..778f913c3 100644
--- a/src/smt/smt_model_checker.h
+++ b/src/smt/smt_model_checker.h
@@ -73,8 +73,8 @@ namespace smt {
         };
 
         region                                     m_new_instances_region;
-        expr_ref_vector                            m_new_instances_bindings;
         ptr_vector<instance>                       m_new_instances;
+        expr_ref_vector                            m_pinned_exprs;
         bool add_instance(quantifier * q, model * cex, expr_ref_vector & sks, bool use_inv);
         void reset_new_instances();
         void assert_new_instances();