; @author Jonas Schöpf
; Ctrl example from examples/student/sum01.ctrs
(format LCTRS :smtlib 2.6)
(theory Ints)
(sort Result)
(fun return (-> Int Result))
(fun w (-> Int Result Result))
(fun sum (-> Int Result))

(rule (w x (return y)) (return (+ x y)) :var ((x Int) (y Int)))
(rule (sum x) (w x (sum (- x 1))) :guard (<= 0 (- x 1)) :var ((x Int)))
(rule (sum x) (return 0) :guard (<= x 0) :var ((x Int)))