Invalid model issue on String theory

[whangdo]

Greetings, For this instance, an invalid bug occurred. We tried to make this instance as small as possible. We sincerely hope that our report will be helpful for the z3 team.

$ ./z3 ./small.smt2 model_validate=true
sat
(error "line 17 column 10: an invalid model was generated")

$ cat ./small.smt2
(set-logic ALL)
(declare-fun T1_20 () String)
(declare-fun T1_9 () String)
(declare-fun T2_20 () String)
(declare-fun T2_9 () String)
(declare-fun T_1 () String)
(declare-fun T_2 () String)
(declare-fun T_3 () String)
(declare-fun T_4 () String)
(declare-fun T_5 () String)
(declare-fun T_6 () String)
(declare-fun T_7 () String)
(declare-fun T_9 () String)
(declare-fun T_a () String)
(declare-fun var_0xINPUT_13340 () String)
(assert (= T1_9 (str.replace (str.from_int (str.len (str.substr T_6 (str.len "/search.jsp") (str.indexof "/search.jsp" T_7 6)))) (str.substr T_3 (str.to_int (str.replace (str.from_int 1) T_a (str.substr "&utmcc=" 8 6))) (mod (str.to_int T_2) (str.to_int (str.from_code 7)))) (str.substr T1_9 (str.len (str.substr T1_20 (str.to_int "/search.jsp") (str.to_int "&utmn=1665319367&utmcs=UTF-8&utmsr=1680x976&utmsc=24-bit&utmul=en-us&utmje=0&utmfl=-&utmdt=Ask%20A%20Word&utmhn=www.askaword.com&utmhid=445703265&utmr=0&utmp="))) 28))))
(check-sat)
(exit)

commit version: efc8932 release version: 4.13.0