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

(theory Reals)

(fun log (-> Real Real Real))
(fun lif (-> Real Real Real))

(rule (log x y) (lif x y))
(rule (lif x y) (+ 1.0 (log (/ x y) y)) :guard (and (>= x y) (> y 1.0)))
(rule (lif x y) 0.0 :guard (not (and (>= x y) (> y 1.0))))