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

(rule (u_6 x) x :guard (>= x 0) :var ((x Int)))
(rule (u_6 x) 0 :guard (< x 0) :var ((x Int)))
(rule (f1 x) (u_6 x) :guard (<= x 0) :var ((x Int)))
(rule (u_1 w_1) (u_6 (+ w_1 1)) :var ((w_1 Int)))
(rule (f1 x) (u_1 (f1 (- x 1))) :guard (> x 0) :var ((x Int)))