/
bolognesa-18-e10.tptp.smt2
126 lines (106 loc) · 2.17 KB
/
bolognesa-18-e10.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
(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)
(assert
(and
(= (as nil RefSll_t) (as nil RefSll_t))
(sep
(pto x18 (c_Sll_t x4 ))
(ls x11 x18 )
(pto x14 (c_Sll_t x5 ))
(pto x6 (c_Sll_t x18 ))
(pto x8 (c_Sll_t x1 ))
(pto x15 (c_Sll_t x9 ))
(pto x16 (c_Sll_t x2 ))
(pto x2 (c_Sll_t x15 ))
(pto x5 (c_Sll_t x17 ))
(ls x10 x17 )
(pto x4 (c_Sll_t x17 ))
(pto x1 (c_Sll_t x10 ))
(pto x9 (c_Sll_t x6 ))
(pto x12 (c_Sll_t x3 ))
(pto x17 (c_Sll_t x18 ))
(pto x3 (c_Sll_t x12 ))
(ls x13 x15 )
(ls x7 x14 )
)
)
)
(assert (not
(sep
(ls x13 x15 )
(ls x12 x3 )
(ls x11 x18 )
(ls x7 x14 )
(ls x3 x12 )
(ls x16 x2 )
(ls x8 x1 )
(ls x14 x17 )
(ls x1 x18 )
(ls x2 x18 )
(ls x18 x17 )
)
))
(check-sat)