mirror of
https://github.com/Z3Prover/z3
synced 2025-04-13 20:38:43 +00:00
value
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
a8e366aa24
commit
b77e387265
|
@ -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) {
|
||||
|
|
Loading…
Reference in a new issue