Z3 returns SAT for a query that should be UNSAT.

To reproduce

Run z3 on the following query:

(set-logic QF_S)
(declare-const xs String)
(declare-const ys String)
(assert (= (str.++ (str.substr ys 0 18) (str.substr xs 0 18)) (str.++ "It")))
(assert (> (str.len ys) 18))
(check-sat)

Expected: unsat
Actual: sat

A string concatenation of 18 characters should not equal a 2 character string "It".