blob: 9ff80e14cdc4d0fcf7d8fa0b388ac74d4d064a24 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
|
; COMMAND-LINE: --finite-model-find
; EXPECT: sat
(set-logic ALL)
(declare-sort Atom 0)
(declare-fun p ((Set Atom) (Set Atom)) (Set Atom))
(declare-fun j ((Set Atom) (Set Atom)) (Set Atom))
(declare-fun k ((Set Atom) (Set Atom)) (Set Atom))
(declare-fun d ((Set Atom) (Set Atom)) (Set Atom))
(declare-fun a () (Set Atom))
(declare-fun n () Atom)
(declare-fun v () Atom)
(assert (forall ((b Atom) (c Atom))
(or
(member v (k (singleton n) (j (singleton b) a)))
(= (as emptyset (Set Atom)) (d (j (singleton b) a) (singleton n)))
)
)
)
(check-sat)
|
