summaryrefslogtreecommitdiff
path: root/Test/test2/NeverPattern.bpl.expect
blob: 3ce334aadfaffb6a28e6cbc51741a66ef7a2c04e (plain)
1
2
3
4
5
6
7
8
9
10
11
NeverPattern.bpl(18,3): Error BP5001: This assertion might not hold.
Execution trace:
    NeverPattern.bpl(17,3): anon0
NeverPattern.bpl(24,3): Error BP5001: This assertion might not hold.
Execution trace:
    NeverPattern.bpl(23,3): anon0
NeverPattern.bpl(30,3): Error BP5001: This assertion might not hold.
Execution trace:
    NeverPattern.bpl(29,3): anon0

Boogie program verifier finished with 2 verified, 3 errors