-
Notifications
You must be signed in to change notification settings - Fork 2
/
spaguetti-20-e05.tptp.smt2
134 lines (116 loc) · 2.35 KB
/
spaguetti-20-e05.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
(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 unsat)
(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)
(assert
(and
(= (as nil RefSll_t) (as nil RefSll_t))
(distinct x6 x16)
(distinct x3 x7)
(distinct x3 x19)
(distinct x3 x14)
(distinct x7 x11)
(distinct x7 x18)
(distinct x7 x9)
(distinct x7 x16)
(distinct x7 x12)
(distinct x7 x14)
(distinct x2 x6)
(distinct x8 x10)
(distinct x8 x15)
(distinct x1 x10)
(distinct x1 x19)
(distinct x4 x18)
(distinct x4 x9)
(distinct x4 x17)
(distinct x4 x15)
(distinct x16 x18)
(distinct x10 x20)
(distinct x13 x17)
(distinct x5 x10)
(distinct x5 x20)
(distinct x5 x14)
(sep
(ls x5 x16 )
(ls x13 x3 )
(ls x19 x14 )
(ls x19 x1 )
(ls x16 x17 )
(ls x18 x15 )
(ls x1 x9 )
(ls x8 x9 )
(ls x20 x5 )
(ls x17 x20 )
(ls x12 x13 )
(ls x2 x11 )
(ls x9 x2 )
(ls x11 x5 )
(ls x11 x7 )
(ls x11 x4 )
)
)
)
(check-sat)