(meta-info (comment "Ctrl example from examples-transformed/student/fib09.ctrs")) (format LCTRS :logic QF_LIA) (fun return 1 :sort (Int Unit)) (fun tmp 2 :sort (Unit Unit Unit)) (fun fib 1 :sort (Int Unit)) (rule (tmp (return x) (return y)) (return (+ x y)) :vars ((x Int) (y Int))) (rule (fib x) (tmp (fib (- x 1)) (fib (- x 2))) :guard (>= (- x 2) 0) :vars ((x Int))) (rule (fib 1) (return 1)) (rule (fib x) (return 0) :guard (<= x 0) :vars ((x Int)))