1 2 3 4 5 6 7 8 9
; EXPECT: unsat (set-logic ALL) (set-option :incremental false) (set-option :finite-model-find true) (set-option :fmf-bound-int true) (declare-fun X () (Set Int)) (assert (= (set.card X) 3)) (assert (forall ((z Int)) (=> (set.member z X) (and (> z 0) (< z 2))))) (check-sat-assuming ( (forall ((z Int)) (=> (set.member z X) (> z 0))) ))