(meta-info (comment "Example 5 from Kop et al. 2013"))
(format LCTRS :logic QF_LIA)
(fun sum 1 :sort (Int Int))

(rule (sum x) 0 :guard (>= 0 x))
(rule (sum x) (+ x (sum (+ x (- 1)))) :guard (not (>= 0 x)))