Re: [Smtcomp-discussion] FP demo track at SMT-COMP
Tools and documentation of the annual SMT competition
Brought to you by:
webertj
From: Tjark W. <tja...@it...> - 2015-06-10 19:09:41
|
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 |