[766] % z3 small.smt2
sat
(error "line 10 column 10: an invalid model was generated")
[767] % 
[767] % cat small.smt2
(set-option :model_validate true)
(set-option :smt.arith.solver 4)
(declare-fun a () Int)
(declare-fun b (Int) Bool)
(declare-fun c (Int) Bool)
(push)
(assert (or (= a 0) (b 0)))
(assert (c 0))
(assert (not (c a)))
(check-sat)
[768] %