mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-14 06:45:25 +00:00
Code Activity

Avoid broken stack by mbp_arrays

Browse source
This commit is contained in:
Kirill A. Korinsky 2024-08-26 20:17:14 +02:00
parent cff1e9233f
commit dc752913a6
No known key found for this signature in database
GPG key ID: 98D8D9867759226E
3 changed files with 11 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/model/model_evaluator.cpp
View file

@ -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) { model_evaluator::model_evaluator(model_core & md, params_ref const & p) {
m_imp = alloc(imp, md, p); m_imp = alloc(imp, md, p);
} }

1
src/model/model_evaluator.h
View file

@ -32,6 +32,7 @@ class model_evaluator {
struct imp; struct imp;
imp * m_imp; imp * m_imp;
public: public:
model_evaluator(model_evaluator & mev);
model_evaluator(model_core & m, params_ref const & p = params_ref()); model_evaluator(model_core & m, params_ref const & p = params_ref());
~model_evaluator(); ~model_evaluator();

12
src/qe/mbp/mbp_arrays.cpp
View file

@ -60,7 +60,7 @@ namespace mbp {
ast_manager& m; ast_manager& m;
array_util m_arr_u; array_util m_arr_u;
model_ref M; model_ref M;
model_evaluator* m_mev; model_evaluator* m_mev = nullptr;
app_ref m_v; // array var to eliminate app_ref m_v; // array var to eliminate
ast_mark m_has_stores_v; // has stores for m_v ast_mark m_has_stores_v; // has stores for m_v
expr_ref m_subst_term_v; // subst term for m_v expr_ref m_subst_term_v; // subst term for m_v
@ -499,7 +499,7 @@ namespace mbp {
model_evaluator mev(mdl); model_evaluator mev(mdl);
mev.set_model_completion(true); mev.set_model_completion(true);
M = &mdl; M = &mdl;
m_mev = &mev; flet<model_evaluator*> _mev(m_mev, &mev);
unsigned j = 0; unsigned j = 0;
for (unsigned i = 0; i < arr_vars.size (); i++) { 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_pinned; // to ensure a reference
expr_ref_vector m_idx_lits; expr_ref_vector m_idx_lits;
model_ref M; model_ref M;
model_evaluator* m_mev; model_evaluator* m_mev = nullptr;
th_rewriter m_rw; th_rewriter m_rw;
ast_mark m_arr_test; ast_mark m_arr_test;
ast_mark m_has_stores; ast_mark m_has_stores;
@ -726,7 +726,7 @@ namespace mbp {
model_evaluator mev(mdl); model_evaluator mev(mdl);
mev.set_model_completion(true); mev.set_model_completion(true);
M = &mdl; M = &mdl;
m_mev = &mev; flet<model_evaluator*> _mev(m_mev, &mev);
m_reduce_all_selects = reduce_all_selects; m_reduce_all_selects = reduce_all_selects;
// mark vars to eliminate // mark vars to eliminate
@ -778,7 +778,7 @@ namespace mbp {
app_ref_vector m_sel_consts; app_ref_vector m_sel_consts;
expr_ref_vector m_idx_lits; expr_ref_vector m_idx_lits;
model_ref M; model_ref M;
model_evaluator* m_mev; model_evaluator* m_mev = nullptr;
expr_safe_replace m_sub; expr_safe_replace m_sub;
ast_mark m_arr_test; ast_mark m_arr_test;
@ -1010,7 +1010,7 @@ namespace mbp {
model_evaluator mev(mdl); model_evaluator mev(mdl);
mev.set_model_completion(true); mev.set_model_completion(true);
M = &mdl; M = &mdl;
m_mev = &mev; flet<model_evaluator*> _mev(m_mev, &mev);
// mark vars to eliminate // mark vars to eliminate
// alloc empty map from array var to sel terms over it // alloc empty map from array var to sel terms over it