Solution unsoundness for real formula, invalid mdoel for integer formula

[rainoftime]

Hi, for the following formula, z3 4d41db2

(declare-const v Bool)
(assert (= v (distinct 0.0 (/ 1.0 0.0))))
(assert (= v (= 0.0 (/ 1.0 0.0))))
(check-sat)
(check-sat-using (then purify-arith aig recover-01 smt))

z3 model_validate=true yy.smt2
unsat
sat
(error "line 5 column 55: an invalid model was generated")

[rainoftime]

Invalid model

(declare-fun m () Int)
(declare-fun A () Bool)
(declare-fun r () Int)
(assert (and (= 0 m) (or A (= r 0)) (or (not A) (= r 1))))
(check-sat)
(check-sat-using (then reduce-invertible recover-01 smt))

z3 xx.smt2 model_validate=true
sat
sat
(error "line 6 column 56: an invalid model was generated")