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

(rule (sum1 n) (return (div (* n (+ n 1)) 2)) :guard (not (< n 0)) :vars ((n Int)))
(rule (sum1 n) (return 0) :guard (< n 0) :vars ((n Int)))
