Incorrect model
Author: LeventErkokCreated Sep 2, 2025Updated Sep 11, 2026
LabelsFloats
This query should be unsat.
$ cat a.smt2
(set-logic ALL)
(declare-datatype Expr ((Flt (getFlt_1 (_ FloatingPoint 8 24)))))
(declare-fun x () Expr)
(assert (distinct x (Flt (_ NaN 8 24))))
(assert (fp.isNaN (getFlt_1 x)))
(check-sat)
(get-model)
$ z3 model_validate=true a.smt2
sat
(error "line 6 column 10: an invalid model was generated")
(
(define-fun x () Expr
(Flt (_ NaN 8 24)))
)Source: Z3Prover/z3