blob: a22f2a44f290a38a6b5b10f380929a2d4f263419 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
|
; EXPECT: (error "Extended set operators are not supported in default mode, try --sets-ext.")
; EXIT: 1
(set-logic ALL)
(declare-fun a () Int)
(declare-fun f ((Set Bool)) Int)
(declare-fun s () (Set Bool))
(assert (member true s))
(assert (member false s))
(assert (= a (f (as univset (Set Bool)))))
(assert (= (f (as emptyset (Set Bool))) 1))
(assert (= (f (singleton true)) 2))
(assert (= (f (singleton false)) 3))
(assert (= (f (union (singleton true) (singleton false))) 4))
(check-sat)
|
