(meta-info (comment "Ctrl example from examples-transformed/llreve/llreve_rec_inlininga.ctrs")) (format LCTRS :logic QF_LIA) (fun u_6 1 :sort (Int Int)) (fun f1 1 :sort (Int Int)) (fun u_1 1 :sort (Int Int)) (rule (u_6 x) x :guard (>= x 0) :vars ((x Int))) (rule (u_6 x) 0 :guard (< x 0) :vars ((x Int))) (rule (f1 x) (u_6 x) :guard (<= x 0) :vars ((x Int))) (rule (u_1 w_1) (u_6 (+ w_1 1)) :vars ((w_1 Int))) (rule (f1 x) (u_1 (f1 (- x 1))) :guard (> x 0) :vars ((x Int)))