blob: b5c38542ff030c975ac6b6922a49d3449aa7aef0 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
|
InliningAndLoops.bpl(14,5): Error BP5001: This assertion might not hold.
Execution trace:
InliningAndLoops.bpl(7,10): anon0#3
InliningAndLoops.bpl(8,3): anon4_LoopHead#3
InliningAndLoops.bpl(10,5): anon4_LoopBody#3
InliningAndLoops.bpl(10,5): anon4_LoopBody$1#3
InliningAndLoops.bpl(8,3): anon4_LoopHead#2
InliningAndLoops.bpl(10,5): anon4_LoopBody#2
InliningAndLoops.bpl(10,5): anon4_LoopBody$1#2
InliningAndLoops.bpl(8,3): anon4_LoopHead#1
InliningAndLoops.bpl(8,3): anon4_LoopDone#3
InliningAndLoops.bpl(14,5): anon5_Then#3
Boogie program verifier finished with 0 verified, 1 error
|