diff --git a/src/tactic/fpa/qffp_tactic.cpp b/src/tactic/fpa/qffp_tactic.cpp index 3bee224b3..fbce1668e 100644 --- a/src/tactic/fpa/qffp_tactic.cpp +++ b/src/tactic/fpa/qffp_tactic.cpp @@ -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(); } };