(meta-info (comment "Ctrl example from examples-transformed/student/fib01.ctrs"))
(format LCTRS :logic QF_LIA)
(fun return 1 :sort (Int Unit))
(fun u 4 :sort (Int Int Int Int Unit))
(fun fastfib 1 :sort (Int Unit))

(rule (u num f0 f1 f2) (return f1) :guard (not (>= num 2)) :vars ((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) :vars ((num Int) (f0 Int) (f1 Int) (f2 Int)))
(rule (fastfib num) (u num 1 1 rnd) :vars ((num Int) (rnd Int)))