(meta-info (comment "Ctrl example from examples-transformed/student/fib11.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 pre1 pre2 val i) (return val) :guard (and (not (<= i n)) (not (< val 0))) :vars ((n Int) (pre1 Int) (pre2 Int) (val Int) (i Int)))
(rule (v n pre1 pre2 val i) (return -1) :guard (and (not (<= i n)) (< val 0)) :vars ((n Int) (pre1 Int) (pre2 Int) (val Int) (i Int)))
(rule (v n pre1 pre2 val i) (v n (+ pre1 pre2) pre1 (+ pre1 pre2) (+ i 1)) :guard (<= i n) :vars ((n Int) (pre1 Int) (pre2 Int) (val Int) (i Int)))
(rule (u n pre1 pre2 val i) (v n pre1 pre2 val 2) :guard (and (not (<= n 0)) (not (= n 1))) :vars ((n Int) (pre1 Int) (pre2 Int) (val Int) (i Int)))
(rule (u n pre1 pre2 val i) (return 1) :guard (and (not (<= n 0)) (= n 1)) :vars ((n Int) (pre1 Int) (pre2 Int) (val Int) (i Int)))
(rule (u n pre1 pre2 val i) (return 0) :guard (<= n 0) :vars ((n Int) (pre1 Int) (pre2 Int) (val Int) (i Int)))
(rule (fastfib n) (u n 1 0 0 rnd) :vars ((n Int) (rnd Int)))