[SMT-COMP] QF_FP, min and zeros
tjark.weber at it.uu.se
Fri Apr 21 08:04:54 EDT 2017
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?
More information about the SMT-COMP