[SMT-COMP] QF_FP, min and zeros

[Martin Nyx Brain]

On Tue, 2017-04-25 at 18:08 +0200, François Bobot wrote:
> 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.

I've found that it's not the numerical part that is the challenge but
the edge cases around overflow, underflow, signs of zeros, etc.
Thankfully these can be enumerated and I think between all of the test
case we have, we are getting there.

Cheers,
 - Martin