path: root/test/regress/regress1/sets/choose4.smt2

; COMMAND-LINE: --quiet
(set-logic ALL)
(set-info :status sat)
(set-option :produce-models true)
(declare-fun A () (Set Int))
(declare-fun a () Int)
(assert (not (= A (as set.empty (Set Int)))))
(assert (set.member 10 A))
(assert (= a (set.choose A)))
;(assert (exists ((x Int)) (and (= x (set.choose A)) (= x a))))
(check-sat)