path: root/test/regress/regress0/sets/sets-poly-nonint.smt2

(set-logic QF_UFLIRAFS)
(set-info :status sat)
(declare-fun s () (Set Real))
(declare-fun t () (Set Real))
(declare-fun r () (Set Real))
(declare-fun u () (Set Real))
(assert (set.member 1.5 t))
(assert (set.member 2.5 r))
(assert (set.member 3.5 u))
(assert (or (= s t) (= s r) (= s u)))
(check-sat)