QF_UFLRA.smt2

(set-option :produce-models)
(set-logic QF_UFLRA)
(declare-sort U 0)
(declare-fun x () Real)
(declare-fun f (U) Real)
(declare-fun P (U) Bool)
(declare-fun g (U) U)
(declare-fun c () U)
(declare-fun d () U)
(assert (= (P c) (= (g c) c)))
(assert (ite (P c) (> x (f d)) (< x (f d))))
(check-sat)
(get-model)
(exit)