invalid model issue on an incremental QF_NIA instance

[zhendongsu]

Commit: 3af2b36
OS: Ubuntu 22.04

[535] % z3release model_validate=true small.smt2
sat
sat
(error "line 25 column 10: an invalid model was generated")
(
  (define-fun c () Int
    1)
  (define-fun g () Int
    1)
  (define-fun b () Int
    1)
  (define-fun d () Int
    1)
  (define-fun f () Int
    1)
  (define-fun e () Int
    (- 1))
  (define-fun a () Int
    0)
  (define-fun div0 ((x!0 Int) (x!1 Int)) Int
    0)
  (define-fun mod0 ((x!0 Int) (x!1 Int)) Int
    (ite (and (= x!0 0) (= x!1 0)) (- 1)
      0))
)
[536] % cat small.smt2
(declare-const a Int)
(declare-const b Int)
(declare-const c Int)
(declare-const d Int)
(declare-const e Int)
(declare-const f Int)
(declare-const g Int)
(push)
(assert (> f 0))
(push)
(assert (> c 0))
(push)
(assert (> d 0))
(push)
(assert (> b 0))
(push)
(assert (> g 0))
(push)
(assert (< e 0))
(push)
(assert (= a (div 1 0)))
(assert (distinct 0 (mod 0 0)))
(check-sat)
(assert (= 0 (mod a 0)))
(check-sat)
(get-model)

[zhendongsu]

Not sure whether it's related or not, but below is another instance:

[560] % z3release smt.threads=2 model_validate=true small.smt2
sat
sat
sat
sat
[561] % z3release small.smt2
sat
sat
sat
unsat
[562] % cat small.smt2
(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c () Int)
(declare-fun d () Int)
(declare-fun e () Int)
(declare-fun f () Int)
(declare-fun g () Int)
(declare-fun h () Int)
(declare-fun i () Int)
(declare-fun j () Int)
(declare-fun k () Int)
(declare-fun l () Int)
(declare-fun m () Int)
(declare-fun n () Int)
(declare-fun o () Int)
(declare-fun p () Int)
(declare-fun q () Int)
(declare-fun r () Int)
(declare-fun s () Int)
(declare-fun t () Int)
(declare-fun u () Int)
(declare-fun v () Int)
(push)
(assert (and (<= (- 1) e) (<= (- 1) f 1) (<= r v 1) (<= (- 1) g 1) (distinct (- 1) h) (<= h 1) (>= i 0) (>= j 0) (>= k 0) (> (- i k (+ m k) u) 0) (= (+ (+ (- 1) i  e j) k) 0(- i (+ f j) (* g k)) 0(- (- v j) (* h k)))))
(check-sat)
(assert (and (>= n 0) (>= o 0)  (> (+ n c (* n p) m) 0) (distinct (+ l (- f o) (* g p)) 0) (= (+ (* v o) p (- (+ g h))) 0)))
(check-sat)
(assert (and (= (+ q r) 0) (distinct (+ a d) 0) (<= (+ l (* e q) f v) 0) (< (+ m r (* g d) (* h b)) 0)))
(check-sat)
(assert (and (< s 0) (<= t 0) (>= u 0) (distinct (+ (+ 1 s) (* l t)) 0) (= (+ (+ (- 1) s) (* e t) u) 0(+ s (* f t) (* g u)) 0(+ (* v t) (- h u)))))
(check-sat)