Invalid model for QF_LIA formula (add-bounds ctx-solver-simplify nnf unit-subsume-simplify qffd, sat.local_search)

[rainoftime]

Hi, for the following formula,

(set-logic QF_LIA) 
(set-option :model_validate true)
(set-option :sat.local_search true)
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const i5 Int)
(assert (or (xor false false true true true false true true false v5 false) (xor v4 false true true true false true true (> (mod i5 775) 26) v5 true)))
(check-sat-using (then simplify add-bounds ctx-solver-simplify nnf unit-subsume-simplify qffd))

z3 commit 0f69783 gives an invalid model

(sat.local-search l_true)
Verifying solution
solution verified
sat
model check failed on:  (or (xor false false true true true false true true false v5 false)
    (xor v4 false true true true false true true (> (mod i5 775) 26) v5 true))
expected value: true
#49: (or #32 #48) false
#32: (xor false #31) false
#48: (xor v4 #47) false
...
...
#35: 775 775
(define-fun v4 () Bool
  false)
(define-fun i5 () Int
  (- 2))
(define-fun v5 () Bool
  true)
(error "line 8 column 94: an invalid model was generated")