; @author Jonas Schöpf
; Ctrl example from examples/student/sum02.ctrs
(format LCTRS :smtlib 2.6)
(theory Ints)
(sort Unit)
(sort Result)
(fun ditch_globals (-> Unit Result))
(fun return (-> Int Int Int Unit))
(fun return1 (-> Int Result))
(fun u (-> Int Int Int Unit))
(fun sum1 (-> Int Int Int Unit))

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