[Consolidated] Invalid model issues

[merlinsun]

Hi,
For this instance, z3 af80bd1 gives an invalid model.

$ z3 small.smt2 model_validate=true
sat
(error "line 8 column 10: an invalid model was generated")
$ cat small.smt2
(declare-const x Bool)
(declare-const x2 Int)
(declare-fun v () String)
(declare-fun e () Bool)
(declare-fun a () Bool)
(assert (and (>= 0 (mod x2 (* x2 x2 x2))) (= a (not x)) (= 0 (ite (str.contains (str.substr v 0 (str.len v)) "L") 1 0)) (= x (not e))))
(assert (exists ((T Bool)) T))
(check-sat)

[merlinsun]

$ z3 delta.smt2 model_validate=true
sat
(error "line 9 column 10: an invalid model was generated")
$  cat delta.smt2
(declare-const x2 Bool)
(declare-const x20 Bool)
(declare-const x1 Bool)
(declare-const x Bool)
(declare-fun b (Int) Bool)
(declare-fun v () Int)
(assert (= 1 (div 2 (* 4 v))))
(assert (exists ((v Int)) (or x2 (and x1 x x20 (b v)))))
(check-sat)

[merlinsun]

$ z3 model_validate=true small2.smt2
sat
(error "line 4 column 10: an invalid model was generated")
$ cat small2.smt2
(declare-fun e () Int)
(declare-fun v () Int)
(assert (and (= 0 (bv2nat ((_ int2bv 2) e))) (= (+ e 1) (bv2nat ((_ int2bv 2) v)))))
(check-sat)

[NikolajBjorner]

see #6194