test/regress/regress1/quantifiers/set-choice-koikonomou.cvc.smt2


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 (= (card X) 3))
(assert (forall ((z Int)) (=> (member z X) (and (> z 0) (< z 2)))))
(check-sat-assuming ( (forall ((z Int)) (=> (member z X) (> z 0))) ))