1 2 3 4 5 6 7 8 9 10
; COMMAND-LINE: --quiet (set-logic ALL) (set-info :status sat) (declare-fun A () (Bag Int)) (declare-fun a () Int) (assert (not (= A (as emptybag (Bag Int))))) (assert (= (bag.choose A) 10)) (assert (= a (bag.choose A))) (assert (exists ((x Int)) (and (= x (bag.choose A)) (= x a)))) (check-sat)