unsatisfiable string formula reported satisfiable

[wintered]

Hi,
the following unsatisfiable formula is reported satisfiable by z3

(declare-fun x () String)
(declare-fun y () String)
(declare-fun z () String)
(assert
  (not
    (=
      (str.contains y (str.replace "A" (str.replace (str.++ x z) x "") z))
      (str.contains y "A")
    )
  )
)
(check-sat)     

We have double-checked the formula with CVC4 which gives unsat. We fed the model to the formula which is unsat as well.

Revision: 000e485
OS: Ubuntu 18.04