Necessary assume command(s): s0, s2, s3

Boogie program verifier finished with 3 verified, 0 errors