From dc752913a611dd15ec27edc8162c14da211757a6 Mon Sep 17 00:00:00 2001
From: "Kirill A. Korinsky" <kirill@korins.ky>
Date: Mon, 26 Aug 2024 20:17:14 +0200
Subject: [PATCH] Avoid broken stack by mbp_arrays

---
 src/model/model_evaluator.cpp |  4 ++++
 src/model/model_evaluator.h   |  1 +
 src/qe/mbp/mbp_arrays.cpp     | 12 ++++++------
 3 files changed, 11 insertions(+), 6 deletions(-)

diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp
index 2446609c6..30dab4690 100644
--- a/src/model/model_evaluator.cpp
+++ b/src/model/model_evaluator.cpp
@@ -745,6 +745,10 @@ struct model_evaluator::imp : public rewriter_tpl<mev::evaluator_cfg> {
     }
 };
 
+model_evaluator::model_evaluator(model_evaluator & mev) {
+    m_imp = mev.m_imp;
+}
+
 model_evaluator::model_evaluator(model_core & md, params_ref const & p) {
     m_imp = alloc(imp, md, p);
 }
diff --git a/src/model/model_evaluator.h b/src/model/model_evaluator.h
index 8efd50688..892f29d09 100644
--- a/src/model/model_evaluator.h
+++ b/src/model/model_evaluator.h
@@ -32,6 +32,7 @@ class model_evaluator {
     struct imp;
     imp *  m_imp;
 public:
+    model_evaluator(model_evaluator & mev);
     model_evaluator(model_core & m, params_ref const & p = params_ref());
     ~model_evaluator();
 
diff --git a/src/qe/mbp/mbp_arrays.cpp b/src/qe/mbp/mbp_arrays.cpp
index bf3ad08ed..84a20a00e 100644
--- a/src/qe/mbp/mbp_arrays.cpp
+++ b/src/qe/mbp/mbp_arrays.cpp
@@ -60,7 +60,7 @@ namespace mbp {
         ast_manager&                m;
         array_util                  m_arr_u;
         model_ref                   M;
-        model_evaluator*            m_mev;
+        model_evaluator*            m_mev = nullptr;
         app_ref                     m_v;    // array var to eliminate
         ast_mark                    m_has_stores_v; // has stores for m_v
         expr_ref                    m_subst_term_v; // subst term for m_v
@@ -499,7 +499,7 @@ namespace mbp {
             model_evaluator mev(mdl);
             mev.set_model_completion(true);
             M = &mdl;
-            m_mev = &mev;
+            flet<model_evaluator*> _mev(m_mev, &mev);
 
             unsigned j = 0;
             for (unsigned i = 0; i < arr_vars.size (); i++) {
@@ -546,7 +546,7 @@ namespace mbp {
         expr_ref_vector             m_pinned;   // to ensure a reference
         expr_ref_vector             m_idx_lits;
         model_ref                   M;
-        model_evaluator*            m_mev;
+        model_evaluator*            m_mev = nullptr;
         th_rewriter                 m_rw;
         ast_mark                    m_arr_test;
         ast_mark                    m_has_stores;
@@ -726,7 +726,7 @@ namespace mbp {
             model_evaluator mev(mdl);
             mev.set_model_completion(true);
             M = &mdl;
-            m_mev = &mev;
+            flet<model_evaluator*> _mev(m_mev, &mev);
             m_reduce_all_selects = reduce_all_selects;
 
             // mark vars to eliminate
@@ -778,7 +778,7 @@ namespace mbp {
         app_ref_vector              m_sel_consts;
         expr_ref_vector             m_idx_lits;
         model_ref                   M;
-        model_evaluator*            m_mev;
+        model_evaluator*            m_mev = nullptr;
         expr_safe_replace           m_sub;
         ast_mark                    m_arr_test;
 
@@ -1010,7 +1010,7 @@ namespace mbp {
             model_evaluator mev(mdl);
             mev.set_model_completion(true);
             M = &mdl;
-            m_mev = &mev;
+            flet<model_evaluator*> _mev(m_mev, &mev);
 
             // mark vars to eliminate
             // alloc empty map from array var to sel terms over it