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

Boogie program verifier finished with 3 verified, 0 errors