Invalid model for QF_LIA formula (opt)

[rainoftime]

Hi, for the following formula, z3 (commit a0de244) gives an invalid model

(set-logic QF_LIA)
(declare-fun _substvar_774_ () Bool)
(set-option :opt.priority pareto)
(set-option :model_validate true)
(declare-const v2 Bool)
(declare-const i0 Int)
(declare-const i2 Int)
(declare-const i3 Int)
(declare-const i5 Int)
(declare-const v5 Bool)
(declare-const v6 Bool)
(declare-const i7 Int)
(assert (or v2 (> (div i3 53) (+ i3 87))))
(assert (or (= _substvar_774_ v6 (= i5 i0) (not v2) v6 (>= 87 (+ i3 87)) false false) v5))
(assert (or (xor true false v5) (= i5 i0)))
(minimize (+ i0 i2))
(maximize (- i0 i3))
(minimize (+ i0 i5))
(maximize (- i0 i7))
(maximize (- i2 i3))
(maximize (- i3 i5))
(check-sat)

[NikolajBjorner]

similar to #4136