Invalid model issue on a simple string formula

[merlinsun]

Hi,
For this instance, z3 7cd8edc gives an invalid model.

$ cat small.smt2 
(declare-fun t () String)
(declare-fun r () String)
(declare-fun i () String)
(declare-fun tr () String)
(declare-fun s () String)
(assert (= (str.++ i r) (str.++ r t)))
(assert (= (str.++ tr t) (str.++ s (str.++ i r))))
(check-sat)
$ z3 model_validate=true small.smt2       
sat
(error "line 8 column 10: an invalid model was generated")