mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
make extensionality commutative
This commit is contained in:
parent
88b6c4a30d
commit
fa91a644d3
|
@ -326,7 +326,9 @@ func_decl * array_decl_plugin::mk_array_ext(unsigned arity, sort * const * domai
|
|||
}
|
||||
sort * r = to_sort(s->get_parameter(i).get_ast());
|
||||
parameter param(i);
|
||||
return m_manager->mk_func_decl(m_array_ext_sym, arity, domain, r, func_decl_info(m_family_id, OP_ARRAY_EXT, 1, ¶m));
|
||||
func_decl_info info(func_decl_info(m_family_id, OP_ARRAY_EXT, 1, ¶m));
|
||||
info.set_commutative(true);
|
||||
return m_manager->mk_func_decl(m_array_ext_sym, arity, domain, r, info);
|
||||
}
|
||||
|
||||
|
||||
|
|
Loading…
Reference in a new issue