Model Validation Fail

[muchang]

Hi,
For this formula:

(declare-fun a () String)
(declare-fun b () String)
(declare-fun c () String)
(declare-fun d () String)
(declare-fun h () String)
(declare-fun k () String)
(declare-fun l () String)
(declare-fun m () String)
(declare-fun n () String)
(declare-fun o () String)
(declare-fun p () String)
(declare-fun u () String)
(declare-fun w () String)
(declare-fun x () String)
(declare-fun e () Bool)
(declare-fun f () Bool)
(declare-fun g () Bool)
(declare-fun q () Bool)
(declare-fun r () Bool)
(declare-fun s () Bool)
(declare-fun t () Bool)
(declare-fun v () Bool)
(declare-fun y () Bool)
(declare-fun i () Int)
(declare-fun j () Int)
(assert (= (not (= e (not (= f r)))) (not (= "" (str.substr h 6 (str.len u))))))
(assert (not (= e (not (= f r)))))
(assert (= (not (= g v)) (not (= j 0))))
(assert
 (ite
  t
  (and
   (= j i)
   (= u (str.++ k l))
   (= i (str.len (str.substr x 0 (str.len o))))
   (= l (str.++ (str.substr c 0 (str.len m)) (str.substr d 0 (str.len n))))
   (= (str.substr c 0 (str.len m)) (str.++ (str.substr x 0 (str.len o)) p))
   (= p "**utma0168862645")
   )
  (and (= j 0))))
(assert
 (=
  (not (= e q))
  (= ""
   (str.substr a (str.len k)
    (str.len (str.substr b (str.len l)
              (str.len (str.substr d (str.len n) (str.len w)))))))))
(assert (= (not (= y s)) (not v)))
(assert (not (= y s)))
(assert (= a (str.++ k w)))
(assert (= b (str.++ l w)))
(assert (= d (str.++ n w)))
(assert (= e (not (= q  r v))))
(assert (=  g (not (= t v))))
(assert (= h (str.++ u w)))
(check-sat)

Z3 will correctly answer sat, but if model_validate is on, it will throw out an invalid model error:

z3 model_validate=true file.smt2
disequality failed: "" != w
""
""
exclude "" = w = ""
sat
(error "line 56 column 10: an invalid model was generated")

OS: Ubuntu 18.04
Revision: 16d4ccd