From 4f223542acb829a5085b4437dd6803ed2b7335c5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 16 Feb 2019 09:38:47 -0800 Subject: [PATCH] fix #2129 Signed-off-by: Nikolaj Bjorner --- src/model/model_evaluator.cpp | 15 ++++++++++----- 1 file changed, 10 insertions(+), 5 deletions(-) diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp index 53defbc3d..968aca51f 100644 --- a/src/model/model_evaluator.cpp +++ b/src/model/model_evaluator.cpp @@ -217,13 +217,18 @@ struct evaluator_cfg : public default_rewriter_cfg { return BR_DONE; } if (get_macro(g, def, q, def_pr)) { - sort_ref_vector vars(m); + sort_ref_vector sorts(m); + expr_ref_vector vars(m); svector var_names; - for (unsigned i = 0; i < g->get_arity(); ++i) { - var_names.push_back(symbol(i)); - vars.push_back(g->get_domain(i)); + unsigned sz = g->get_arity(); + for (unsigned i = 0; i < sz; ++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); result = ev(result); m_pinned.push_back(result);