Invalid model issue on float formula

[merlinsun]

Hi, For this following instance, z3 https://github.com/Z3Prover/z3/commit/5cee19fa09555323f1b82baf8038cfdb858e6ee6 gives an invalid model.

$ cat small.smt2 
(declare-fun v () Real)
(assert (= ((_ to_fp 2 6) RTZ v) (fp (_ bv1 1) (_ bv0 2) (_ bv0 5))))
(check-sat)
$ z3 model_validate=true small.smt2
sat
(error "line 3 column 10: an invalid model was generated")