; @author Jonas Schöpf
; @author Aart Middeldorp
; @doi 10.1007/978-3-031-38499-8_27
; Example 13
(format LCTRS :smtlib 2.6)
(theory Ints)

(fun f (-> Int Int))
(fun g (-> Int Int))
(fun a Int)

(rule (f x) z :guard (= z 3))
(rule (g (f x)) a)
(rule (g 3) a)