Invalid model for string formula

[jiwonparc]

commit: 6bdf377

$ z3-4.8.10 model_validate=true small.smt2
unknown
(error "line 7 column 10: model is not available")
$ z3release model_validate=true small.smt2
sat
(error "line 6 column 10: an invalid model was generated")
(
  (define-fun a () String
    "")
)
$ cat small.smt2
(declare-fun a () String)
(assert (str.in_re a (re.* (re.union (str.to_re "b") (str.to_re (ite
 (str.in_re a (re.* (re.range "" (ite (str.in_re a (str.to_re "")) ""
 a)))) "" "a"))))))
(assert (not (str.in_re a (re.* (str.to_re "")))))
(check-sat)
(get-model)

[jiwonparc]

commit: 6bdf377
might be related to the above but returns a valid model in z3-4.8.10

$ z3release model_validate=true small.smt2
sat
(error "line 7 column 10: an invalid model was generated")
(
 (define-fun a () String
  "za")
)
$ cat small.smt2
(declare-fun a () String)
(assert (str.in_re (str.++ "z" a) (re.++ (re.* (re.union (re.diff
 (re.++ (re.* (re.union (str.to_re "z") (str.to_re "b"))) (str.to_re
 "a")) (re.+ (re.* (re.union (str.to_re "z") (str.to_re (str.at "a"
 (str.len a))))))) (re.* (re.range "a" "u")))) (str.to_re "b") (re.*
 (str.to_re "")))))
(check-sat)
(get-model)

[wintered]

Commit: 6bdf377

(proof=true)

$z3release proof=true model_validate=true bug.smt2
sat
(error "line 12 column 10: an invalid model was generated")
$cat bug.smt2
(declare-fun x1 () String)
(declare-fun x2 () String)
(declare-fun z1 () String)
(declare-fun z2 () String)
(declare-fun y1 () String)
(declare-fun y2 () String) 
(declare-fun t1 () String)      
(declare-fun t2 () String) 
(assert (= (str.++ (str.++ (str.++ x2 x1) (str.replace (str.++ z2 "fe")
        (str.++ z1 "gf") "fe")) (str.++ (str.++ y1 t1) y2))
        (str.++ z1 (str.++ (str.++ y2 t2) y1)))) 
(check-sat)