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

(rule (v x i p q) (return q) :guard (not (< i x)) :vars ((x Int) (i Int) (p Int) (q Int)))
(rule (v x i p q) (v x (+ i 1) (+ p q) p) :guard (< i x) :vars ((x Int) (i Int) (p Int) (q Int)))
(rule (u x i p q) (v x 1 p q) :guard (and (not (= x 0)) (not (= x 1))) :vars ((x Int) (i Int) (p Int) (q Int)))
(rule (u x i p q) (return 1) :guard (and (not (= x 0)) (= x 1)) :vars ((x Int) (i Int) (p Int) (q Int)))
(rule (u x i p q) (return 0) :guard (= x 0) :vars ((x Int) (i Int) (p Int) (q Int)))
(rule (fastfib x) (u x rnd 1 0) :vars ((x Int) (rnd Int)))