[SMT-COMP] QF_FP, min and zeros

[François Bobot]

Le 20/04/2017 à 18:58, Christoph Wintersteiger a écrit :
> That's not exactly right; min-has-no-other-solution-13472.smt2 asserts this:
>
> (assert (= r (fp.min x y)))
> (assert (and (not (= r (_ +zero 11 53))) (not (= r (_ -zero 11 53)))))
>
> I.e., we have x/y are zeros and the result r is not +0 && not -0. The whole problem is unsatisfiable, i.e., r must be one of the zeros, but it's not known which one. I understand that this is the SMT-LIB semantics at least per BTRW15 (and that's also what's implemented in Z3).

Thank you for the confirmation of the semantics. I finally found the current version of the 
benchmark, thank you.

Best,

-- 
François