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

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

(rule (log x y) (lif (and (>= x y) (> y 1.0)) x y))
(rule (lif true x y) (+ 1.0 (log (/ x y) y)))
(rule (lif false x y) 0.0)