; @author Jonas Schöpf
; Ctrl example from examples/vidal2.ctrs
(format LCTRS :smtlib 2.6)
(theory Ints)
(sort Unit)
(fun i' (-> Int Unit))
(fun f (-> Int Unit))
(fun i (-> Int Unit))
(fun h' (-> Int Unit))
(fun h (-> Int Unit))
(fun g (-> Int Unit))
(fun end Unit)
(fun start Unit)

(rule (i' x) (f x))
(rule (i x) (i' (+ x 1)))
(rule (h' x) (f x))
(rule (h x) (h' (- x 12)))
(rule (g x) (i x) :guard (not (> x 2)))
(rule (g x) (h x) :guard (> x 2))
(rule (f x) end :guard (not (> x 0)))
(rule (f x) (g x) :guard (> x 0))
(rule start (f input))