-
Notifications
You must be signed in to change notification settings - Fork 2
/
08.tst.smt2
93 lines (70 loc) · 1.26 KB
/
08.tst.smt2
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
(set-logic QF_SHID)
(set-info :source |
James Brotherston, Nikos Gorogiannis, and Rasmus Petersen
A Generic Cyclic Theorem Prover. APLAS, 2012.
https://github.com/ngorogiannis/cyclist
|)
(set-info :smt-lib-version 2.0)
(set-info :category "crafted")
(set-info :status unsat)
(set-info :version "2014-05-31")
; Sorts for locations, one by cell sort
(declare-sort RefGTyp 0)
; Types of cells in the heap
(declare-datatypes (
(GTyp 0)
) (
((c_GTyp (f0 RefGTyp) (f1 RefGTyp) ))
)
)
; Type of heap
(declare-heap (RefGTyp GTyp)
)
(define-fun-rec BSLL ((x RefGTyp)(y RefGTyp)) Bool
(or
(and
(= x y)
(_ emp RefGTyp GTyp)
)
(exists ((xp RefGTyp)(yp RefGTyp))
(and
(distinct (as nil RefGTyp) xp)
(sep
(pto xp (c_GTyp yp y ))
(BSLL x xp )
)
)
)
)
)
(define-fun-rec DLL ((x RefGTyp)(y RefGTyp)(z RefGTyp)(w RefGTyp)) Bool
(or
(and
(= x y)
(= z w)
(_ emp RefGTyp GTyp)
)
(exists ((zp RefGTyp))
(and
(distinct (as nil RefGTyp) x)
(sep
(pto x (c_GTyp zp w ))
(DLL zp y z x )
)
)
)
)
)
(check-sat)
;; variables
(declare-const x RefGTyp)
(declare-const y RefGTyp)
(declare-const z RefGTyp)
(declare-const w RefGTyp)
(assert
(DLL x y z w )
)
(assert (not
(BSLL z w )
))
(check-sat)