Incorrect SAT on String formula

[muchang]

Hi,
For this formula,

(declare-fun a () Int)
(declare-fun b () String)
(declare-fun c () String)
(declare-fun d () String)
(declare-fun f () String)
(declare-fun e () Int)
(declare-fun w () String)
(declare-fun g () String)
(declare-fun h () String)
(declare-fun i () String)
(declare-fun j () String)
(declare-fun k () Bool)
(declare-fun l () String)
(declare-fun m () Int)
(declare-fun n () Int)
(declare-fun o () String)
(declare-fun p () String)
(declare-fun q () String)
(declare-fun d () String)
(declare-fun r () String)
(declare-fun s () String)
(declare-fun t () String)
(declare-fun u () Bool)
(declare-fun v () String)
(assert (or
            (and (=   (and (= l  (str.++ g h)g (str.++ i j))(= j "__utmz=169413169.")(not (str.in.re w (re.++   (str.to.re "_" )  (re.++   (str.to.re "_" ) (re.++  (str.to.re "u" 
) (re.++  (str.to.re "t" ) (re.++  (str.to.re "m" ) (re.++  (str.to.re "z" ) (re.++  (str.to.re "=" ) (re.++  (str.to.re "1" ) (re.++  (str.to.re "6" ) (re.++  (str.to.re "9" ) (r
e.++  (str.to.re "4" ) (re.++  (str.to.re "1" ) (re.++  (str.to.re "3" ) (re.++  (str.to.re "1" ) (re.++  (str.to.re "6" ) (re.++  (str.to.re "9" )  (str.to.re "." )  ) ) ) ) ) ) 
) ) ) ) ) ) ) ) ) ) )))k (= "" l)) k)
        (and (=
                (and (= (div a e) m)(= (str.replace d h (str.at d (str.len d))) (str.++ o (str.replace (str.replace c w (str.at c (str.len c))) "Mw7V" (str.at c (str.len c)))))(= 
m (str.len s))(= (str.replace (str.replace c w (str.at c (str.len c))) "Mw7V" (str.at c (str.len c))) (str.++ q r))(= q (str.++ s t))(= (str.replace (str.replace f i (str.at f (st
r.len f))) "0oP6M" (str.at f (str.len f))) "__utmz=169413169.")(not (str.in.re p (re.++   (str.to.re "_" )  (re.++   (str.to.re "_" ) (re.++  (str.to.re "u" ) (re.++  (str.to.re "
t" ) (re.++  (str.to.re "m" ) (re.++  (str.to.re "z" ) (re.++  (str.to.re "=" ) (re.++  (str.to.re "1" ) (re.++  (str.to.re "6" ) (re.++  (str.to.re "9" ) (re.++  (str.to.re "4" )
 (re.++  (str.to.re "1" ) (re.++  (str.to.re "3" ) (re.++  (str.to.re "1" ) (re.++  (str.to.re "6" ) (re.++  (str.to.re "9" )  (str.to.re "." )  ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ))
)
                u
                (= "" (str.substr b 0 (str.len (str.replace d h (str.at d (str.len d)))))))
            u)))
(assert (=  (div a n) n))
(assert (= b c (str.++ (str.++ w "Mw7V") p)))
(assert (= d (str.++ h v)))
(assert (= f (str.++ (str.++ i "0oP6M") t)))
(check-sat)

z3 will incorrectly report sat and give a wrong model:

(model
  (define-fun p () String
    "__utmz=169413169.\x00")
  (define-fun t () String
    "__utmz=169413169.")
  (define-fun n () Int
    0)
  (define-fun w () String
    "")
  (define-fun h () String
    "\x00")
  (define-fun u () Bool
    true)
  (define-fun j () String
    "")
  (define-fun e () Int
    0)
  (define-fun o () String
    "")
  (define-fun i () String
    "")
  (define-fun q () String
    "__utmz=169413169.")
  (define-fun g () String
    "!0!")
  (define-fun s () String
    "")
  (define-fun l () String
    "")
  (define-fun a () Int
    (- 1))
  (define-fun m () Int
    0)
  (define-fun v () String
    "__utmz=169413169.\x00")
  (define-fun r () String
    "\x00")
  (define-fun f () String
    "0oP6M__utmz=169413169.")
  (define-fun d () String
    "\x00__utmz=169413169.\x00")
  (define-fun b () String
    "Mw7V__utmz=169413169.\x00")
  (define-fun c () String
    "Mw7V__utmz=169413169.\x00")
  (define-fun k () Bool
    false)
)

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

OS: Ubuntu 18.04
Revision: bba9d11