[525] % z3release model_validate=true rewriter.flat=false small.smt2
sat
(error "line 19 column 10: an invalid model was generated")
(
  (define-fun d () Int
    0)
  (define-fun b () Int
    0)
  (define-fun a () Int
    1)
  (define-fun l () Int
    1)
  (define-fun k () Int
    0)
  (define-fun c () Int
    0)
  (define-fun j () Int
    0)
  (define-fun i () Int
    0)
  (define-fun h () Int
    1)
  (define-fun g () Int
    1)
  (define-fun f () Int
    1)
  (define-fun e () Int
    1)
  (define-fun div0 ((x!0 Int) (x!1 Int)) Int
    0)
  (define-fun mod0 ((x!0 Int) (x!1 Int)) Int
    0)
)
[526] % 
[526] % cat small.smt2
(set-logic QF_NIA)
(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)
(assert (or (= d 0 (div k c) i)))
(assert (= (mod 0 (- (- l) b)) i))
(assert (or (and (= j 0) (>= 0 (+ k a) 0))
         (and (= f 0 g a 0) (= b h 0))
         (= (div (- l) 9) 0) (= e 0)))
(check-sat)
(get-model)
[527] %