; @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)) :var ((x Int) (i Int) (p Int) (q Int)))
(rule (v x i p q) (v x (+ i 1) (+ p q) p) :guard (< i x) :var ((x Int) (i Int) (p Int) (q Int)))
(rule (u x i p q) (v x 1 p q) :guard (and (not (= x 0)) (not (= x 1))) :var ((x Int) (i Int) (p Int) (q Int)))
(rule (u x i p q) (return 1) :guard (and (not (= x 0)) (= x 1)) :var ((x Int) (i Int) (p Int) (q Int)))
(rule (u x i p q) (return 0) :guard (= x 0) :var ((x Int) (i Int) (p Int) (q Int)))
(rule (fastfib x) (u x rnd 1 0) :var ((x Int) (rnd Int)))