-------------------- contractinfer --------------------

Boogie program verifier finished with 2 verified, 0 errors

-------------------- flpydisk --------------------

Boogie program verifier finished with 2 verified, 0 errors