1 2 3 4 5 6 7 8 9 10 11
; 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)