[698] % z3 small.smt2
sat
[699] % cvc4 -q small.smt2
unsat
[700] % 
[700] % cat small.smt2
(define-funs-rec ((a () Int) (b ((c Int)) Bool))
 (0 (ite (< c 0) false (ite (= c 0) true (b (- 2))))))
(assert (b 7))
(check-sat)
[701] %