(smt.arith.solver=2) Invalid model on QF_SLIA formula

[wintered]

Commit: 1fc9a7b

$z3release smt.arith.solver=2 model_validate=true bug.smt2 
sat
(error "line 50 column 10: an invalid model was generated")
$z3release model_validate=true bug.smt2 
sat
$cat bug.smt2 
(declare-fun a () String)
(declare-fun b () String)
(declare-fun c () String)
(declare-fun d () String)
(declare-fun x () String)
(declare-fun e () String)
(declare-fun f () String)
(declare-fun y () String)
(declare-fun g () String)
(declare-fun h () String)
(declare-fun i () String)
(declare-fun j () Int)
(declare-fun k () Int)
(declare-fun l () Int)
(declare-fun m () Int)
(declare-fun n () String)
(declare-fun o () String)
(declare-fun false () Bool)
(declare-fun p () Bool)
(declare-fun q () Bool)
(declare-fun r () Bool)
(declare-fun s () Bool)
(declare-fun t () Bool)
(declare-fun u () Bool)
(declare-fun v () Bool)
(declare-fun w () String)
(assert (= false (not (= m 1))))
(assert
 (ite
  r
  (and false
       (= g d)
       (= h "")
       (= 0 (str.len a))
       (= w (str.++ o i))
       (not (str.in_re o (str.to_re ""))))
  (= k 0)))
(assert (= false (not (= l 0))))
(assert (ite s (and v q p (= l (str.len c))) (and (= 2 m) (= w (str.++ b f)))))
(assert (= t (not (= m 0))))
(assert
 (ite
  t
  (and (= y "") (= m j (str.len x)) false (= w n (str.++ g e)))
  (and u (= 0 (str.len d)))))
(assert (not (= "B" w)))
(assert (< k 0))
(assert (>= 0 l))
(assert (< 0 m))
(check-sat)

[NikolajBjorner]

Invalid model on QF_S formula

[562] % z3release model_validate=true small.smt2
sat
(error "line 16 column 10: an invalid model was generated")
(
 (define-fun i () String
  "B")
 (define-fun f () String
  "DC")
 (define-fun g () String
  "efDCF")
 (define-fun a () String
  "ab")
 (define-fun b () String
  "DCfeF")
 (define-fun d () String
  "")
 (define-fun scr2_t2 () String
  "")
 (define-fun h () String
  "")
 (define-fun c () String
  "")
 (define-fun e () String
  "E")
 (define-fun j () String
  "DC")
)
[563] % 
[563] % cat small.smt2
(declare-fun a () String)
(declare-fun b () String)
(declare-fun c () String)
(declare-fun d () String)
(declare-fun e () String)
(declare-fun f () String)
(declare-fun g () String)
(declare-fun h () String)
(declare-fun i () String)
(declare-fun j () String)
(declare-fun scr2_t2 () String)
(assert (distinct "-" (str.substr f 0 (str.len i))))
(assert (distinct i ""))
(assert (= j (str.replace (str.replace f i "") "fgomsicgrrddxntn" "")))
(assert (= (str.++ c "abdc" a b "ef" j d scr2_t2 e) (str.++ a "dcab" c j "fe" e g h)))
(check-sat)
(get-model)
[564] %

With unicode=false, the bug doesn't trigger.

Commit: 0a9ee6c

from #4613