Invalid model for UFNIA formula

[rainoftime]

Hi, for the following formula,

(set-option :model_validate true)
(declare-const i5 Int)
(declare-const i12 Int)
(declare-sort S1 0)
(assert (exists ((q9 Int) (q10 S1)) (>= q9 0)))
(assert (>= 83 i12))
(assert (distinct 7 i5))
(assert (<= i12 91))
(assert-soft (or (>= 83 i12)))
(check-sat)

z3 c431a10 gives an invalid model.

[rainoftime]

@NikolajBjorner I am aware that opt cannot support quantified formulas well. But I am not sure about the maxsmt feature (although it may use a similar algorithm with opt). If the feature is not stable, I will close the issue.