Soundness bug on QF_S formula with str.indexof, str.++

Hi,
For this case, Z3  gives an incorrect answer:
```
[633] % cvc4 -q --strings-exp small.smt2
unsat
[634] % z3-4.8.7 small.smt2
unsat
[635] % z3 small.smt2
sat
[636] % cat small.smt2
(declare-fun t () String)
(assert (= (str.indexof (str.++ "aa" t) t 3) (str.indexof (str.++ "aa" t) t 1)))
(check-sat)
[637] %
```

OS: Ubuntu 18.04
Commit: dd064a5
