Soundness bug z3-seq

[wintered]

Hi,
on this formula, Z3 returns sat although the formula is unsat.

(declare-fun a () String)
(declare-fun b () String)
(declare-fun c () String)
(assert
 (or
  (str.contains "abc23cd"
   (str.++ (int.to.str (str.len c))
    (int.to.str (str.len c))
    (int.to.str (str.len c))))
  (str.contains (str.++ a b) (str.++ a "a" b))))
(check-sat)

OS: Ubuntu 18.04
Commit: 9f6a0a0