mirror of
https://github.com/Z3Prover/z3
synced 2025-04-15 13:28:47 +00:00
Fix for arrays with arity > 1 in static_features
This commit is contained in:
parent
83a90a9133
commit
614caaca62
|
@ -321,12 +321,12 @@ void static_features::update_core(expr * e) {
|
||||||
if (m_arrayutil.is_array(e)) {
|
if (m_arrayutil.is_array(e)) {
|
||||||
TRACE("sf_array", tout << mk_ismt2_pp(e, m_manager) << "\n";);
|
TRACE("sf_array", tout << mk_ismt2_pp(e, m_manager) << "\n";);
|
||||||
sort * ty = to_app(e)->get_decl()->get_range();
|
sort * ty = to_app(e)->get_decl()->get_range();
|
||||||
SASSERT(ty->get_num_parameters() == 2);
|
|
||||||
sort * inx_srt = to_sort(ty->get_parameter(0).get_ast());
|
|
||||||
sort * elm_srt = to_sort(ty->get_parameter(1).get_ast());
|
|
||||||
mark_theory(ty->get_family_id());
|
mark_theory(ty->get_family_id());
|
||||||
update_core(inx_srt);
|
unsigned n = ty->get_num_parameters();
|
||||||
update_core(elm_srt);
|
for (unsigned i = 0; i < n; i++) {
|
||||||
|
sort * ds = to_sort(ty->get_parameter(i).get_ast());
|
||||||
|
update_core(ds);
|
||||||
|
}
|
||||||
}
|
}
|
||||||
func_decl * d = to_app(e)->get_decl();
|
func_decl * d = to_app(e)->get_decl();
|
||||||
inc_num_apps(d);
|
inc_num_apps(d);
|
||||||
|
|
Loading…
Reference in a new issue