From fa91a644d3eb90d9a75a0ed35e244f71182932cd Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 13 Aug 2022 07:07:14 -0700 Subject: [PATCH] make extensionality commutative --- src/ast/array_decl_plugin.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/ast/array_decl_plugin.cpp b/src/ast/array_decl_plugin.cpp index b336dd2e5..975eaa07a 100644 --- a/src/ast/array_decl_plugin.cpp +++ b/src/ast/array_decl_plugin.cpp @@ -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); }