; @author Jonas Schöpf
; Ctrl example from examples/student/fib08.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 a b c d) (return d) :guard (not (<= c n)))
(rule (v n a b c d) (v n b (+ a b) (+ c 1) (+ a b)) :guard (<= c n))
(rule (u n a b c d) (v n a b 2 d) :guard (and (not (< n 0)) (not (= n 1))) :var ((n Int)))
(rule (u n a b c d) (return 1) :guard (and (not (< n 0)) (= n 1)) :var ((n Int)))
(rule (u n a b c d) (return 0) :guard (< n 0))
(rule (fastfib n) (u n 0 1 rnd3 rnd4))