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

[Tjark Weber]

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. It is
foreseeable then that users will use fp.min to model IEEE min, that
some (if not most) will be unaware of the subtle semantic difference,
and that they will ultimately believe they've verified their code when
it may well break on some architectures.

For the competition, I think the best solution by far is to remove
affected benchmarks this year. Are there any other floating-point
operators with underspecified semantics that should be removed as well?

Best,
Tjark