verification of loop invariant

Feb 8, 2016 at 3:16 PM
We are trying to write a program that verifies matrix multiplication using dafny,
we can't understand why it won't verify our code and why the invariant won't hold.
here is the link to our code :
Feb 10, 2016 at 10:37 AM
Edited Feb 13, 2016 at 11:14 AM
I put an answer on stackoverflow

The stackoverflow question got deleted so here is the answer on my blog: