z3 incorrect answer on string formula

[muchang]

Hi,
For this formula,

(declare-fun a () String)
(declare-fun b () String)
(declare-fun c () String)
(assert (str.in.re c (re.* (re.union (str.to.re "aa") (str.to.re "")))))
(assert (= 0 (str.to.int (str.replace a b (str.at a (str.len a))))))
(assert (= a (str.++ b c)))
(check-sat)
(get-model)

z3 will report sat and give the following model:

  (define-fun c () String
    "")
  (define-fun b () String
    "")
  (define-fun a () String
    "")

If I feed this model to the formula, z3 will report unsat.

z3-4.8.5 and 4.8.6 also report sat on this case.

OS: Ubuntu 18.04
Revision: f9b6e4e