(meta-info (comment "Ctrl example from examples-transformed/student/fib12.ctrs"))
(format LCTRS :logic QF_LIA)

(fun return 1 :sort (Int  Unit))
(fun fastfib 1 :sort (Int  Unit))
(fun v 5 :sort (Int Int Int Int Int  Unit))
(fun u 5 :sort (Int Int Int Int Int  Unit))

(rule (v  num a b c i) (return  c) :guard (not (< i num)))
(rule (v  num a b c i) (v  num b (+  a b) (+  a b) (+  i 1)) :guard (< i num))
(rule (u  num a b c i) (v  num a b c 0) :guard (and (not (= num 1)) (not (= num 2))))
(rule (u  num a b c i) (return  1) :guard (and (not (= num 1)) (= num 2)))
(rule (u  num a b c i) (return  1) :guard (= num 1))
(rule (fastfib  num) (u  num 1 1 0 rnd))