-
Notifications
You must be signed in to change notification settings - Fork 2
/
clones-07-e07.tptp.smt2
142 lines (122 loc) · 2.72 KB
/
clones-07-e07.tptp.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
138
139
140
141
142
(set-logic QF_SHLS)
(set-info :source |
A. Rybalchenko and J. A. Navarro Perez.
[Separation Logic + Superposition Calculus = Heap Theorem Prover]
[PLDI 2011]
http://navarroj.com/research/papers.html#pldi11
|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status sat)
(set-info :version "2014-05-28")
; Sorts for locations, one by cell sort
(declare-sort RefSll_t 0)
; Types of cells in the heap
(declare-datatypes (
(Sll_t 0)
) (
((c_Sll_t (next RefSll_t) ))
)
)
; Type of heap
(declare-heap (RefSll_t Sll_t)
)
(define-fun-rec ls ((in RefSll_t)(out RefSll_t)) Bool
(or
(and
(= in out)
(_ emp RefSll_t Sll_t)
)
(exists ((u RefSll_t))
(and
(distinct in out)
(sep
(pto in (c_Sll_t u ))
(ls u out )
)
)
)
)
)
(check-sat)
;; variables
(declare-const x0 RefSll_t)
(declare-const x1 RefSll_t)
(declare-const x2 RefSll_t)
(declare-const x3 RefSll_t)
(declare-const x4 RefSll_t)
(declare-const x5 RefSll_t)
(declare-const x6 RefSll_t)
(declare-const x7 RefSll_t)
(declare-const x8 RefSll_t)
(declare-const x9 RefSll_t)
(declare-const x10 RefSll_t)
(declare-const x11 RefSll_t)
(declare-const x12 RefSll_t)
(declare-const x13 RefSll_t)
(declare-const x14 RefSll_t)
(declare-const x15 RefSll_t)
(declare-const x16 RefSll_t)
(declare-const x17 RefSll_t)
(declare-const x18 RefSll_t)
(declare-const x19 RefSll_t)
(declare-const x20 RefSll_t)
(declare-const x21 RefSll_t)
(declare-const x22 RefSll_t)
(declare-const x23 RefSll_t)
(declare-const x24 RefSll_t)
(declare-const x25 RefSll_t)
(assert
(and
(= (as nil RefSll_t) (as nil RefSll_t))
(distinct (as nil RefSll_t) x1)
(distinct (as nil RefSll_t) x2)
(distinct (as nil RefSll_t) x4)
(distinct (as nil RefSll_t) x5)
(distinct (as nil RefSll_t) x7)
(distinct (as nil RefSll_t) x8)
(distinct (as nil RefSll_t) x10)
(distinct (as nil RefSll_t) x11)
(distinct (as nil RefSll_t) x13)
(distinct (as nil RefSll_t) x14)
(distinct (as nil RefSll_t) x16)
(distinct (as nil RefSll_t) x17)
(distinct (as nil RefSll_t) x19)
(distinct (as nil RefSll_t) x20)
(sep
(ls x19 x20 )
(pto x20 (c_Sll_t x19 ))
(ls x16 x17 )
(pto x17 (c_Sll_t x16 ))
(ls x13 x14 )
(pto x14 (c_Sll_t x13 ))
(ls x10 x11 )
(pto x11 (c_Sll_t x10 ))
(ls x7 x8 )
(pto x8 (c_Sll_t x7 ))
(ls x4 x5 )
(pto x5 (c_Sll_t x4 ))
(ls x1 x2 )
(pto x2 (c_Sll_t x1 ))
)
)
)
(assert (not
(sep
(ls x21 x20 )
(pto x20 (c_Sll_t x21 ))
(ls x18 x17 )
(pto x17 (c_Sll_t x18 ))
(ls x15 x14 )
(pto x14 (c_Sll_t x15 ))
(ls x12 x11 )
(pto x11 (c_Sll_t x12 ))
(ls x9 x8 )
(pto x8 (c_Sll_t x9 ))
(ls x6 x5 )
(pto x5 (c_Sll_t x6 ))
(ls x3 x2 )
(pto x2 (c_Sll_t x3 ))
)
))
(check-sat)