; @author Jonas Schöpf
; Ctrl example from examples/student/sumfrom06.ctrs
(format LCTRS :smtlib 2.6)

(theory Ints)

(sort Unit)

(fun u (-> Int Int Int Unit))
(fun return (-> Int Unit))
(fun v (-> Int Int Int Unit))
(fun sum2 (-> Int Int Unit))

(rule (u a b c) (return c) :guard (not (< a b)))
(rule (v a b c) (return c) :guard (not (>= b a)))
(rule (v a b c) (v a (- b 1) (+ c b)) :guard (>= b a))
(rule (u a b c) (v a b c) :guard (< a b))
(rule (sum2 a b) (u a b 0))