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,22): Error: assertion violation
Execution trace:
(0,0): anon0
TypeParameters.dfy(69,27): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon3_Then
(0,0): anon2
TypeParameters.dfy(156,12): Error: assertion violation
TypeParameters.dfy(156,28): Related location
Execution trace:
(0,0): anon0
(0,0): anon20_Then
TypeParameters.dfy(156,32): anon21_Else
(0,0): anon5
TypeParameters.dfy(158,12): Error: assertion violation
TypeParameters.dfy(158,33): Related location
Execution trace:
(0,0): anon0
(0,0): anon23_Then
TypeParameters.dfy(158,37): anon24_Else
(0,0): anon11
TypeParameters.dfy(160,12): Error: assertion violation
TypeParameters.dfy(160,20): Related location
Execution trace:
(0,0): anon0
(0,0): anon25_Then
TypeParameters.dfy(162,12): Error: assertion violation
TypeParameters.dfy(147,5): Related location
TypeParameters.dfy(162,21): Related location
Execution trace:
(0,0): anon0
(0,0): anon26_Then
TypeParameters.dfy(164,12): Error: assertion violation
TypeParameters.dfy(149,8): Related location
Execution trace:
(0,0): anon0
(0,0): anon27_Then
TypeParameters.dfy(178,15): Error BP5005: This loop invariant might not be maintained by the loop.
TypeParameters.dfy(178,38): 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
|
