Z3 smt.arith.solver=3 incorrect answer on String formual with str.to.int, str.len operators

[muchang]

Hi,
For this formula,

(declare-fun s () String)
(assert (= (str.to.int s) 10))
(assert (= (str.len s) 1))
(check-sat)

z3 smt.arith.solver=3 reports sat, while the formula should be unsat.

OS: Ubuntu 18.04
Revision: 23fcc21