Invalid model issue on QF_NRA

[merlinsun]

Hi,
For this following instance, z3 0556059 gives an invalid model.
But I'm not sure if it's a duplicate of #2650.

$ cat small.smt2 
(declare-fun r () Real)
(assert (= 0.0 (/ 1.0 1.0 r)))
(check-sat-using nlqsat)
$ z3 model_validate=true small.smt2
sat
(error "line 3 column 23: an invalid model was generated")
$ z3 model_validate=true nlsat.check_lemmas=true small.smt2
check lemma: b1
check
sat
(error "line 3 column 23: an invalid model was generated")