1 2 3 4 5 6 7 8 9 10 11
; COMMAND-LINE: -q ; EXPECT: sat (set-logic ALL_SUPPORTED) (set-info :status sat) (declare-fun S () (Set Int)) (declare-fun x () Int) (assert (= (choose (singleton x)) 5)) (assert (= (singleton x) S)) (assert (is_singleton S)) (assert (is_singleton (singleton 3))) (check-sat)