(z3str3) Soundness bug on QF_SLIA formula with str.substr and str.indexof

Hi,
For this case, Z3  gives an incorrect answer:
```
[594] % z3 small.smt2 
unsat
[595] % cvc4 --strings-exp small.smt2 
unsat
[596] % z3 smt.string_solver=z3str3 small.smt2 
sat
[597] % 
[597] % cat small.smt2 
(set-logic QF_S)
(declare-fun s () String)
(declare-fun i () Int)
(assert (distinct "" (str.substr s i (str.indexof "A" s i))))
(check-sat)
[598] %
```

OS: Ubuntu 18.04
Commit: 1729232
