invalid model on a QF_LIA formula

[zhendongsu]

[511] % z3release model_validate=true small.smt2
failed to validate: (or a!0 a!1 (not ((_ pbge 4 1 1 2 2) b!2 b!3 (not c!4) (not c!5))))
sat
(error "line 8 column 40: an invalid model was generated")
(
  (define-fun c () Int
    0)
  (define-fun a () Int
    0)
  (define-fun b () Int
    0)
)
[512] % cat small.smt2
(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c () Int)
(assert (>= a 0))
(assert (>= b 0))
(assert (>= c 0))
(assert (> (+ (* 3 a) (- b) (* 2 c)) 0))
(check-sat-using (then add-bounds qfnia))
(get-model)