diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index 65df99c5a..41aa7aa90 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -348,8 +348,7 @@ app* seq_decl_plugin::mk_string(symbol const& s) { } bool seq_decl_plugin::is_value(app* e) const { - // TBD: empty sequence is a value. - return false; + return is_app_of(e, m_family_id, OP_STRING_CONST); } app* seq_util::str::mk_string(symbol const& s) {