(set-logic QF_UFLIRAFS)
(set-info :status sat)
(declare-fun s () (Set Real))
(declare-fun t1 () (Set Real))
(declare-fun t2 () (Set Real))
(declare-fun t3 () (Set Real))
(declare-fun r1 () (Set Real))
(declare-fun r2 () (Set Real))
(declare-fun r3 () (Set Real))
(assert (and (member 1.5 s) (member 0.0 s)))
(assert (= t1 (union s (singleton 2.5))))
(assert (= t2 (union s (singleton 2.0))))
(assert (= t3 (union r3 (singleton 2.5))))
(assert (= (intersection r1 r2) (intersection s (singleton 0.0))))
(assert (not (= r1 (as emptyset (Set Real)))))

(check-sat)