; @author Jonas Schöpf
; Ctrl example from examples/notsn.ctrs
(format LCTRS :smtlib 2.6)
(theory Ints)
(fun f (-> Int Int Int))

(rule (f x y) 0 :guard (or (or (>= (- x 1) y) (< (- x 1) 0)) (< y 0)))
(rule (f x y) 0 :guard (or (< x 0) (<= y 0)))
(rule (f 0 y) 0 :guard (>= y 0))
(rule (f x y) (f (- x 1) y) :guard (and (and (< (- x 1) y) (>= (- x 1) 0)) (>= y 0)))