diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index 059fe9674..90fd3fb22 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -830,6 +830,8 @@ void seq_decl_plugin::get_sort_names(svector & sort_names, symbol init(); sort_names.push_back(builtin_name("Seq", SEQ_SORT)); sort_names.push_back(builtin_name("RegEx", RE_SORT)); + // SMT-LIB 2.5 compatibility + sort_names.push_back(builtin_name("String", _STRING_SORT)); sort_names.push_back(builtin_name("StringSequence", _STRING_SORT)); }