; @author Jonas Schöpf
; @doi 10.1007/978-3-642-40885-4_24
; Example 5
(format LCTRS :smtlib 2.6)
(theory Ints)
(fun sum (-> Int Int))

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