Invalid model on QF_ANIRA

[merlinsun]

Hi,
For the following instance, z3 2354998 gives an invalid model.

$ cat small.smt2 
(declare-const x1 Int)
(declare-const x Real)
(declare-fun a () Real)
(declare-fun r () (Array (Array Real Bool) Real))
(declare-fun v () (Array Real Bool))
(assert (and (< 0.0 x) (= 0.0 x1) (= x (/ x a)) (= 0.0 (/ 1.0 0.0)) (= 2 (* (select r v) (select r v)))))
(check-sat)
$ z3 model_validate=true rewriter.eq2ineq=true small.smt2
sat
(error "line 7 column 10: an invalid model was generated")