From b77e3872651555e4941958c5d07df3647ec5a14f Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 4 Dec 2015 15:26:53 -0800
Subject: [PATCH] value
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/ast/seq_decl_plugin.cpp | 3 +--
1 file changed, 1 insertion(+), 2 deletions(-)
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) {