Invalid model issue on floats

[lsrcz]

$ z3 model_validate=true bug.smt2
sat
(error "line 10 column 10: an invalid model was generated")
((s0 (fp #b0 #x0 #b001)))

$ z3 model_validate=true ok.smt2
unsat
(error "line 11 column 15: model is not available")

$ cat bug.smt2
(declare-fun s0 () (_ FloatingPoint 4 4))
(define-fun s1 () (_ FloatingPoint 4 4) (fp #b0 #b0000 #b001))
(define-fun s2 () Bool (fp.eq s0 s1))
(define-fun s8 () Real (fp.to_real s0))
(define-fun s10 () Real (/ 1.0 512.0))
(define-fun s11 () Bool (= s8 s10))
(define-fun s12 () Bool (not s11))
(define-fun s13 () Bool (and s2 s12))
(assert s13)
(check-sat)
(get-value (s0))

$ cat ok.smt2
(declare-fun s0 () (_ FloatingPoint 4 4))
(define-fun s1 () (_ FloatingPoint 4 4) (fp #b0 #b0000 #b001))
(define-fun s2 () Bool (fp.eq s0 s1))
(define-fun s8 () Real (fp.to_real s1))
(define-fun s10 () Real (/ 1.0 512.0))
(define-fun s11 () Bool (= s8 s10))
(define-fun s12 () Bool (not s11))
(define-fun s13 () Bool (and s2 s12))
(assert s13)
(check-sat)
(get-value (s0))

The s8 converts the float to real number. If we directly convert s1, then the solver is able to correctly conclude that it must be equal to 1/512, thus gives an unsat. However, if we convert s0, which is asserted to be equal to s1, then the solver will give an invalid model.