summaryrefslogtreecommitdiff
path: root/test/regress/regress0/rec-fun-const-parse-bug.smt2
blob: a2f30eec3f3a042f02d371af04216430a144cd89 (plain) 
1
2
3
4
5
6
7
8
9
10
11
12

(set-logic ALL)
(set-info :status unsat)

(define-funs-rec (
(f () Int)
(pred ((y Int)) Bool)) (
0
(ite (< y 0) false (ite (= y 0) true (pred (- y 2))))
))

(assert (pred 5))
(check-sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback