test/regress/regress1/fmf/radu-quant-set.smt2


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18

; COMMAND-LINE: --fmf-bound
; EXPECT: unsat
(set-logic ALL)

(declare-const A (Set Int))
(declare-const B (Set Int))

(define-fun F () Bool
            (exists ((i Int) (j Int)) (and (distinct i j) (member i A) (member j B)))
)

(define-fun G () Bool
            (and (>= (card (union A B)) 2) (>= (card A) 1) (>= (card B) 1))
)

(assert (and G (not F)))

(check-sat)