mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

fix #2129

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-02-16 09:38:47 -08:00
parent f84de9400e
commit 4f223542ac
1 changed files with 10 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
src/model/model_evaluator.cpp
View file

@ -217,13 +217,18 @@ struct evaluator_cfg : public default_rewriter_cfg {
return BR_DONE; return BR_DONE;
} }
if (get_macro(g, def, q, def_pr)) { if (get_macro(g, def, q, def_pr)) {
sort_ref_vector vars(m); sort_ref_vector sorts(m);
expr_ref_vector vars(m);
svector<symbol> var_names; svector<symbol> var_names;
for (unsigned i = 0; i < g->get_arity(); ++i) { unsigned sz = g->get_arity();
var_names.push_back(symbol(i)); for (unsigned i = 0; i < sz; ++i) {
vars.push_back(g->get_domain(i)); var_names.push_back(symbol(sz - i - 1));
vars.push_back(m.mk_var(sz - i - 1, g->get_domain(i)));
sorts.push_back(g->get_domain(i));
} }
result = m.mk_lambda(vars.size(), vars.c_ptr(), var_names.c_ptr(), def); var_subst subst(m, false);
result = subst(def, sorts.size(), vars.c_ptr());
result = m.mk_lambda(sorts.size(), sorts.c_ptr(), var_names.c_ptr(), result);
model_evaluator ev(m_model, m_params); model_evaluator ev(m_model, m_params);
result = ev(result); result = ev(result);
m_pinned.push_back(result); m_pinned.push_back(result);