[SMT-LIB] [Smtcomp-discussion] FP demo track at SMT-COMP

[Schanda Florian]

> On Wed, 2015-06-10 at 17:26 +0200, Alberto Griggio wrote:
> > Is it too late to ask for a change in the FP standard? Fixing one
> return
> > value for e.g. (fp.min -0 +0) would make life simpler without losing
> > much IMHO, given that the underspecified semantics can still be
> encoded
> > if someone really wants that. What do people think?
> 
> Fixing one return value while existing IEEE-compliant implementations
> return different values would be actively harmful in my opinion.

Yes, to add my "industry" voice to this, please keep it as is, that is
unspecified. ;) This leaves it up to the tool vendor to specify it, if
they happen to know.

For example - if I remember right the intel manuals also do not specify
what the hardware does. Although, if I remember right, it seems to behave
consistently in that it always returns the second (or first?) argument.

But fp.min returning -0 and fp.max returning +0 seems an equally likely
implementation choice.

In fact, I will add some benchmarks to my own testsuite to make sure this
behaviour exists. 

It might all sound a bit silly, but it would be easy enough to construct
a program that exploits this behaviour (convert floats to array of bytes)
and we would get unsound proofs because of it!

	Florian