[542] % z3release model_validate=true small.smt2 
sat
(
 (define-fun x () (_ FloatingPoint 11 53)
  (_ -zero 11 53))
)
sat
(error "line 8 column 20: an invalid model was generated")
(
 (define-fun x () (_ FloatingPoint 11 53)
  (_ +zero 11 53))
)
[543] % 
[543] % cat small.smt2 
(define-sort FPN () (_ FloatingPoint 11 53))
(declare-const x FPN)
(assert (= x (fp.max (_ -zero 11 53) (_ +zero 11 53))))
(assert (= x (_ -zero 11 53)))
(assert (distinct x (_ +zero 11 53)))
(check-sat)
(get-model)
(check-sat-using smt)
(get-model)
[544] %