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