blob: f5ef1d003cd2c0655d9f366e0164b74a30fe54a4 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
|
; COMMAND-LINE: --symmetry-detect
(set-logic ALL)
(set-info :status unsat)
(declare-fun A () (Set Int))
(declare-fun B () (Set Int))
(declare-fun C () (Set Int))
(declare-fun f () Int)
(declare-fun g () Int)
(declare-fun h () Int)
(declare-fun i () Int)
(declare-fun j () Int)
(assert (subset A (insert g h i (singleton f))))
(assert (= C (setminus A B) ))
(assert (subset B A))
(assert (= C (intersection A B)))
(assert (member j C))
(check-sat)
|
