(meta-info (comment "Ctrl example from examples-transformed/llreve/llreve_rec_inlininga.ctrs"))
(format LCTRS :logic QF_LIA)
(fun u_15 1 :sort (Int Int))
(fun f2 1 :sort (Int Int))
(fun u_10 1 :sort (Int Int))

(rule (u_15 x) x :guard (>= x 0) :vars ((x Int)))
(rule (u_15 x) 0 :guard (< x 0) :vars ((x Int)))
(rule (f2 x) (u_15 x) :guard (<= x 1) :vars ((x Int)))
(rule (u_10 w_2) (u_15 (+ w_2 2)) :vars ((w_2 Int)))
(rule (f2 x) (u_10 (f2 (- x 2))) :guard (> x 1) :vars ((x Int)))
