Invalid mode on QF_S formula with str.substr, str.++ and str.len 

Hi,
For this case, Z3  gives an invalid model:
```
[566] % z3 model_validate=true small.smt2
sat
(error "line 4 column 10: an invalid model was generated")
[567] % 
[567] % cat small.smt2
(declare-fun a () String)
(declare-fun b () String)
(assert (= (str.substr (str.++ a "aa" b) 4 (str.len a)) a))
(check-sat)
[568] %
```

OS: Ubuntu 18.04
Commit: 38e0968
