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

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

(rule (v  num a b c i) (return  c) :guard (not (< i num)))
(rule (v  num a b c i) (v  num b (+  a b) (+  a b) (+  i 1)) :guard (< i num))
(rule (u  num a b c i) (v  num a b c 0) :guard (and (not (= num 1)) (not (= num 2))))
(rule (u  num a b c i) (return  1) :guard (and (not (= num 1)) (= num 2)))
(rule (u  num a b c i) (return  1) :guard (= num 1))
(rule (fastfib  num) (u  num 1 1 0 rnd))