[SMT-COMP] SMT-COMP 2016: Main Track Test Job

[Tjark Weber]

On Fri, 2016-05-27 at 13:37 +0000, Christoph Wintersteiger wrote:
> Regarding the benchmarks in QF_FP\wintersteiger\rem: Those have very
> recently (less than two months ago) been updated, because when they
> were first generated, the wrong semantics of the fp.rem operator were
> used. Not all solver developers may have realized this yet. The
> current benchmarks should hopefully be correct, but solvers that were
> not updated yet may produce wrong results (so does z3 4.4.1; and the
> latest development version is still not fully compliant either). I'd
> suggest not to use these benchmarks in the competition (the other
> QF_FP\wintersteiger\* should be ok though), but I'll leave that
> decision to the organizers of course.

We have decided to retain these benchmarks. They are (hopefully)
correct now, and the semantics of fp.rem in SMT-LIB -- which is defined
independently of these benchmarks -- has not changed in a long time.

There are three solvers currently entered into QF_FP: Colibri, MathSAT
5 (entered non-competitively by the organizers) and Z3 (also entered
non-competitively by the organizers). MathSAT 5 does not support
fp.rem, so there is no soundness issue. Since Z3 is known to produce
wrong results, we will withdraw it from QF_FP.

The Colibri authors are of course free to withdraw their solver from
QF_FP, or to submit a new version (e.g., to report "unknown" on
problems containing fp.rem) until the final solver submission deadline
this Sunday.

Best,
Tjark