(set-option :produce-models true)
(get-option :produce-models)
(set-logic QF_UF)
(set-info :status sat)
(declare-sort U 0)
(declare-fun f (U) U)
(declare-fun g (U) U)
(declare-fun A () Bool)
(declare-fun x () U)
(declare-fun y () U)
(check-sat)
(get-value (x A (f x) (g y)))