Skip to content

Commit 783a9e9

Browse files
geo2ageo2a
committed
Remove attribute info from golden files
1 parent 7aae51a commit 783a9e9

26 files changed

+104
-237
lines changed

‎test/imp/sum-save-proofs-spec.k.save-proofs.kore.golden

Lines changed: 41 additions & 101 deletions
Original file line numberDiff line numberDiff line change
@@ -2,98 +2,64 @@
22
module haskell-backend-saved-claims-43943e50-f723-47cd-99fd-07104d664c6d
33
import IMP []
44
import kore []
5-
claim {} /* Spa */
5+
claim {}
66
\implies{SortGeneratedTopCell{}}(
7-
/* Spa */
87
\and{SortGeneratedTopCell{}}(
9-
/* Spa */
108
\equals{SortBool{}, SortGeneratedTopCell{}}(
11-
/* T Fn D Sfa Cl */ \dv{SortBool{}}("true"),
12-
/* T Fn D Spa */
9+
\dv{SortBool{}}("true"),
1310
Lbl'Unds-GT-Eqls'Int'Unds'{}(
14-
/* T Fn D Sfa */ VarN:SortInt{},
15-
/* T Fn D Sfa Cl */ \dv{SortInt{}}("0")
11+
VarN:SortInt{},
12+
\dv{SortInt{}}("0")
1613
)
1714
),
18-
/* T Fn D Spa */
1915
Lbl'-LT-'generatedTop'-GT-'{}(
20-
/* T Fn D Spa */
2116
Lbl'-LT-'T'-GT-'{}(
22-
/* T Fn D Spa */
2317
Lbl'-LT-'k'-GT-'{}(
24-
/* T Fn D Spa */
2518
kseq{}(
26-
/* T Fn D Sfa Cli */
27-
/* Inj: */ inj{SortStmt{}, SortKItem{}}(
28-
/* T Fn D Sfa Cl */
19+
inj{SortStmt{}, SortKItem{}}(
2920
Lblwhile'LParUndsRParUndsUnds'IMP-SYNTAX'Unds'Stmt'Unds'BExp'Unds'Block{}(
30-
/* T Fn D Sfa Cl */
3121
Lbl'BangUndsUnds'IMP-SYNTAX'Unds'BExp'Unds'BExp{}(
32-
/* T Fn D Sfa Cl */
3322
Lbl'Unds-LT-EqlsUndsUnds'IMP-SYNTAX'Unds'BExp'Unds'AExp'Unds'AExp{}(
34-
/* T Fn D Sfa Cli */
35-
/* Inj: */ inj{SortId{}, SortAExp{}}(
36-
/* T Fn D Sfa Cl */
37-
\dv{SortId{}}(/* T Fn D Sfa Cl */
23+
inj{SortId{}, SortAExp{}}(
24+
\dv{SortId{}}(
3825
"n")
3926
),
40-
/* T Fn D Sfa Cli */
41-
/* Inj: */ inj{SortInt{}, SortAExp{}}(
42-
/* T Fn D Sfa Cl */
27+
inj{SortInt{}, SortAExp{}}(
4328
\dv{SortInt{}}("0")
4429
)
4530
)
4631
),
47-
/* T Fn D Sfa Cl */
4832
Lbl'LBraUndsRBraUnds'IMP-SYNTAX'Unds'Block'Unds'Stmt{}(
49-
/* T Fn D Sfa Cl */
5033
Lbl'UndsUndsUnds'IMP-SYNTAX'Unds'Stmt'Unds'Stmt'Unds'Stmt{}(
51-
/* T Fn D Sfa Cl */
5234
Lbl'UndsEqlsUndsSClnUnds'IMP-SYNTAX'Unds'Stmt'Unds'Id'Unds'AExp{}(
53-
/* T Fn D Sfa Cl */
54-
\dv{SortId{}}(/* T Fn D Sfa Cl */
35+
\dv{SortId{}}(
5536
"sum"),
56-
/* T Fn D Sfa Cl */
5737
Lbl'UndsPlusUndsUnds'IMP-SYNTAX'Unds'AExp'Unds'AExp'Unds'AExp{}(
58-
/* T Fn D Sfa Cl */
5938
Lbl'UndsPlusUndsUnds'IMP-SYNTAX'Unds'AExp'Unds'AExp'Unds'AExp{}(
60-
/* T Fn D Sfa Cli */
61-
/* Inj: */ inj{SortId{}, SortAExp{}}(
62-
/* T Fn D Sfa Cl */
63-
\dv{SortId{}}(/* T Fn D Sfa Cl */
39+
inj{SortId{}, SortAExp{}}(
40+
\dv{SortId{}}(
6441
"sum")
6542
),
66-
/* T Fn D Sfa Cli */
67-
/* Inj: */ inj{SortId{}, SortAExp{}}(
68-
/* T Fn D Sfa Cl */
69-
\dv{SortId{}}(/* T Fn D Sfa Cl */
43+
inj{SortId{}, SortAExp{}}(
44+
\dv{SortId{}}(
7045
"n")
7146
)
7247
),
73-
/* T Fn D Sfa Cli */
74-
/* Inj: */ inj{SortId{}, SortAExp{}}(
75-
/* T Fn D Sfa Cl */
76-
\dv{SortId{}}(/* T Fn D Sfa Cl */
48+
inj{SortId{}, SortAExp{}}(
49+
\dv{SortId{}}(
7750
"n")
7851
)
7952
)
8053
),
81-
/* T Fn D Sfa Cl */
8254
Lbl'UndsEqlsUndsSClnUnds'IMP-SYNTAX'Unds'Stmt'Unds'Id'Unds'AExp{}(
83-
/* T Fn D Sfa Cl */
84-
\dv{SortId{}}(/* T Fn D Sfa Cl */
55+
\dv{SortId{}}(
8556
"n"),
86-
/* T Fn D Sfa Cl */
8757
Lbl'UndsPlusUndsUnds'IMP-SYNTAX'Unds'AExp'Unds'AExp'Unds'AExp{}(
88-
/* T Fn D Sfa Cli */
89-
/* Inj: */ inj{SortId{}, SortAExp{}}(
90-
/* T Fn D Sfa Cl */
91-
\dv{SortId{}}(/* T Fn D Sfa Cl */
58+
inj{SortId{}, SortAExp{}}(
59+
\dv{SortId{}}(
9260
"n")
9361
),
94-
/* T Fn D Sfa Cli */
95-
/* Inj: */ inj{SortInt{}, SortAExp{}}(
96-
/* T Fn D Sfa Cl */
62+
inj{SortInt{}, SortAExp{}}(
9763
\dv{SortInt{}}("-1")
9864
)
9965
)
@@ -102,101 +68,75 @@ module haskell-backend-saved-claims-43943e50-f723-47cd-99fd-07104d664c6d
10268
)
10369
)
10470
),
105-
/* T Fn D Sfa */ Var'Unds'DotVar2:SortK{}
71+
Var'Unds'DotVar2:SortK{}
10672
)
10773
),
108-
/* T Fn D Spa */
10974
Lbl'-LT-'state'-GT-'{}(
110-
/* T Fn D Spa */
111-
/* InternalMap: */ Lbl'Unds'Map'Unds'{}(
112-
/* concrete element: */ Lbl'UndsPipe'-'-GT-Unds'{}(
113-
/* Inj: */ inj{SortId{}, SortKItem{}}(
75+
Lbl'Unds'Map'Unds'{}(
76+
Lbl'UndsPipe'-'-GT-Unds'{}(
77+
inj{SortId{}, SortKItem{}}(
11478
\dv{SortId{}}("n")
11579
),
116-
/* T Fn D Spa */
117-
/* Inj: */ inj{SortInt{}, SortKItem{}}(
118-
/* T Fn D Sfa */ VarN:SortInt{}
80+
inj{SortInt{}, SortKItem{}}(
81+
VarN:SortInt{}
11982
)
12083
),
121-
/* concrete element: */ Lbl'UndsPipe'-'-GT-Unds'{}(
122-
/* Inj: */ inj{SortId{}, SortKItem{}}(
84+
Lbl'UndsPipe'-'-GT-Unds'{}(
85+
inj{SortId{}, SortKItem{}}(
12386
\dv{SortId{}}("sum")
12487
),
125-
/* T Fn D Spa */
126-
/* Inj: */ inj{SortInt{}, SortKItem{}}(
127-
/* T Fn D Sfa */ VarS:SortInt{}
88+
inj{SortInt{}, SortKItem{}}(
89+
VarS:SortInt{}
12890
)
12991
)
13092
)
13193
)
13294
),
133-
/* T Fn D Spa */
13495
Lbl'-LT-'generatedCounter'-GT-'{}(
135-
/* T Fn D Sfa */ Var'Unds'Gen0:SortInt{}
96+
Var'Unds'Gen0:SortInt{}
13697
)
13798
)
13899
),
139-
/* Spa */
140100
weakAlwaysFinally{SortGeneratedTopCell{}}(
141-
/* Spa */
142101
\exists{SortGeneratedTopCell{}}(
143102
Var'QuesUnds'Gen1:SortInt{},
144-
/* Fn Spa */
145103
Lbl'-LT-'generatedTop'-GT-'{}(
146-
/* Fn Spa */
147104
Lbl'-LT-'T'-GT-'{}(
148-
/* T Fn D Spa */
149105
Lbl'-LT-'k'-GT-'{}(
150-
/* T Fn D Sfa */ Var'Unds'DotVar2:SortK{}
106+
Var'Unds'DotVar2:SortK{}
151107
),
152-
/* Fn Spa */
153108
Lbl'-LT-'state'-GT-'{}(
154-
/* Fn Spa */
155109
Lbl'Unds'Map'Unds'{}(
156-
/* T Fn D Spa */
157110
Lbl'UndsPipe'-'-GT-Unds'{}(
158-
/* T Fn D Sfa Cli */
159-
/* Inj: */ inj{SortId{}, SortKItem{}}(
160-
/* T Fn D Sfa Cl */
161-
\dv{SortId{}}(/* T Fn D Sfa Cl */ "n")
111+
inj{SortId{}, SortKItem{}}(
112+
\dv{SortId{}}( "n")
162113
),
163-
/* T Fn D Sfa Cli */
164-
/* Inj: */ inj{SortInt{}, SortKItem{}}(
165-
/* T Fn D Sfa Cl */ \dv{SortInt{}}("0")
114+
inj{SortInt{}, SortKItem{}}(
115+
\dv{SortInt{}}("0")
166116
)
167117
),
168-
/* T Fn D Spa */
169118
Lbl'UndsPipe'-'-GT-Unds'{}(
170-
/* T Fn D Sfa Cli */
171-
/* Inj: */ inj{SortId{}, SortKItem{}}(
172-
/* T Fn D Sfa Cl */
173-
\dv{SortId{}}(/* T Fn D Sfa Cl */ "sum")
119+
inj{SortId{}, SortKItem{}}(
120+
\dv{SortId{}}( "sum")
174121
),
175-
/* T Fn D Spa */
176-
/* Inj: */ inj{SortInt{}, SortKItem{}}(
177-
/* T Fn D Spa */
122+
inj{SortInt{}, SortKItem{}}(
178123
Lbl'UndsPlus'Int'Unds'{}(
179-
/* T Fn D Sfa */ VarS:SortInt{},
180-
/* T Fn D Spa */
124+
VarS:SortInt{},
181125
Lbl'UndsStar'Int'Unds'{}(
182-
/* T Fn D Spa */
183126
Lbl'UndsPlus'Int'Unds'{}(
184-
/* T Fn D Sfa */
185127
VarN:SortInt{},
186-
/* T Fn D Sfa Cl */
187128
\dv{SortInt{}}("1")
188129
),
189-
/* T Fn D Sfa */ VarN:SortInt{}
130+
VarN:SortInt{}
190131
)
191132
)
192133
)
193134
)
194135
)
195136
)
196137
),
197-
/* T Fn D Spa */
198138
Lbl'-LT-'generatedCounter'-GT-'{}(
199-
/* T Fn D Sfa */ Var'QuesUnds'Gen1:SortInt{}
139+
Var'QuesUnds'Gen1:SortInt{}
200140
)
201141
)
202142
)

0 commit comments

Comments
 (0)