Refutation soundness bug in string logic

[jiwonparc]

commit: 484c83e

$ z3release bug.smt2 
unsat
$ z3-4.8.9 bug.smt2
sat
(model 
  (define-fun x () String
    "AA")
  (define-fun y () String
    "")
)
$ cat bug.smt2
(declare-fun x () String)
(declare-fun y () String)
(assert (not (= (str.prefixof (str.++ "A" "A") x) 
                  (str.prefixof "A" (str.replace (str.replace x "A" "") "A" "")))))
(check-sat)
(get-model)
(exit)
$ z3release feed_model.smt2
sat
$ cat feed_model.smt2
(define-fun x () String "AA")
(define-fun y () String "")
(assert (not (= (str.prefixof (str.++ "A" "A") x) 
                  (str.prefixof "A" (str.replace (str.replace x "A" "") "A" "")))))
(check-sat)
(exit)