; @author Jonas Schöpf
; Ctrl example from examples/llreve/llreve_rec_inlininga.ctrs
(format LCTRS :smtlib 2.6)
(theory Ints)
(fun u_15 (-> Int Int))
(fun f2 (-> Int Int))
(fun u_10 (-> Int Int))

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