Dafny program verifier finished with 56 verified, 0 errors
Program compiled successfully
Running...

400
320
40
41
42
9
9
a is null
a and b are equal
good world order
given array is non-null