SBV->C: Semantics of fpMin/fpMax around +/-0 is not the same as SMTLib

[LeventErkok]

Not sure if this is really worth "fixing." But we're currently translating SMTLib's fpMin/fpMax to C's fmin/fmax functions; which semantically disagree when given +/-0.

In case of SMTLib2; the result is +0. In case of the C-function (following x86 hardware), the result is the second argument.

Note that both behaviors are IEEE754 compliant; but just another nuisance to watch out for; if it ever comes up.

[LeventErkok]

The real issue here is that which semantics should we go with? If we take the C-semantics, then we need to wrap-around in our SMT-Lib generator to generate different code; otherwise, we need to wrap-around the C-translator to match the Z3/SMTLib semantics. Neither choice is satisfactory. Note that this only is an issue with the explicit calls to fpMin/fpMax; as those directly translate to Z3/C "equivalents." Regular use of min/max just goes through regular comparison, which does "whatever it does," but does it the same in both backends.

There's really no good solution here.