diff options
Diffstat (limited to 'src/parser/smt2/smt2.cpp')
| -rw-r--r-- | src/parser/smt2/smt2.cpp | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index ef13d379e..94a273193 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -171,7 +171,9 @@ void Smt2::addStringOperators() { } addOperator(kind::STRING_PREFIX, "str.prefixof" ); addOperator(kind::STRING_SUFFIX, "str.suffixof" ); + addOperator(kind::STRING_FROM_CODE, "str.from_code"); addOperator(kind::STRING_IS_DIGIT, "str.is_digit" ); + // at the moment, we only use this syntax for smt2.6.1 if (getLanguage() == language::input::LANG_SMTLIB_V2_6_1 || getLanguage() == language::input::LANG_SYGUS_V2) @@ -180,7 +182,7 @@ void Smt2::addStringOperators() { addOperator(kind::STRING_STOI, "str.to_int"); addOperator(kind::STRING_IN_REGEXP, "str.in_re"); addOperator(kind::STRING_TO_REGEXP, "str.to_re"); - addOperator(kind::STRING_CODE, "str.to_code"); + addOperator(kind::STRING_TO_CODE, "str.to_code"); addOperator(kind::STRING_STRREPLALL, "str.replace_all"); } else @@ -189,7 +191,7 @@ void Smt2::addStringOperators() { addOperator(kind::STRING_STOI, "str.to.int"); addOperator(kind::STRING_IN_REGEXP, "str.in.re"); addOperator(kind::STRING_TO_REGEXP, "str.to.re"); - addOperator(kind::STRING_CODE, "str.code"); + addOperator(kind::STRING_TO_CODE, "str.code"); addOperator(kind::STRING_STRREPLALL, "str.replaceall"); } |