(meta-info (comment "Ctrl example from examples-transformed/student/sumfrom06.ctrs"))
(format LCTRS :logic QF_LIA)
(fun u 3 :sort (Int Int Int Unit))
(fun return 1 :sort (Int Unit))
(fun v 3 :sort (Int Int Int Unit))
(fun sum2 2 :sort (Int Int Unit))

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