[Consolidated] Invalid model issues

[merlinsun]

Hi,
For the following instance, z3 9c35971 returns an invalid model.

$ z3 model_validate=true small.smt2
sat
(error "line 9 column 34: an invalid model was generated")
$ cat small.smt2
(declare-fun b (Int Int) Int)
(declare-fun b (Int Real) (Array Int Real))
(declare-fun v () Real)
(declare-fun va () Real)
(declare-fun r () Real)
(declare-fun a () Real)
(assert (forall ((a Real)) (distinct 0.0 (div (to_int a) 0))))
(assert (and (< 0.0 (- v r)) (= r (* va va (/ va r))) (= a (select (b (b 0 0) a) 0))))
(check-sat-using (then fm default))

[merlinsun]

$ cat delta.smt2
(declare-const x2 Int)
(declare-const x Bool)
(declare-fun r () String)
(declare-fun r2 () String)
(declare-fun a () String)
(declare-fun v () Bool)
(declare-fun ar () Int)
(assert (= (= x v) (str.in.re (str.substr a (mod x2 (* ar (- ar) (div ar x2) (div 0 x2))) 1) (str.to.re (str.substr r2 0 (str.len r))))))
(assert (or (forall ((V String)) (str.in_re r2 (str.to_re "A"))) (exists ((v String)) (not (str.in.re v (str.to.re (str.substr a 0 (str.len r))))))))
(check-sat-using smt)
$ z3 model_validate=true small.smt2
sat
(error "line 10 column 20: an invalid model was generated")

[merlinsun]

$ z3 small.smt2 model_validate=true
sat
(error "line 7 column 10: an invalid model was generated")
$cat small.smt2
(declare-const x Int)
(declare-const x1 Bool)
(declare-fun v () String)
(declare-fun a () String)
(assert (forall ((v Int)) (or x1 (> v 0))))
(assert (distinct v "l" "" (str.substr a 0 (div 1 (* x x x)))))
(check-sat)