; @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)) :var ((a Int) (b Int) (c Int)))
(rule (v a b c) (return c) :guard (not (>= b a)) :var ((a Int) (b Int) (c Int)))
(rule (v a b c) (v a (- b 1) (+ c b)) :guard (>= b a) :var ((a Int) (b Int) (c Int)))
(rule (u a b c) (v a b c) :guard (< a b) :var ((a Int) (b Int) (c Int)))
(rule (sum2 a b) (u a b 0) :var ((a Int) (b Int)))