Statements.3.expect

text.dfy(12,2): Warning: this loop has no body (loop frame: i, a, $Heap)
text.dfy(16,2): Error: assertion might not hold
text.dfy(18,2): Error: assertion might not hold

Dafny program verifier finished with 1 verified, 2 errors