[604] % z3 model_validate=true small.smt2 
sat
(error "line 4 column 10: an invalid model was generated")
[605] % 
[605] % cat small.smt2 
(declare-fun a () String)
(declare-fun b () Int)
(assert (= (str.replace "A" (int.to.str b) a) (str.++ "A" (str.replace "" (int.to.str b) a))))
(check-sat)
[606] %