; @author Jonas Schöpf
; Ctrl example from examples/student/fib07.ctrs
(format LCTRS :smtlib 2.6)
(theory Ints)
(sort Unit)
(fun v (-> Int Int Int Int Int Unit))
(fun return (-> Int Unit))
(fun u (-> Int Int Int Int Int Unit))
(fun fastfib (-> Int Unit))

(rule (v n now next i tmp) (return next) :guard (not (<= i n)) :var ((n Int) (now Int) (next Int) (i Int) (tmp Int)))
(rule (v n now next i tmp) (v n next (+ next now) (+ i 1) now) :guard (<= i n) :var ((n Int) (now Int) (next Int) (i Int) (tmp Int)))
(rule (u n now next i tmp) (v n 1 1 3 tmp) :guard (and (not (<= n 0)) (not (= n 1))) :var ((n Int) (now Int) (next Int) (i Int) (tmp Int)))
(rule (u n now next i tmp) (return 1) :guard (and (not (<= n 0)) (= n 1)) :var ((n Int) (now Int) (next Int) (i Int) (tmp Int)))
(rule (u n now next i tmp) (return 0) :guard (<= n 0) :var ((n Int) (now Int) (next Int) (i Int) (tmp Int)))
(rule (fastfib n) (u n rnd1 rnd2 rnd3 rnd4) :var ((n Int) (rnd1 Int) (rnd2 Int) (rnd3 Int) (rnd4 Int)))