mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 02:15:19 +00:00
FPA probe bugfix
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
parent
b968eb2b8c
commit
4c8bbad8d6
|
@ -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();
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue