; @author Jonas Schöpf
; Ctrl example from examples/student/sum06.ctrs
(format LCTRS :smtlib 2.6)
(theory Ints)
(sort Unit)
(fun sum1 (-> Int Unit))
(fun return (-> Int Unit))

(rule (sum1 n) (return (div (* n (+ n 1)) 2)) :guard (not (< n 0)) :var ((n Int)))
(rule (sum1 n) (return 0) :guard (< n 0) :var ((n Int)))