[SMT-COMP] QF_FP, min and zeros

[François Bobot]

Le 20/04/2017 à 17:45, François Bobot a écrit :
> Hi everyone,
>
> 	We wonder what is the semantic of fp.min and fp.max:
>
> [RW10] Philipp Ruemmer and Thomas Wahl.
>           An SMT-LIB Theory of Binary Floating-Point Arithmetic.
>
>
> and
>
> [BTRW15] Martin Brain, Cesare Tinelli, Philipp Ruemmer, and Thomas Wahl.
>             An Automatable Formal Semantics for IEEE-754 Floating-Point Arithmetic
>             Technical Report, 2015.
>
>
> disagree on min(-0,+0), the first gives -0 the second is uninterpreted.
"uninterpreted" but still constrained to be equal to one of the argument. sorry.

> Moreover
> min-has-no-other-solution-13472.smt2 from Wintersteiger's benchmark says that min(-0,+0) is +0.
>
> We prefer the one of BTRW15 which correspond to IEEE, but in that case SMTCOMP should be fixed.
>
>
>
> As a side note, Wintersteiger is great and invaluable as a set of unit tests, but it should not be
> used for the competition. But perhaps it will not since it is crafted.
>
>
> PS: starexec seems down so I have not been able to check if I have the last version of the benchmark
>
> Thank you for the precisions,
>
> Best,
>