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

; COMMAND-LINE: --no-check-models
(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 emptyset (Set Int)))))
(assert (= (choose A) 10))
(assert (= a (choose A)))
(assert (exists ((x Int)) (and (= x (choose A)) (= x a))))
(check-sat)