Invalid model for String formula (seq, unsat_core)

[rainoftime]

z3 commit fcd2bc6

(set-option :model_validate true)
(set-option :unsat_core true)
(set-option :smt.string_solver seq)
(declare-const v5 Bool)
(declare-const v6 Bool)
(declare-const v10 Bool)
(declare-const v11 Bool)
(declare-const v12 Bool)
(declare-const v14 Bool)
(declare-const v16 Bool)
(declare-const i9 Int)
(declare-const i11 Int)
(declare-const Str12 String)
(assert (>= (str.len Str12) (div i11 i11)))
(assert (! (or v11 v11 (< 37 (div i11 i11))) :named IP_32))
(assert (! (or (< 37 (div i11 i11)) v11 (< 37 (div i11 i11))) :named IP_33))
(assert (! (or (< 37 (div i11 i11)) v11 (or v16 v5 v14 v10 v16)) :named IP_34))
(assert (! (or (or v16 v5 v14 v10 v16) v11 (< 37 (div i11 i11))) :named IP_35))
(assert (! (or (< 37 (div i11 i11)) (or v16 v5 v14 v10 v16) (< 37 (div i11 i11))) :named IP_36))
(maximize i9)
(check-sat-assuming (IP_32 IP_35))