[SMT-COMP] QF_FP, min and zeros

[Tjark Weber]

On a related note, I am wondering about the status of benchmarks and
solver implementations regarding

  fp.min, fp.max, fp.to_ubv, fp.to_sbv, fp.to_real

In 2016, benchmarks containing any of these functions where excluded
from the competition.

Based on http://smtlib.cs.uiowa.edu/theories-FloatingPoint.shtml my
understanding is that these functions are underspecified (i.e., they
have more than one possible interpretation).

1) Is the status of benchmarks in QF_FP/QF_BVFP (if known) correct with
respect to this semantics?

2) Do solvers that support floating-point logics (e.g., MathSAT, Z3)
implement this semantics?

3) Are there (other) reasons to again exclude these functions from the
competition in 2017?

Best,
Tjark