diff --git a/src/ast/array_decl_plugin.cpp b/src/ast/array_decl_plugin.cpp index 22c2184c1..b820b5213 100644 --- a/src/ast/array_decl_plugin.cpp +++ b/src/ast/array_decl_plugin.cpp @@ -568,6 +568,7 @@ func_decl * array_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters void array_decl_plugin::get_sort_names(svector& sort_names, symbol const & logic) { sort_names.push_back(builtin_name(ARRAY_SORT_STR, ARRAY_SORT)); sort_names.push_back(builtin_name("=>", ARRAY_SORT)); + sort_names.push_back(builtin_name("->", ARRAY_SORT)); if (logic == symbol::null || logic == symbol("HORN") || logic == symbol("ALL")) { // this could easily break users even though it is already used in CVC4: sort_names.push_back(builtin_name("Set", _SET_SORT));