invalid model on a QF_NIA instance

[zhendongsu]

Commit: e6ea815
OS: Ubuntu 18.04

[531] % z3release model_validate=true small.smt2
sat
(error "line 22 column 10: an invalid model was generated")
(
  (define-fun q () Bool
    true)
  (define-fun g () Bool
    true)
  (define-fun d () Bool
    true)
  (define-fun i () Bool
    true)
  (define-fun n () Bool
    true)
  (define-fun m () Bool
    true)
  (define-fun s () Bool
    true)
  (define-fun e () Bool
    true)
  (define-fun r () Bool
    true)
  (define-fun h () Bool
    true)
  (define-fun f () Bool
    true)
  (define-fun b () Int
    7)
  (define-fun j () Bool
    true)
  (define-fun l () Bool
    true)
  (define-fun t () Int
    18)
  (define-fun k () Bool
    true)
  (define-fun c () Int
    2)
  (define-fun a () Int
    0)
  (define-fun p () Int
    0)
  (define-fun o () Bool
    false)
)
[532] % cat small.smt2
(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c () Int)
(declare-fun d () Bool)
(declare-fun e () Bool)
(declare-fun f () Bool)
(declare-fun g () Bool)
(declare-fun h () Bool)
(declare-fun i () Bool)
(declare-fun j () Bool)
(declare-fun k () Bool)
(declare-fun l () Bool)
(declare-fun m () Bool)
(declare-fun n () Bool)
(declare-fun o () Bool)
(declare-fun p () Int)
(declare-fun q () Bool)
(declare-fun r () Bool)
(declare-fun s () Bool)
(declare-fun t () Int)
(assert (and j (< 0 t 31) f q (<= 0 a 1) (<= 0 c 3) (> (* b t) 0) l (<= 0 p 1) e d (or o (> 0 (- c a (* 2 p)))) g k m h n s r i))
(check-sat)
(get-model)