; @author Jonas Schöpf
; Ctrl example from examples/sumreduce.ctrs
(format LCTRS :smtlib 2.6)
(theory Ints)
(sort Unit)
(fun test (-> Int Unit))
(fun sum (-> 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))