Incorrect answer of smt.arith.solver=3 on string formula with str.to.int operator

Hi,
For this unsat formula,
```
(declare-fun s () String)
(assert (or (= s "0") (= s "1")))
(assert (> (str.to.int s) 1))
(check-sat)
```
`z3 smt.arith.solver=3` incorrectly gives sat and an incorrect model:
```
(model 
  (define-fun s () String
    "0")
)
```

OS: Ubuntu 18.04
Revision: 321bad2

