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

(rule (test x) (test y) :guard (and (> x 0) (= x (+ y 1))))
(rule (sum x) (+ x (sum (- x 1))) :guard (< 0 x))
(rule (sum 0) 0)
(rule (sum x) 0 :guard (< x 0))