[SMT-COMP] QF_FP, min and zeros

[François Bobot]

Le 25/04/2017 à 15:12, Christoph Wintersteiger a écrit :
> Yeah, FMA is a perpetual mystery ��
>
> There is 1 open bug report for Z3's FMA, so it may well be that there's an actual bug there as
> well. But, I haven't had access to a machine that supports FMA for a while now, so I wasn't able
> to check it against the hardware yet (the SMT-LIB benchmarks were generated via an Itanium with
> actual FMA instruction).
>

We are checking the examples by computing in rationals and doing the rounding only at the end. So we 
don't need any particular hardware.

-- 
François