[SMT-COMP] QF_FP, min and zeros

François Bobot francois.bobot at cea.fr
Tue Apr 25 12:08:42 EDT 2017

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.


More information about the SMT-COMP mailing list