mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 09:05:31 +00:00
Code Activity

fix t154 regression

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-03-03 13:10:11 -08:00
parent 8e812ea239
commit e51b5fd99c
2 changed files with 10 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/ast/array_decl_plugin.cpp
View file

@ -127,6 +127,7 @@ func_decl * array_decl_plugin::mk_const(sort * s, unsigned arity, sort * const *
return nullptr;
}
if (!m_manager->compatible_sorts(get_array_range(s), domain[0])) {
SASSERT(false);
m_manager->raise_exception("invalid const array definition, sort mismatch between array range and argument");
return nullptr;
}

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

@ -270,15 +270,21 @@ br_status array_rewriter::mk_map_core(func_decl * f, unsigned num_args, expr * c
values.push_back(to_app(a)->get_arg(num_indices+1));
}
}
ptr_buffer<expr> new_args;
new_args.push_back(m_util.mk_map(f, arrays.size(), arrays.c_ptr()));
if (store_expr) {
ptr_buffer<expr> new_args;
new_args.push_back(m_util.mk_map(f, arrays.size(), arrays.c_ptr()));
new_args.append(num_indices, to_app(args[0])->get_args() + 1);
new_args.push_back(m().mk_app(f, values.size(), values.c_ptr()));
result = m().mk_app(get_fid(), OP_STORE, new_args.size(), new_args.c_ptr());
}
else {
result = m_util.mk_const_array(m().get_sort(args[0]), new_args.back());
expr_ref value(m().mk_app(f, values.size(), values.c_ptr()), m());
sort* s0 = m().get_sort(args[0]);
unsigned sz = get_array_arity(s0);
ptr_vector<sort> domain;
for (unsigned i = 0; i < sz; ++i) domain.push_back(get_array_domain(s0, i));
sort_ref s(m_util.mk_array_sort(sz, domain.c_ptr(), m().get_sort(value)), m());
result = m_util.mk_const_array(s, value);
}
return BR_REWRITE2;
}