1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
|
TypeParameters.dfy(47,21): Error: assertion violation
Execution trace:
(0,0): anon0
TypeParameters.dfy(69,26): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon3_Then
(0,0): anon2
TypeParameters.dfy(156,11): Error: assertion violation
TypeParameters.dfy(156,27): Related location
Execution trace:
(0,0): anon0
(0,0): anon20_Then
TypeParameters.dfy(156,32): anon21_Else
(0,0): anon5
TypeParameters.dfy(158,11): Error: assertion violation
TypeParameters.dfy(158,32): Related location
Execution trace:
(0,0): anon0
(0,0): anon23_Then
TypeParameters.dfy(158,37): anon24_Else
(0,0): anon11
TypeParameters.dfy(160,11): Error: assertion violation
TypeParameters.dfy(160,19): Related location
Execution trace:
(0,0): anon0
(0,0): anon25_Then
TypeParameters.dfy(162,11): Error: assertion violation
TypeParameters.dfy(147,4): Related location
TypeParameters.dfy(162,20): Related location
Execution trace:
(0,0): anon0
(0,0): anon26_Then
TypeParameters.dfy(164,11): Error: assertion violation
TypeParameters.dfy(149,7): Related location
Execution trace:
(0,0): anon0
(0,0): anon27_Then
TypeParameters.dfy(178,14): Error BP5005: This loop invariant might not be maintained by the loop.
TypeParameters.dfy(178,37): Related location
Execution trace:
(0,0): anon0
TypeParameters.dfy(171,3): anon16_LoopHead
(0,0): anon16_LoopBody
TypeParameters.dfy(171,3): anon17_Else
(0,0): anon19_Then
TypeParameters.dfy(177,3): anon20_LoopHead
(0,0): anon20_LoopBody
TypeParameters.dfy(177,3): anon21_Else
TypeParameters.dfy(177,3): anon23_Else
Dafny program verifier finished with 63 verified, 8 errors
|
