/
skl3-vc09.smt2
137 lines (106 loc) · 2.16 KB
/
skl3-vc09.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
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
(set-logic QF_SHID)
(set-info :source |
C. Enea, O. Lengal, M. Sighireanu, and T. Vojnar
[Compositional Entailment Checking for a Fragment of Separation Logic]
http://www.liafa.univ-paris-diderot.fr/spen
|)
(set-info :smt-lib-version 2.0)
(set-info :category "crafted")
(set-info :status unsat)
; Sorts for locations, one by cell sort
(declare-sort RefSL3_t 0)
; Types of cells in the heap
(declare-datatypes (
(SL3_t 0)
) (
((c_SL3_t (n1 RefSL3_t) (n2 RefSL3_t) (n3 RefSL3_t) ))
)
)
; Type of heap
(declare-heap (RefSL3_t SL3_t)
)
(define-fun-rec skl1 ((hd RefSL3_t)(ex RefSL3_t)) Bool
(or
(and
(= hd ex)
(_ emp RefSL3_t SL3_t)
)
(exists ((tl RefSL3_t))
(and
(distinct hd ex)
(sep
(pto hd (c_SL3_t tl (as nil RefSL3_t) (as nil RefSL3_t) ))
(skl1 tl ex )
)
)
)
)
)
(define-fun-rec skl2 ((hd RefSL3_t)(ex RefSL3_t)) Bool
(or
(and
(= hd ex)
(_ emp RefSL3_t SL3_t)
)
(exists ((tl RefSL3_t)(Z1 RefSL3_t))
(and
(distinct hd ex)
(sep
(pto hd (c_SL3_t Z1 tl (as nil RefSL3_t) ))
(skl1 Z1 tl )
(skl2 tl ex )
)
)
)
)
)
(define-fun-rec skl3 ((hd RefSL3_t)(ex RefSL3_t)) Bool
(or
(and
(= hd ex)
(_ emp RefSL3_t SL3_t)
)
(exists ((tl RefSL3_t)(Z1 RefSL3_t)(Z2 RefSL3_t))
(and
(distinct hd ex)
(sep
(pto hd (c_SL3_t Z1 Z2 tl ))
(skl1 Z1 Z2 )
(skl2 Z2 tl )
(skl3 tl ex )
)
)
)
)
)
(check-sat)
;; variables
(declare-const x1 RefSL3_t)
(declare-const x2 RefSL3_t)
(declare-const x2_0_1 RefSL3_t)
(declare-const x2_1 RefSL3_t)
(declare-const x2_2 RefSL3_t)
(declare-const x2_2_1 RefSL3_t)
(declare-const x2_2_2 RefSL3_t)
(declare-const x3 RefSL3_t)
(declare-const x3_0_1 RefSL3_t)
(declare-const x3_1 RefSL3_t)
(declare-const x4 RefSL3_t)
(assert
(sep
(pto x2 (c_SL3_t x2_0_1 x2_1 x3 ))
(skl1 x2_0_1 x2_1 )
(skl2 x2_1 x2_2 )
(pto x2_2 (c_SL3_t x2_2_1 x3 (as nil RefSL3_t) ))
(skl1 x2_2_1 x2_2_2 )
(pto x2_2_2 (c_SL3_t x3 (as nil RefSL3_t) (as nil RefSL3_t) ))
(pto x3 (c_SL3_t x3_0_1 x3_1 x4 ))
(skl1 x3_0_1 x3_1 )
(skl2 x3_1 x4 )
(skl3 x4 (as nil RefSL3_t) )
)
)
(assert (not
(skl3 x2 (as nil RefSL3_t) )
))
(check-sat)