[536] % z3 small.smt2
sat
(model 
 (define-fun a () Int
  0)
 (define-fun b () Int
  0)
)
[537] % cat small.smt2
(declare-fun a () Int)
(declare-fun b () Int)
(assert (= (= a 0) (= b 1)))
(assert (>= b 0))
(minimize 0)
(check-sat)
(get-model)
[538] %