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

(rule (sum n m) 0 :guard (< n m))
(rule (sum n m) (+ n (sum (- n 1) m)) :guard (>= n m))