Invalid model for String formula (z3str3, dom-simplify unit-subsume-simplify smt)

[rainoftime]

Hi, for the following formula, z3 commit 1c760b0 gives an invali model

(set-option :model_validate true)
(set-option :smt.string_solver z3str3)
(declare-const Str4 String)
(declare-const Str13 String)
(declare-const Str17 String)
(declare-const i10 Int)
(assert (or false false (= (str.++ Str13 Str4) (str.++ Str4 "" (int.to.str i10) Str13) Str17 "")))
(check-sat-using (then simplify dom-simplify unit-subsume-simplify smt))

[rainoftime]

(set-option :model_validate true)
(set-option :smt.string_solver z3str3)
(declare-const i14 Int)
(declare-const Str1 String)
(declare-const Str7 String)
(declare-const Str8 String)
(declare-const Str9 String)
(declare-const Str10 String)
(declare-const Str17 String)
(declare-const Str18 String)
(declare-const v15 Bool)
(assert v15)
(assert (= (str.++ Str17 Str8) (str.++ Str8 (int.to.str i14) "" "" "") (str.++ Str8 (int.to.str i14) "" "" "") Str7 Str10))
(assert (= Str18 Str9 Str1 (str.++ Str18 Str7)))
(check-sat-using (then simplify dom-simplify unit-subsume-simplify qfufbv))

[rainoftime]

from #4364

(set-option :model_validate true)
(set-option :smt.string_solver z3str3)
(declare-const v2 Bool)
(declare-const Str0 String)
(declare-const Str3 String)
(declare-const Str9 String)
(declare-const Str14 String)
(declare-const Str16 String)
(declare-const Str19 String)
(declare-const i7 Int)
(declare-const i8 Int)
(assert (or (= false false false false false false false v2 false false false) (= Str19 "" "" Str0 Str14)))
(assert (or (= Str19 "" Str9 Str0 Str14) v2 (>= 630 i8)))
(assert (or (>= 630 i8) (= "" (str.++ Str3 Str16) Str9 (str.++ Str14 Str3)) (= Str19 "" Str9 Str0 Str14)))
(assert (> i7 0))
(check-sat-using (then simplify unit-subsume-simplify ufbv))