Invaid model for QF_LIA formulas (rewriter.flat false)

[rainoftime]

Hi, for the following formula,
z3 9f6a733 gives an invalid model

(set-logic QF_LIA)
(set-option :model_validate true)
(set-option :rewriter.flat false)
(declare-const i2 Int)
(assert (< (abs (+ 0 (- 0 83 i2 i2 0) i2)) (- 0 83 i2 0 0)))
(check-sat)

[rainoftime]

Another case with more options

(set-logic QF_LIA)
(set-option :model_validate true)
(set-option :rewriter.flat false)
(set-option :rewriter.sort_sums true)
(set-option :rewriter.arith_ineq_lhs true)
(declare-const i1 Int)
(declare-const i3 Int)
(declare-const i4 Int)
(assert (not (<= 0 867 (abs (+ i3 (- i1 867 i1 867 i1) 867)) 0 867)))
(assert (xor true true true true true true (<= i4 (abs (+ i3 (- i1 867 i1 867 i1) 867)))))
(check-sat)

[NikolajBjorner]

less is actually more (useful)