CODEWITHSUNDEEP
z3
chen rui
chen rui

Reputation: 37

Z3 gives a NaN value for my floating point constraint

Given the following floating point constraint, Z3 produces a abnormal model, in which z is NaN. Obviously, it is not a right solution. Is it a bug? BTW. the version of z3 is 4.5.0

(declare-const x (_ FP 11 53))
(declare-const y (_ FP 11 53))
(declare-const z (_ FP 11 53))


(assert 
 (and 
  (not (fp.lt x (_ +zero 11 53)))
  (not (fp.lt y (_ +zero 11 53)))
  (not (fp.lt z (_ +zero 11 53)))
  (not (fp.leq (fp.add roundNearestTiesToEven x y) z))
 )
)

(check-sat)
(get-model)

Upvotes: 0

Views: 174

Answers (1)

Christoph Wintersteiger
Christoph Wintersteiger

Reputation: 8392

This is not a bug, these are the correct semantics for the operators involved (according to SMT-LIB and according to IEEE-754 as well). The model I get is this:

(model 
  (define-fun z () (_ FloatingPoint 11 53)
    (_ NaN 11 53))
  (define-fun y () (_ FloatingPoint 11 53)
    (fp #b0 #b00000000000 #x0000000004000))
  (define-fun x () (_ FloatingPoint 11 53)
    (_ +zero 11 53))
)

and indeed (not (fp.leq (fp.add roundNearestTiesToEven x y) z)) is satisfied, i.e., x + y is not less than NaN, because nothing is less than NaN (all predicates are false for NaN inputs).

If this behavior is not desired, we can of course add another constraint to make sure z is not a NaN:

(assert (not (= z (_ NaN 11 53))))

and Z3 will then find a model where y (and thus x+y) is NaN.

Upvotes: 2

Related Questions