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

[Martin Brain]

On Wed, 2015-06-10 at 21:09 +0200, Tjark Weber wrote:
> 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.

I agree with you but note that there is a counter-argument that in the
situation you give, the current semantics will give spurious
counter-examples that cannot be executed on the target platform.  I
guess it is personal taste depending on whether you feel it is better to
under or over approximate the behaviour of the system.  My reasoning was
that all IEEE-754 compliant systems should be model of the theory.

> 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?

(_ fp.to_ubv m), (_ fp.to_sbv m) and fp.to_real are all underspecified
for the 'special values' such as +/-Inf and NaN.  The first two are also
underspecified for all values outside of the current range because,
again, there are significant differences in hardware.

Cheers,
 - Martin