; @author Jonas Schöpf
; Ctrl example from examples/student/fib03.ctrs
(format LCTRS :smtlib 2.6)

(theory Ints)

(sort Unit)

(fun return (-> Int Unit))
(fun v (-> Int Int Int Int Unit))
(fun u (-> Int Int Int Int Unit))
(fun fastfib (-> Int Unit))

(rule (v x i p q) (return q) :guard (not (< i x)))
(rule (v x i p q) (v x (+ i 1) (+ p q) p) :guard (< i x))
(rule (u x i p q) (v x 1 p q) :guard (and (not (= x 0)) (not (= x 1))) :var ((x Int)))
(rule (u x i p q) (return 1) :guard (and (not (= x 0)) (= x 1)) :var ((x Int)))
(rule (u x i p q) (return 0) :guard (= x 0) :var ((x Int)))
(rule (fastfib x) (u x rnd 1 0))