Invalid model issue on String

[merlinsun]

Hi, z3 https://github.com/Z3Prover/z3/commit/a8da0a685184ffbe89292ac1f325c8ae32c68303 produces an invalid model for the instance I've attached. Unfortunately, I'm unable to provide a reduced test case as the delta debugging tools cannot reduce the instance.

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

case.smt2.zip