(meta-info (comment "Ctrl example from examples-transformed/quad1.ctrs"))
(format LCTRS :logic QF_LIA)
(fun u 3 :sort (Int Int Int Int))
(fun twice 1 :sort (Int Int))
(fun quad 1 :sort (Int Int))

(rule (u x i z) z :guard (>= i x))
(rule (u x i z) (u x (+ i 1) (+ z 2)) :guard (< i x))
(rule (twice x) (u x 0 0))
(rule (quad x) (+ (twice x) (twice x)))