Incorrect model QF_S, distinct, str++, str.len

[wintered]

Hi,

consider the following formula.

(declare-fun x () String)
(declare-fun y () String)
(assert (distinct (str.++ x y) (str.++ y x)))
(assert (= (str.len x) 17))
(check-sat)
(get-model)

Z3 gives the following incorrect model:

(model 
  (define-fun y () String
    "\x00")
  (define-fun x () String
    "\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00")
)

OS: Ubuntu 18.04
Revision: a257ec0