CODEWITHSUNDEEP
z3
Artem Razin
Artem Razin

Reputation: 1286

Rounded floating-point number comparison issue

Working on an analyzer based on Z3 (this analyzer should detect overflows when doubles converted to long/ulong in .net), I came across a strange thing related to floating-point numbers.

Finally, I've created a small sample that shows the issue:

Both:

(assert (= ((_ fp.to_sbv 64) roundTowardZero (fp #b0 #b10000111110 #x0000000000000)) #x8000000000000000))
(check-sat)

and:

(assert (not (= ((_ fp.to_sbv 64) roundTowardZero (fp #b0 #b10000111110 #x0000000000000)) #x8000000000000000)))
(check-sat)

give me sat.

How could it happen that a rounded floating-point number may be equal to some value, and at the same time it may not be equal?

Upvotes: 1

Views: 158

Answers (2)

Patrick Trentin
Patrick Trentin

Reputation: 7342

The floating point constant evaluates to

(-1)^0 * 2^(1086 - 1023) * (1 + 0) = 2^63

A Signed Bit-Vector of size e can hold values in the range [-2^(e-1), 2^(e-1) - 1]. Thus, the range of a Signed Bit-Vector of size 64 is [-2^63, 2^63 - 1].

Because 2^63 is outside that range, the conversion of 2^63 to a Signed Bit-Vector of size 64 is undefined:

In addition, fp.to_ubv and fp.to_sbv are unspecified for finite number inputs that are out of range (which includes all negative numbers for fp.to_ubv).

(source: SMT-LIB docs)

Since the conversion is undefined, the following expression

((_ fp.to_sbv 64) roundTowardZero (fp #b0 #b10000111110 #x0000000000000))

may have an arbitrary, unconstrained, 64-bit Bit-Vector value.

This explains why the equality can be found to be both true and false.

Upvotes: 2

Malte Schwerhoff
Malte Schwerhoff

Reputation: 12852

I assume you made those assertions separately of another, i.e. you asked Z3 if P is satisfiable, and (separately) if ¬P is satisfiable. This is different from asking if P ∧ ¬P is satisfiable. As an example, assume P is n = 0, for some integer n. Clearly, n could be 1, in which case ¬(n = 0) is satisfied, and n could be 0, in which case n = 0 is satisfied.

Upvotes: 1

Related Questions