From d00723e7ea4252c0a2d7e6cf66668f54f41d830d Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Wed, 1 Mar 2017 18:23:48 -0500 Subject: [PATCH] add String name for string sort, SMTLIB2.5 compat --- src/ast/seq_decl_plugin.cpp | 2 ++ 1 file changed, 2 insertions(+) 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)); }