(meta-info (comment "Ctrl example from examples-transformed/student/sum02.ctrs"))
(format LCTRS :logic QF_LIA)
(fun ditch_globals 1 :sort (Unit Result))
(fun return 3 :sort (Int Int Int Unit))
(fun return1 1 :sort (Int Result))
(fun u 3 :sort (Int Int Int Unit))
(fun sum1 3 :sort (Int Int Int Unit))

(rule (ditch_globals (return x y z)) (return1 z) :vars ((x Int) (y Int) (z Int)))
(rule (u num i answer) (return i answer answer) :guard (not (<= i num)) :vars ((num Int) (i Int) (answer Int)))
(rule (u num i answer) (u num (+ i 1) (+ answer i)) :guard (<= i num) :vars ((num Int) (i Int) (answer Int)))
(rule (sum1 num i answer) (u num 0 0) :guard (not (< num 0)) :vars ((num Int) (i Int) (answer Int)))
(rule (sum1 num i answer) (return i answer 0) :guard (< num 0) :vars ((num Int) (i Int) (answer Int)))