(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)))