Skip to content

Commit 67bf458

Browse files
geo2ageo2a
committed
Update integration tests
Separate booster-dev and kore-rpc-booster responses for collectiontest.k Separate kore-rpc-dev and kore-rpc-booster responses for test-vacuous Separate kore-rpc-dev and kore-rpc-booster responses for test-diamond Separate kore-rpc-dev and kore-rpc-booster responses for test-substitution Remove redundant booster-dev responses for test-substitutions Update test-3934-smt Update test-issue3764-vacuous-branch Update output for test-log-simplify-json
1 parent b2c3850 commit 67bf458

25 files changed

+73870
-11848
lines changed

‎booster/test/rpc-integration/test-3934-smt/response-008.json

Lines changed: 2290 additions & 2114 deletions
Large diffs are not rendered by default.

‎booster/test/rpc-integration/test-collectiontest/response-from-12.booster-dev

Lines changed: 594 additions & 0 deletions
Large diffs are not rendered by default.

‎booster/test/rpc-integration/test-collectiontest/response-from-12.json

Lines changed: 10 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -93,7 +93,7 @@
9393
"name": "SortInt",
9494
"args": []
9595
},
96-
"value": "6"
96+
"value": "4"
9797
}
9898
]
9999
}
@@ -132,7 +132,7 @@
132132
"name": "SortInt",
133133
"args": []
134134
},
135-
"value": "7"
135+
"value": "5"
136136
}
137137
]
138138
}
@@ -171,7 +171,7 @@
171171
"name": "SortInt",
172172
"args": []
173173
},
174-
"value": "4"
174+
"value": "6"
175175
}
176176
]
177177
}
@@ -210,7 +210,7 @@
210210
"name": "SortInt",
211211
"args": []
212212
},
213-
"value": "5"
213+
"value": "7"
214214
}
215215
]
216216
}
@@ -249,7 +249,7 @@
249249
"name": "SortInt",
250250
"args": []
251251
},
252-
"value": "2"
252+
"value": "1"
253253
}
254254
]
255255
}
@@ -288,7 +288,7 @@
288288
"name": "SortInt",
289289
"args": []
290290
},
291-
"value": "3"
291+
"value": "2"
292292
}
293293
]
294294
}
@@ -327,7 +327,7 @@
327327
"name": "SortInt",
328328
"args": []
329329
},
330-
"value": "1"
330+
"value": "3"
331331
}
332332
]
333333
}
@@ -366,7 +366,7 @@
366366
"name": "SortInt",
367367
"args": []
368368
},
369-
"value": "8"
369+
"value": "12"
370370
}
371371
]
372372
}
@@ -405,7 +405,7 @@
405405
"name": "SortInt",
406406
"args": []
407407
},
408-
"value": "9"
408+
"value": "8"
409409
}
410410
]
411411
}
@@ -444,7 +444,7 @@
444444
"name": "SortInt",
445445
"args": []
446446
},
447-
"value": "12"
447+
"value": "9"
448448
}
449449
]
450450
}

‎booster/test/rpc-integration/test-diamond/response-infeasible-branching.json

Lines changed: 33 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -67,13 +67,13 @@
6767
"sorts": [],
6868
"args": [
6969
{
70-
"tag": "DV",
70+
"tag": "EVar",
71+
"name": "X",
7172
"sort": {
7273
"tag": "SortApp",
7374
"name": "SortInt",
7475
"args": []
75-
},
76-
"value": "42"
76+
}
7777
}
7878
]
7979
},
@@ -96,14 +96,14 @@
9696
]
9797
}
9898
},
99-
"substitution": {
99+
"predicate": {
100100
"format": "KORE",
101101
"version": 1,
102102
"term": {
103103
"tag": "Equals",
104104
"argSort": {
105105
"tag": "SortApp",
106-
"name": "SortInt",
106+
"name": "SortBool",
107107
"args": []
108108
},
109109
"sort": {
@@ -112,25 +112,41 @@
112112
"args": []
113113
},
114114
"first": {
115-
"tag": "EVar",
116-
"name": "X",
117-
"sort": {
118-
"tag": "SortApp",
119-
"name": "SortInt",
120-
"args": []
121-
}
122-
},
123-
"second": {
124115
"tag": "DV",
125116
"sort": {
126117
"tag": "SortApp",
127-
"name": "SortInt",
118+
"name": "SortBool",
128119
"args": []
129120
},
130-
"value": "42"
121+
"value": "true"
122+
},
123+
"second": {
124+
"tag": "App",
125+
"name": "Lbl'UndsEqlsEqls'Int'Unds'",
126+
"sorts": [],
127+
"args": [
128+
{
129+
"tag": "EVar",
130+
"name": "X",
131+
"sort": {
132+
"tag": "SortApp",
133+
"name": "SortInt",
134+
"args": []
135+
}
136+
},
137+
{
138+
"tag": "DV",
139+
"sort": {
140+
"tag": "SortApp",
141+
"name": "SortInt",
142+
"args": []
143+
},
144+
"value": "42"
145+
}
146+
]
131147
}
132148
}
133149
}
134150
}
135151
}
136-
}
152+
}

‎booster/test/rpc-integration/test-substitutions/response-symbolic-two-substitutions.booster-dev renamed to ‎booster/test/rpc-integration/test-diamond/response-infeasible-branching.kore-rpc-dev

Lines changed: 16 additions & 63 deletions
Original file line numberDiff line numberDiff line change
@@ -2,8 +2,9 @@
22
"jsonrpc": "2.0",
33
"id": 1,
44
"result": {
5-
"reason": "vacuous",
6-
"depth": 0,
5+
"reason": "terminal-rule",
6+
"depth": 3,
7+
"rule": "TEST.BD",
78
"state": {
89
"term": {
910
"format": "KORE",
@@ -46,7 +47,7 @@
4647
"name": "SortState",
4748
"args": []
4849
},
49-
"value": "symbolic-subst"
50+
"value": "d"
5051
}
5152
]
5253
},
@@ -66,45 +67,13 @@
6667
"sorts": [],
6768
"args": [
6869
{
69-
"tag": "EVar",
70-
"name": "X",
70+
"tag": "DV",
7171
"sort": {
7272
"tag": "SortApp",
7373
"name": "SortInt",
7474
"args": []
75-
}
76-
}
77-
]
78-
},
79-
{
80-
"tag": "App",
81-
"name": "Lbl'-LT-'jnt'-GT-'",
82-
"sorts": [],
83-
"args": [
84-
{
85-
"tag": "App",
86-
"name": "Lbl'UndsPlus'Int'Unds'",
87-
"sorts": [],
88-
"args": [
89-
{
90-
"tag": "DV",
91-
"sort": {
92-
"tag": "SortApp",
93-
"name": "SortInt",
94-
"args": []
95-
},
96-
"value": "1"
97-
},
98-
{
99-
"tag": "EVar",
100-
"name": "X",
101-
"sort": {
102-
"tag": "SortApp",
103-
"name": "SortInt",
104-
"args": []
105-
}
106-
}
107-
]
75+
},
76+
"value": "42"
10877
}
10978
]
11079
},
@@ -144,40 +113,24 @@
144113
},
145114
"first": {
146115
"tag": "EVar",
147-
"name": "Y",
116+
"name": "X",
148117
"sort": {
149118
"tag": "SortApp",
150119
"name": "SortInt",
151120
"args": []
152121
}
153122
},
154123
"second": {
155-
"tag": "App",
156-
"name": "Lbl'UndsPlus'Int'Unds'",
157-
"sorts": [],
158-
"args": [
159-
{
160-
"tag": "DV",
161-
"sort": {
162-
"tag": "SortApp",
163-
"name": "SortInt",
164-
"args": []
165-
},
166-
"value": "1"
167-
},
168-
{
169-
"tag": "EVar",
170-
"name": "X",
171-
"sort": {
172-
"tag": "SortApp",
173-
"name": "SortInt",
174-
"args": []
175-
}
176-
}
177-
]
124+
"tag": "DV",
125+
"sort": {
126+
"tag": "SortApp",
127+
"name": "SortInt",
128+
"args": []
129+
},
130+
"value": "42"
178131
}
179132
}
180133
}
181134
}
182135
}
183-
}
136+
}

0 commit comments

Comments
 (0)