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

(rule (u_8 w_3) w_3 :var ((w_3 Int)))
(rule (u_5 w_2) (u_8 (f1 w_2)) :var ((w_2 Int)))
(rule (f1 a) (u_5 (f1 (+ a 11))) :guard (<= a 100) :var ((a Int)))
(rule (f1 a) (- a 10) :guard (> a 100) :var ((a Int)))