1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
|
MapOutputTypeParams.bpl(35,3): Warning: type parameter a is ambiguous, instantiating to int
MapOutputTypeParams.bpl(18,3): Error BP5001: This assertion might not hold.
Execution trace:
MapOutputTypeParams.bpl(13,9): anon0
MapOutputTypeParams.bpl(19,3): Error BP5001: This assertion might not hold.
Execution trace:
MapOutputTypeParams.bpl(13,9): anon0
MapOutputTypeParams.bpl(29,3): Error BP5001: This assertion might not hold.
Execution trace:
MapOutputTypeParams.bpl(25,9): anon0
MapOutputTypeParams.bpl(30,3): Error BP5001: This assertion might not hold.
Execution trace:
MapOutputTypeParams.bpl(25,9): anon0
MapOutputTypeParams.bpl(37,3): Error BP5001: This assertion might not hold.
Execution trace:
MapOutputTypeParams.bpl(34,8): anon0
MapOutputTypeParams.bpl(38,3): Error BP5001: This assertion might not hold.
Execution trace:
MapOutputTypeParams.bpl(34,8): anon0
Boogie program verifier finished with 0 verified, 6 errors
|
