blob: 0452f42dbb81766d3c07e67bb5faa315348b17ac (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
|
Bug132.dfy(33,29): Error: receiver argument must be allocated in the state in which the function is invoked
Execution trace:
(0,0): anon0
(0,0): anon24_Then
Bug132.dfy(34,29): Error: receiver argument must be allocated in the state in which the function is invoked
Execution trace:
(0,0): anon0
(0,0): anon25_Then
Bug132.dfy(37,36): Error: argument must be allocated in the state in which the function is invoked
Execution trace:
(0,0): anon0
(0,0): anon26_Then
Bug132.dfy(41,29): Error: receiver argument must be allocated in the state in which the function is invoked
Execution trace:
(0,0): anon0
(0,0): anon27_Then
Dafny program verifier finished with 3 verified, 4 errors
|
