Incorrect model

[LeventErkok]

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)))
)