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

(sort Unit)
(fun start Unit)
(fun f (-> Int  Unit))
(fun product (-> Unit Unit  Unit))

(rule (f  x) (product  (f  y) (f  z)) :guard (and (and (and (and (> x y) (> y 0)) (> x z)) (> z 0)) (= x (* y z))))
(rule start (f  input))