(meta-info (comment "Ctrl example from examples-transformed/student/sum01.ctrs"))
(format LCTRS :logic QF_LIA)
(fun return 1 :sort (Int Result))
(fun w 2 :sort (Int Result Result))
(fun sum 1 :sort (Int Result))

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