; @author Jonas Schöpf
; Ctrl example from examples/student/fib01.ctrs
(format LCTRS :smtlib 2.6)
(theory Ints)
(sort Unit)
(fun return (-> Int Unit))
(fun u (-> Int Int Int Int Unit))
(fun fastfib (-> Int Unit))

(rule (u num f0 f1 f2) (return f1) :guard (not (>= num 2)) :var ((num Int) (f0 Int) (f1 Int) (f2 Int)))
(rule (u num f0 f1 f2) (u (- num 1) f1 (+ f1 f0) (+ f1 f0)) :guard (>= num 2) :var ((num Int) (f0 Int) (f1 Int) (f2 Int)))
(rule (fastfib num) (u num 1 1 rnd) :var ((num Int) (rnd Int)))