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 #5229

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-04-30 02:20:51 -07:00
parent 381e502d30
commit c50e6bdbb1
1 changed files with 6 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
src/ast/rewriter/array_rewriter.cpp
View file

@ -336,8 +336,13 @@ br_status array_rewriter::mk_map_core(func_decl * f, unsigned num_args, expr * c
// //
quantifier* lam = nullptr; quantifier* lam = nullptr;
for (unsigned i = 0; i < num_args; ++i) { for (unsigned i = 0; i < num_args; ++i) {
if (is_lambda(args[i])) { if (is_lambda(args[i]))
lam = to_quantifier(args[i]); lam = to_quantifier(args[i]);
else if (m_util.is_const(args[i]))
continue;
else {
lam = nullptr;
break;
} }
} }
if (lam) { if (lam) {
@ -351,15 +356,6 @@ br_status array_rewriter::mk_map_core(func_decl * f, unsigned num_args, expr * c
lam = to_quantifier(a); lam = to_quantifier(a);
args1.push_back(lam->get_expr()); args1.push_back(lam->get_expr());
} }
else {
expr_ref_vector sel(m());
sel.push_back(a);
unsigned n = lam->get_num_decls();
for (unsigned i = 0; i < n; ++i) {
sel.push_back(m().mk_var(n - i - 1, lam->get_decl_sort(i)));
}
args1.push_back(m_util.mk_select(sel.size(), sel.data()));
}
} }
result = m().mk_app(f, args1.size(), args1.data()); result = m().mk_app(f, args1.size(), args1.data());
result = m().update_quantifier(lam, result); result = m().update_quantifier(lam, result);