From 334677a7eb4f5a2395cb621dfe24843561e3fca7 Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Thu, 27 Apr 2017 13:58:36 -0400 Subject: [PATCH] fix is_string_term() --- src/ast/seq_decl_plugin.h | 10 ++-------- 1 file changed, 2 insertions(+), 8 deletions(-) diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index 52abb2c45..833455ff4 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -275,18 +275,12 @@ public: bool is_string_term(expr const * n) const { sort * s = get_sort(n); - return is_sort_of(s, m_fid, _STRING_SORT); + return (u.is_seq(s) && u.is_string(s)); } bool is_non_string_sequence(expr const * n) const { - if (is_string_term(n)) - return false; - sort * s = get_sort(n); - if (u.is_seq(s) && !u.is_string(s)) { - return true; - } - return false; + return (u.is_seq(s) && !u.is_string(s)); } MATCH_BINARY(is_concat);