diff --git a/src/tactic/fpa/qffpa_tactic.cpp b/src/tactic/fpa/qffpa_tactic.cpp index 04ffc281a..f9b7f88a1 100644 --- a/src/tactic/fpa/qffpa_tactic.cpp +++ b/src/tactic/fpa/qffpa_tactic.cpp @@ -57,6 +57,8 @@ struct is_non_qffpa_predicate { return; if (fid == u.get_family_id()) return; + if (is_uninterp_const(n)) + return; throw found(); } @@ -83,6 +85,8 @@ struct is_non_qffpabv_predicate { return; if (fid == fu.get_family_id() || fid == bu.get_family_id()) return; + if (is_uninterp_const(n)) + return; throw found(); }