(meta-info (comment "Ctrl example from examples-transformed/student/fib03.ctrs"))
(format LCTRS :logic QF_LIA)
(fun badfib 1 :sort (Int Unit))
(fun w 2 :sort (Unit Unit Unit))
(fun return 1 :sort (Int Unit))

(rule (badfib x) (w (badfib (- x 1)) (badfib (- x 2))) :guard (> x 3) :vars ((x Int)))
(rule (badfib x) (return 1) :guard (<= x 3) :vars ((x Int)))
(rule (w (return x) (return y)) (return (+ x y)) :vars ((x Int) (y Int)))