Invalid model for String formula (smt.arith.solver 5)

[rainoftime]

Hi, for the following formula, z3 (commit 8fe3caa) gives an invalid model

(set-option :model_validate true)
(set-option :smt.arith.solver 5)
(declare-const v3 Bool)
(declare-const v6 Bool)
(declare-const v8 Bool)
(declare-const v14 Bool)
(declare-const v15 Bool)
(declare-const v18 Bool)
(declare-const Str0 String)
(declare-const Str4 String)
(declare-const Str7 String)
(declare-const Str8 String)
(declare-const Str12 String)
(declare-const Str14 String)
(declare-const Str16 String)
(declare-const Str18 String)
(push 1)
(assert (! (distinct (str.++ Str4 Str12 Str4 Str8) "ajmokqsdko" Str8 Str0) :named IP_24))
(assert (! (or v6 (= v8 v8 v15 v14 false v18 v8 v3 true true) (= v8 v8 v15 v14 (= (str.++ Str16 "ajmokqsdko" Str18) Str7 (str.++ Str12 Str4 Str4 "" Str14)) v18 v8 v3 true true)) :named IP_46))
(check-sat)

[NikolajBjorner]

prevent abusive behavior wrt arithmetic solver and sequence solver.
Sequences require the standard arithmetic solvers.