(set-logic ALL_SUPPORTED)
(set-info :status sat)
(declare-datatypes () ((D (A (a Int)))))
(declare-fun x1 () D)
(declare-fun S () (Set D))
(declare-fun P (D) Bool)
(assert (member x1 S))
(assert (=> (member (A 0) S) (P x1)))
(check-sat)