diff --git a/src/ast/array_decl_plugin.cpp b/src/ast/array_decl_plugin.cpp index bd9d954c774..c013036f463 100644 --- 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& sort_names, symbol void array_decl_plugin::get_op_names(svector& 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));