; @author Jonas Schöpf
; Ctrl example from examples/student/fib02.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 i r o t) (return r) :guard (not (<= i n)))
(rule (v n i r o t) (v n (+ i 1) (+ r o) r r) :guard (<= i n))
(rule (u n i r o t) (v n 2 1 0 t) :guard (distinct n 0) :var ((n Int)))
(rule (u 0 i r o t) (return 0))
(rule (fastfib n) (u n rnd0 rnd1 rn2 rnd3))