[SMT-LIB] QF_BV and division by zero

[Florian Schanda]

On Tuesday 20 Oct 2015 11:19:50 Viktor Kuncak wrote:
> A clarification question: does IEEE FP standard enforce that multiple
> executions with same arguments always yield the same result, even for the
> cases where the result of the operation is unspecified?

It implies it, I think, but does not strictly enforce it. But it would be 
quite an interesting hardware where that is not the case...

For reference, the relevant section is this: "minNum(x, y) is the 
canonicalized number x if x < y, y if y < y, the canonicalized number if one 
operand is a number and the other a quiet NaN. Otherwise it is either x or y, 
canonicalized (this means results might differ among implementations)."

In addition, in section 11 (reproducible floating-point results), there is a 
specific note on this. "Do not depend on the sign of a zero result [...] for 
minNum(x, y) [...] when x and y are equal."

I think the current unspecified result is the most faithful one.

	Florian