Add support for const array in all logics as per issue #7383

Z3Prover · Sep 19, 2024 · 8349ee0 · 8349ee0
1 parent 4896edf
commit 8349ee0
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/ast/array_decl_plugin.cpp b/src/ast/array_decl_plugin.cpp
@@ -577,9 +577,9 @@ void array_decl_plugin::get_sort_names(svector<builtin_name>& sort_names, symbol
 void array_decl_plugin::get_op_names(svector<builtin_name>& op_names, symbol const & logic) {
     op_names.push_back(builtin_name("store",OP_STORE));
     op_names.push_back(builtin_name("select",OP_SELECT));
+    op_names.push_back(builtin_name("const",OP_CONST_ARRAY)); // github issue #7383
     if (logic == symbol::null || logic == symbol("HORN") || logic == symbol("ALL")) {
         // none of the SMT2 logics support these extensions
-        op_names.push_back(builtin_name("const",OP_CONST_ARRAY));
         op_names.push_back(builtin_name("map",OP_ARRAY_MAP));
         op_names.push_back(builtin_name("default",OP_ARRAY_DEFAULT));
         op_names.push_back(builtin_name("union",OP_SET_UNION));