Skip to content

Commit 2657c50

Browse files
committed
Update test-substitution
1 parent 38187b1 commit 2657c50

File tree

3 files changed

+60
-175
lines changed

3 files changed

+60
-175
lines changed

booster/test/rpc-integration/test-substitutions/README.md

+1
Original file line numberDiff line numberDiff line change
@@ -39,6 +39,7 @@ NB: Booster applies the given substitution before performing any action.
3939
- starts from `concrete-subst`
4040
- with two equations that have circular dependencies: `Y = 1 +Int X`, `X = Y -Int 1`
4141
- leading to end state with `X == 42` from the `ensures`-clause
42+
- `booster-dev` return a trivial circular constraint `X ==Int X`
4243
* `state-symbolic-bottom-predicate.execute`
4344
- starts from `symbolic-subst`
4445
- with an equation that is instantly false: `X = 1 +Int X`

booster/test/rpc-integration/test-substitutions/response-circular-equations.booster-dev

+59-24
Original file line numberDiff line numberDiff line change
@@ -175,34 +175,69 @@
175175
}
176176
},
177177
"second": {
178-
"tag": "App",
179-
"name": "Lbl'UndsPlus'Int'Unds'",
180-
"sorts": [],
181-
"args": [
182-
{
183-
"tag": "DV",
184-
"sort": {
185-
"tag": "SortApp",
186-
"name": "SortInt",
187-
"args": []
188-
},
189-
"value": "1"
190-
},
191-
{
192-
"tag": "EVar",
193-
"name": "X",
194-
"sort": {
195-
"tag": "SortApp",
196-
"name": "SortInt",
197-
"args": []
198-
}
199-
}
200-
]
178+
"tag": "DV",
179+
"sort": {
180+
"tag": "SortApp",
181+
"name": "SortInt",
182+
"args": []
183+
},
184+
"value": "43"
201185
}
202186
}
203187
]
204188
}
189+
},
190+
"predicate": {
191+
"format": "KORE",
192+
"version": 1,
193+
"term": {
194+
"tag": "Equals",
195+
"argSort": {
196+
"tag": "SortApp",
197+
"name": "SortBool",
198+
"args": []
199+
},
200+
"sort": {
201+
"tag": "SortApp",
202+
"name": "SortGeneratedTopCell",
203+
"args": []
204+
},
205+
"first": {
206+
"tag": "DV",
207+
"sort": {
208+
"tag": "SortApp",
209+
"name": "SortBool",
210+
"args": []
211+
},
212+
"value": "true"
213+
},
214+
"second": {
215+
"tag": "App",
216+
"name": "Lbl'UndsEqlsEqls'Int'Unds'",
217+
"sorts": [],
218+
"args": [
219+
{
220+
"tag": "EVar",
221+
"name": "X",
222+
"sort": {
223+
"tag": "SortApp",
224+
"name": "SortInt",
225+
"args": []
226+
}
227+
},
228+
{
229+
"tag": "EVar",
230+
"name": "X",
231+
"sort": {
232+
"tag": "SortApp",
233+
"name": "SortInt",
234+
"args": []
235+
}
236+
}
237+
]
238+
}
239+
}
205240
}
206241
}
207242
}
208-
}
243+
}

booster/test/rpc-integration/test-substitutions/response-symbolic-bottom-predicate.booster-dev

-151
This file was deleted.

0 commit comments

Comments
 (0)