mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 04:03:39 +00:00
Code Activity

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

Browse source
This commit is contained in:
Nikolaj Bjorner 2024-09-19 11:44:18 +03:00
parent 4896edfb04
commit 8349ee0069
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/ast/array_decl_plugin.cpp
View file

@ -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) { 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("store",OP_STORE));
op_names.push_back(builtin_name("select",OP_SELECT)); 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")) { if (logic == symbol::null || logic == symbol("HORN") || logic == symbol("ALL")) {
// none of the SMT2 logics support these extensions // 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("map",OP_ARRAY_MAP));
op_names.push_back(builtin_name("default",OP_ARRAY_DEFAULT)); op_names.push_back(builtin_name("default",OP_ARRAY_DEFAULT));
op_names.push_back(builtin_name("union",OP_SET_UNION)); op_names.push_back(builtin_name("union",OP_SET_UNION));