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
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
|
ControlStructures.dfy(8,2): Error: missing case in case statement: Purple
Execution trace:
(0,0): anon0
(0,0): anon6_Else
(0,0): anon7_Else
(0,0): anon8_Then
ControlStructures.dfy(8,2): Error: missing case in case statement: Blue
Execution trace:
(0,0): anon0
(0,0): anon6_Else
(0,0): anon7_Else
(0,0): anon8_Else
(0,0): anon9_Then
ControlStructures.dfy(17,2): Error: missing case in case statement: Purple
Execution trace:
(0,0): anon0
(0,0): anon6_Else
(0,0): anon7_Else
(0,0): anon8_Then
ControlStructures.dfy(46,4): Error: missing case in case statement: Red
Execution trace:
(0,0): anon0
(0,0): anon8_Then
(0,0): anon9_Else
(0,0): anon10_Then
ControlStructures.dfy(54,2): Error: missing case in case statement: Red
Execution trace:
(0,0): anon0
(0,0): anon9_Else
(0,0): anon10_Else
(0,0): anon11_Else
(0,0): anon12_Else
(0,0): anon13_Then
ControlStructures.dfy(75,2): Error: alternative cases fail to cover all possibilties
Execution trace:
(0,0): anon0
(0,0): anon5_Else
ControlStructures.dfy(218,17): Error: assertion violation
Execution trace:
(0,0): anon0
ControlStructures.dfy(197,3): anon59_LoopHead
(0,0): anon59_LoopBody
ControlStructures.dfy(197,3): anon60_Else
ControlStructures.dfy(197,3): anon61_Else
ControlStructures.dfy(201,5): anon62_LoopHead
(0,0): anon62_LoopBody
ControlStructures.dfy(201,5): anon63_Else
ControlStructures.dfy(201,5): anon64_Else
(0,0): anon68_Then
ControlStructures.dfy(213,9): anon69_LoopHead
(0,0): anon69_LoopBody
ControlStructures.dfy(213,9): anon70_Else
(0,0): anon71_Then
ControlStructures.dfy(235,20): Error: assertion violation
Execution trace:
(0,0): anon0
ControlStructures.dfy(197,3): anon59_LoopHead
(0,0): anon59_LoopBody
ControlStructures.dfy(197,3): anon60_Else
ControlStructures.dfy(197,3): anon61_Else
ControlStructures.dfy(201,5): anon62_LoopHead
(0,0): anon62_LoopBody
ControlStructures.dfy(201,5): anon63_Else
ControlStructures.dfy(201,5): anon64_Else
(0,0): anon68_Then
ControlStructures.dfy(213,9): anon69_LoopHead
(0,0): anon69_LoopBody
ControlStructures.dfy(213,9): anon70_Else
ControlStructures.dfy(213,9): anon71_Else
(0,0): anon72_Then
(0,0): after_0_0_3_0_0_0
ControlStructures.dfy(224,7): anon74_LoopHead
(0,0): anon74_LoopBody
ControlStructures.dfy(224,7): anon75_Else
ControlStructures.dfy(224,7): anon76_Else
(0,0): anon78_Then
(0,0): anon38
(0,0): anon83_Then
(0,0): anon52
ControlStructures.dfy(238,29): Error: assertion violation
Execution trace:
(0,0): anon0
ControlStructures.dfy(197,3): anon59_LoopHead
(0,0): anon59_LoopBody
ControlStructures.dfy(197,3): anon60_Else
ControlStructures.dfy(197,3): anon61_Else
ControlStructures.dfy(201,5): anon62_LoopHead
(0,0): anon62_LoopBody
ControlStructures.dfy(201,5): anon63_Else
ControlStructures.dfy(201,5): anon64_Else
(0,0): anon65_Then
(0,0): anon84_Then
(0,0): anon85_Then
(0,0): anon56
ControlStructures.dfy(241,16): Error: assertion violation
Execution trace:
(0,0): anon0
ControlStructures.dfy(197,3): anon59_LoopHead
(0,0): anon59_LoopBody
ControlStructures.dfy(197,3): anon60_Else
ControlStructures.dfy(197,3): anon61_Else
ControlStructures.dfy(201,5): anon62_LoopHead
(0,0): anon62_LoopBody
ControlStructures.dfy(201,5): anon63_Else
ControlStructures.dfy(201,5): anon64_Else
(0,0): anon68_Then
ControlStructures.dfy(213,9): anon69_LoopHead
(0,0): anon69_LoopBody
ControlStructures.dfy(213,9): anon70_Else
ControlStructures.dfy(213,9): anon71_Else
(0,0): anon72_Then
(0,0): after_0_0_3_0_0_0
ControlStructures.dfy(224,7): anon74_LoopHead
(0,0): anon74_LoopBody
ControlStructures.dfy(224,7): anon75_Else
ControlStructures.dfy(224,7): anon76_Else
(0,0): anon79_Then
(0,0): anon82_Then
(0,0): anon86_Then
(0,0): anon58
Dafny program verifier finished with 22 verified, 10 errors
|
