(meta-info (comment "Ctrl example from examples-transformed/sum.ctrs")) (format LCTRS :logic QF_LIA) (fun sum 1 :sort (Int Int)) (rule (sum x) (+ x (sum (- x 1))) :guard (<= 0 (- x 1))) (rule (sum x) 0 :guard (<= x 0))