; @author Jonas Schöpf
; Ctrl example from examples/sum.ctrs
(format LCTRS :smtlib 2.6)
(theory Ints)
(fun sum (-> Int Int))

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