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

(rule (sum1 x) (+ x (sum1 (- x 1))) :guard (<= 0 (- x 1)))
(rule (sum1 x) 0 :guard (<= x 0))