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

(rule (v n a1 a2 sum i) (return sum) :guard (not (< i n)) :vars ((n Int) (a1 Int) (a2 Int) (sum Int) (i Int)))
(rule (v n a1 a2 sum i) (v n (+ a1 a2) a1 (+ a1 a2) (+ i 1)) :guard (< i n) :vars ((n Int) (a1 Int) (a2 Int) (sum Int) (i Int)))
(rule (u n a1 a2 sum i) (return sum) :guard (not (and (> n 0) (< n 47))) :vars ((n Int) (a1 Int) (a2 Int) (sum Int) (i Int)))
(rule (u n a1 a2 sum i) (v n a1 a2 1 1) :guard (and (> n 0) (< n 47)) :vars ((n Int) (a1 Int) (a2 Int) (sum Int) (i Int)))
(rule (fastfib n) (u n 1 0 0 rnd) :vars ((n Int) (rnd Int)))