mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
Bugfix for QF_FP default tactic.
This commit is contained in:
parent
fde873ac09
commit
5ae2dd9c74
|
@ -45,7 +45,7 @@ struct has_fp_to_real_predicate {
|
|||
void operator()(app * n) {
|
||||
sort * s = get_sort(n);
|
||||
if (au.is_real(s) && n->get_family_id() == fu.get_family_id() &&
|
||||
is_app(n) && to_app(n)->get_kind() == OP_FPA_TO_REAL)
|
||||
is_app(n) && to_app(n)->get_decl_kind() == OP_FPA_TO_REAL)
|
||||
throw found();
|
||||
}
|
||||
};
|
||||
|
|
Loading…
Reference in a new issue