; @author Jonas Schöpf
; Ctrl example from examples/student/fib02.ctrs
(format LCTRS :smtlib 2.6)

(theory Ints)

(sort Unit)

(fun return (-> Int Unit))
(fun w (-> Unit Unit Unit))
(fun fib (-> Int Unit))

(rule (w (return x) (return y)) (return (+ x y)))
(rule (fib x) (w (fib (- x 1)) (fib (- x 2))) :guard (>= (- x 2) 0))
(rule (fib 1) (return 1))
(rule (fib x) (return 0) :guard (<= x 0))