From 8349ee006936f8088e2cbba66504bd2c8fc458a4 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 19 Sep 2024 11:44:18 +0300 Subject: [PATCH] Add support for const array in all logics as per issue #7383 --- src/ast/array_decl_plugin.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ast/array_decl_plugin.cpp b/src/ast/array_decl_plugin.cpp index bd9d954c7..c013036f4 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));