blob: f4203e5eca40758b3d849f57ac246efb5d2bdd64 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
|
; EXPECT: unsat
(set-option :incremental false)
(set-logic ALL)
(declare-fun x () (Set (Tuple Int Int)))
(declare-fun y () (Set (Tuple Int Int)))
(declare-datatypes ((unit 0)) (((u))))
(declare-fun w () (Set (Tuple Int unit)))
(declare-fun z () (Set (Tuple unit Int)))
(assert (let ((_let_1 (rel.join w z))) (let ((_let_2 (rel.join x y))) (and (= _let_2 _let_1) (= _let_2 (rel.transpose _let_1))))))
(assert (set.member (tuple 0 1) (rel.join x y)))
(declare-fun t () Int)
(assert (and (>= t 0) (<= t 1)))
(declare-fun s () Int)
(assert (and (>= s 0) (<= s 1)))
(assert (= (+ s t) 1))
(assert (set.member (tuple s u) w))
(assert (not (set.member (tuple u t) z)))
(check-sat)
|
