mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 09:34:08 +00:00
fix #4245
This commit is contained in:
parent
0acaf1ca0f
commit
eda2eb5124
|
@ -345,7 +345,7 @@ namespace datatype {
|
|||
bool is_recognizer0(app const* f) const { return is_app_of(f, fid(), OP_DT_RECOGNISER);}
|
||||
bool is_is(app const * f) const { return is_app_of(f, fid(), OP_DT_IS);}
|
||||
bool is_is(expr const * e) const { return is_app(e) && is_is(to_app(e)); }
|
||||
bool is_recognizer(expr const * f) const { return is_app(f) && is_recognizer0(to_app(f)) || is_is(to_app(f)); }
|
||||
bool is_recognizer(expr const * f) const { return is_app(f) && (is_recognizer0(to_app(f)) || is_is(to_app(f))); }
|
||||
MATCH_UNARY(is_recognizer);
|
||||
bool is_accessor(expr const* e) const { return is_app(e) && is_app_of(to_app(e), fid(), OP_DT_ACCESSOR); }
|
||||
MATCH_UNARY(is_accessor);
|
||||
|
|
Loading…
Reference in a new issue