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

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