Skip to content

Commit 059a6d4

Browse files
committed
Separate kore-rpc-dev and kore-rpc-booster responses for test-diamond
1 parent aaeba30 commit 059a6d4

File tree

1 file changed

+33
-17
lines changed

1 file changed

+33
-17
lines changed

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+
}

0 commit comments

Comments
 (0)