blob: b65251ca7997fa6c8f6016ae7730f57b3966085a (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
|
; EXPECT: sat
(set-option :incremental false)
(set-logic ALL)
(declare-fun x () (Set (Tuple (Tuple Int Int) (Tuple Int Int))))
(declare-fun y () (Set (Tuple (Tuple Int Int) (Tuple Int Int))))
(declare-fun z () (Set (Tuple Int Int)))
(declare-fun w () (Set (Tuple Int Int)))
(declare-fun a () (Tuple Int Int))
(declare-fun b () (Tuple Int Int))
(declare-fun c () (Tuple (Tuple Int Int) (Tuple Int Int)))
(assert (not (= a b)))
(assert (set.member a z))
(assert (set.member b z))
(assert (set.member (tuple a b) x))
(assert (set.member (tuple b a) x))
(assert (set.member c x))
(assert (and (not (= c (tuple a b))) (not (= c (tuple b a)))))
(check-sat)
|
