(meta-info (comment "Ctrl example from examples-transformed/student/sumfrom01.ctrs"))
(format LCTRS :logic QF_LIA)
(fun return 1 :sort (Int Unit))
(fun tmp 2 :sort (Int Unit Unit))
(fun sumfrom 2 :sort (Int Int Unit))

(rule (tmp m (return n)) (return (+ m n)) :vars ((m Int) (n Int)))
(rule (sumfrom m n) (tmp n (sumfrom m (- n 1))) :guard (<= m n) :vars ((m Int) (n Int)))
(rule (sumfrom m n) (return 0) :guard (> m n) :vars ((m Int) (n Int)))