Dafny program verifier finished with 2 verified, 0 errors Program compiled successfully Running... map[0 := 1] map[0 := 1]