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

(rule (u1 x i z) z :guard (not (<= i x)))
(rule (u2 x i j z) (u1 x (+ i 1) z) :guard (not (< j i)))
(rule (u2 x i j z) (u2 x i (+ j 1) (+ z 1)) :guard (< j i))
(rule (u1 x i z) (u2 x i 0 z) :guard (<= i x))
(rule (sum2 x) (u1 x 0 0))
(rule (sum x) (+ x (sum (- x 1))) :guard (< 0 x))
(rule (sum x) 0 :guard (<= x 0))