/
spaguetti-17-e01.tptp.smt2
117 lines (99 loc) · 1.99 KB
/
spaguetti-17-e01.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
(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)
(assert
(and
(= (as nil RefSll_t) (as nil RefSll_t))
(distinct x6 x11)
(distinct x6 x14)
(distinct x3 x8)
(distinct x3 x15)
(distinct x7 x8)
(distinct x14 x16)
(distinct x8 x11)
(distinct x8 x15)
(distinct x1 x14)
(distinct x13 x15)
(distinct x10 x11)
(distinct x10 x13)
(distinct x5 x16)
(distinct x5 x9)
(sep
(ls x13 x5 )
(ls x13 x2 )
(ls x10 x3 )
(ls x1 x10 )
(ls x4 x12 )
(ls x2 x15 )
(ls x2 x17 )
(ls x2 x16 )
(ls x12 x16 )
(ls x9 x14 )
(ls x7 x1 )
(ls x3 x9 )
(ls x6 x2 )
)
)
)
(check-sat)