(meta-info (comment "Ctrl example from examples-transformed/student/fib02.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 i r o t) (return r) :guard (not (<= i n)) :vars ((n Int) (i Int) (r Int) (o Int) (t Int)))
(rule (v n i r o t) (v n (+ i 1) (+ r o) r r) :guard (<= i n) :vars ((n Int) (i Int) (r Int) (o Int) (t Int)))
(rule (u n i r o t) (v n 2 1 0 t) :guard (distinct n 0) :vars ((n Int) (i Int) (r Int) (o Int) (t Int)))
(rule (u 0 i r o t) (return 0) :vars ((i Int) (r Int) (o Int) (t Int)))
(rule (fastfib n) (u n rnd0 rnd1 rn2 rnd3) :vars ((n Int) (rnd0 Int) (rnd1 Int) (rn2 Int) (rnd3 Int)))