; @author Jonas Schöpf
; Ctrl example from examples/student/fib10.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 fi fp fn i) (return fi) :guard (not (< i n)))
(rule (v n fi fp fn i) (v n (+ fi fp) fi (+ fi fp) (+ i 1)) :guard (< i n))
(rule (u n fi fp fn i) (v n fi fp fn 1) :guard (not (<= n 0)))
(rule (u n fi fp fn i) (return 0) :guard (<= n 0))
(rule (fastfib n) (u n 1 0 rnd1 rnd2))