; @author Jonas Schöpf
; Ctrl example from examples/student/fib01.ctrs
(format LCTRS :smtlib 2.6)
(theory Ints)
(sort Unit)
(fun w2 (-> Unit Unit Unit))
(fun return (-> Int Unit))
(fun badfib (-> Int Unit))

(rule (w2 (return x) (return y)) (return (+ x y)) :var ((x Int) (y Int)))
(rule (badfib x) (w2 (badfib (- x 1)) (badfib (- x 2))) :guard (> x 1) :var ((x Int)))
(rule (badfib x) (return 1) :guard (= x 1) :var ((x Int)))
(rule (badfib x) (return 1) :guard (<= x 0) :var ((x Int)))