mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 19:05:51 +00:00
Code Activity

#5007 - wrong recognizer function definitions

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-02-09 09:54:24 -08:00
parent 55cb12e233
commit cbb570051c
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/ast/seq_decl_plugin.h
View file

@ -337,8 +337,8 @@ public:
bool is_lt(expr const* n) const { return is_app_of(n, m_fid, OP_STRING_LT); }
bool is_le(expr const* n) const { return is_app_of(n, m_fid, OP_STRING_LE); }
bool is_is_digit(expr const* n) const { return is_app_of(n, m_fid, OP_STRING_IS_DIGIT); }
bool is_from_code(expr const* n) const { return is_app_of(n, m_fid, OP_STRING_TO_CODE); }
bool is_to_code(expr const* n) const { return is_app_of(n, m_fid, OP_STRING_FROM_CODE); }
bool is_from_code(expr const* n) const { return is_app_of(n, m_fid, OP_STRING_FROM_CODE); }
bool is_to_code(expr const* n) const { return is_app_of(n, m_fid, OP_STRING_TO_CODE); }
bool is_string_term(expr const * n) const {
return u.is_string(n->get_sort());