; @author Jonas Schöpf
; @doi 10.1007/978-3-642-40885-4_24
; Example 14
(format LCTRS :smtlib 2.6)
(theory Ints)

(fun log (-> Int Int Int))
(fun lif (-> Bool Int Int Int))
(fun / (-> Int Int Int))

(rule (log x y) (lif (and (>= x y) (> y 1)) x y))
(rule (lif true x y) (+ 1 (log (/ x y) y)))
(rule (lif false x y) 0)
(rule (/ x y) z :guard (= x (* y z)))