JFS's handling of fp.min and fp.max is unsound.

[jryans]

Consider this benchmark QF_FP/wintersteiger/min/min-has-solution-13472.smt2.

There are several interesting things here

• Our current "is trivial" classification method considers this non-trivial because Z3's simplifier will not constant fold fp.min(+zero, -zero) or fp.max(+zero, -zero).

• When JFS runs this benchmark it detects that the fuzzing buffer is empty but that constant folding failed. In this case JFS will perform a single fuzzing run to determine if the constraints are sat/unsat by just evaluating all the constants at run time.

• This benchmark is expected to be sat but JFS reports it as unsat because at runtime we determine fp.min(-zero, +zero) to be -zero.

Unfortunately IEEE-754 isn't very clear what the definition of min (minNum in the standard ) and max (maxNum in the standard) should be for differently signed zeros.

There's an interesting discussion about this very issue on Z3's issue track. It seems that in the end the semantics (see BTRW15) that were decided on use non-deterministic choice.

Note that the underspecification is an issue only when one of the inputs to maxε,σ or minε,σ is −0 and
the other is +0. However, it means that we consider as acceptable models any structures with function
families maxε,σ and minε,σ that satisfy the specifications above, regardless of whether they return −0
or +0 for (−0, +0), and for (+0, −0). This is necessary because IEEE-754 itself allows either value to
be returned, and compliant implementations do vary. For example, on some Intel processors the result
returned by the x87 and SSE units is different

This is a problem for us because an implicit design decision of JFS is that all functions evaluate to a single deterministic value.