mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 02:45:51 +00:00
Code Activity

fix #5146

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-04-02 11:48:44 -07:00
parent 1fc9a7ba84
commit cebf83c460
2 changed files with 12 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/cmd_context/cmd_context.cpp
View file

@ -1082,7 +1082,7 @@ void cmd_context::mk_app(symbol const & s, unsigned num_args, expr * const * arg
tout << "s: " << s << "\n";
tout << "body:\n" << mk_ismt2_pp(_t, m()) << "\n";
tout << "args:\n"; for (unsigned i = 0; i < num_args; i++) tout << mk_ismt2_pp(args[i], m()) << "\n" << mk_pp(args[i]->get_sort(), m()) << "\n";);
var_subst subst(m());
var_subst subst(m(), false);
scoped_rlimit no_limit(m().limit(), 0);
result = subst(_t, coerced_args);
if (well_sorted_check_enabled() && !is_well_sorted(m(), result))

12
src/parsers/smt2/smt2parser.cpp
View file

@ -2276,7 +2276,17 @@ namespace smt2 {
sort* const* sorts = sort_stack().c_ptr() + sort_spos;
expr* t = expr_stack().back();
if (is_fun) {
m_ctx.insert(id, num_vars, sorts, t);
expr_ref _t(t, m());
if (num_vars > 1) {
// variable ordering in macros follow non-standard ordering
// we have to reverse the ordering used by the parser.
var_subst sub(m(), true);
expr_ref_vector vars(m());
for (unsigned i = 0; i < num_vars; ++i)
vars.push_back(m().mk_var(i, sorts[i]));
_t = sub(_t, vars);
}
m_ctx.insert(id, num_vars, sorts, _t);
}
else {
m_ctx.model_add(id, num_vars, sorts, t);