Invalid model for QF_LIA formula (proof, smt.phase_selection, smt.random_seed)

[rainoftime]

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

(set-logic QF_LIA)
(set-option :model_validate true)
(set-option :proof true)
(set-option :smt.phase_selection 6)
(set-option :smt.random_seed 8)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v5 Bool)
(declare-const v7 Bool)
(declare-const v8 Bool)
(declare-const v10 Bool)
(declare-const v11 Bool)
(declare-const v12 Bool)
(declare-const v13 Bool)
(declare-const i0 Int)
(declare-const i2 Int)
(declare-const i3 Int)
(declare-const v14 Bool)
(declare-const v15 Bool)
(declare-const v16 Bool)
(declare-const v17 Bool)
(push 1)
(assert (! (or v5 v16 v10) :named IP_1))
(assert (! (or v7 v15 v7) :named IP_5))
(assert (! (or (= v1 v11 v2) v14) :named IP_9))
(assert (! (or (distinct i2 (abs i0)) (distinct (- 27 (- 27) i3 i2 i0) i2) v16) :named IP_12))
(assert (! (distinct i2 (abs i0)) :named IP_13))
(assert (! (or v14 v16 v2) :named IP_15))
(assert (! (or v14 v7 v17) :named IP_21))
(assert (! (or (distinct i2 (abs i0)) v14 v14) :named IP_22))
(assert (! (or v15 v14 v17) :named IP_23))
(assert (! (or v5 v13 v16) :named IP_24))
(assert (! (or v5 v2 v5) :named IP_25))
(assert (! (or v17 v16 v14) :named IP_28))
(assert (! (distinct (- 27 (- 27) i3 i2 i0) i2) :named IP_30))
(assert (! (or v15 v17) :named IP_31))
(assert (! (or v15 v12) :named IP_44))
(assert (! (or v17 (distinct i2 (abs i0))) :named IP_49))
(assert (! (or (distinct (- 27 (- 27) i3 i2 i0) i2) v15 v12) :named IP_50))
(assert (! (or (distinct (- 27 (- 27) i3 i2 i0) i2) v7) :named IP_52))
(assert (! (or v17 v7 v14) :named IP_54))
(assert (! (or v10 v14) :named IP_55))
(assert (! (or v17 v5 v12) :named IP_60))
(assert (! (or v12 false v7) :named IP_62))
(assert (! (or v5 v17 v7) :named IP_63))
(assert (! (or v13 v10 v17) :named IP_66))
(assert (! (or v13 v5 v13) :named IP_67))
(assert (! v8 :named IP_90))
(assert (! (or v13 v12 v7) :named IP_91))
(assert (! (or (= 27 i3) (distinct i2 (abs i0))) :named IP_93))
(assert (! (or v17 v13 v15) :named IP_94))
(check-sat)
(check-sat)
(check-sat)
(check-sat-assuming ((! (or v12 v17 v10) :named IP_29) (! (or (> i0 27 59 i2) v14 (distinct (- 27 (- 27) i3 i2 i0) i2)) :named IP_58)))

[NikolajBjorner]

seems fixed