(meta-info (comment "Ctrl example from examples-transformed/vidal2.ctrs"))
(format LCTRS :logic QF_LIA)
(fun i' 1 :sort (Int Unit))
(fun f 1 :sort (Int Unit))
(fun i 1 :sort (Int Unit))
(fun h' 1 :sort (Int Unit))
(fun h 1 :sort (Int Unit))
(fun g 1 :sort (Int Unit))
(fun end 0 :sort (Unit))
(fun start 0 :sort (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))