Invalid model on QF_S formual with str.at, str.indexof

[muchang]

Hi,
For this case, Z3 gives an invalid model:

[600] % z3release model_validate=true small.smt2
sat
(error "line 4 column 10: an invalid model was generated")
[601] % cvc4 -q --strings-exp small.smt2
sat
[602] % cat small.smt2
(declare-fun a () String)
(declare-fun b () String)
(assert (distinct (str.at a (str.indexof "B" b 1)) (str.at b 5 )))
(check-sat)
[603] %

OS: Ubuntu 18.04
Commit: 7597396

[NikolajBjorner]

same as #4086