Invalid model for string formulas #5121
Description
Tell me if I should continue holding off the invalid model bugs for string formulas.
commit: b918f12
$ z3release model_validate=true t1.smt2
sat
(error "line 4 column 10: an invalid model was generated")
$ cat t1.smt2
(declare-fun a () String)
(declare-fun b () String)
(assert (str.in_re (str.++ "z" b) (re.* (str.to_re (str.substr "z" (str.len a) (str.len b))))))
(check-sat)