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

[Tjark Weber]

On Thu, 2015-06-11 at 08:34 +0100, Martin Brain wrote:
> On Wed, 2015-06-10 at 21:09 +0200, Tjark Weber wrote:
> > 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.

You are right. Do I prefer spurious counter-examples (which users will
then look into, and which they can easily rule out with additional
assumptions if they want to verify their code against a specific IEEE
implementation) over unsound proofs (which users won't notice as
unsound until their programs break in production)? Absolutely.

Best,
Tjark