; @author Jonas Schöpf
; Ctrl example from examples/double.ctrs
(format LCTRS :smtlib 2.6)
(theory Ints)

(fun double (-> Int Int))

(rule (double x) 0 :guard (<= x 0))
(rule (double x) (+ 2 (double (- x 1))) :guard (> x 0))