assert(multiset(arr[..]) == multiset(arr[..arr.Length])) fails!

[btwael]

Dafny version

4.1.0

Code to produce this issue

method main() {
  var arr: array<int>;
  assert(multiset(arr[..]) == multiset(arr[..arr.Length]));
}

Command to run and resulting output

No response

What happened?

The assertion cannot be proven correct which make it more difficult to specify and verify certain type of programs (e.g. array merge).

What type of operating system are you experiencing the problem on?

Mac

[MikaelMayer]

Add assert arr[..] == arr[..arr.Length]; before and verification will pass.
I don't have a good answer why it does not pass. I just know that

arr[..] is translated into Seq#FromArray(arr)
whereas
arr[..arr.Length] is translated into Seq#Take(Seq#FromArray(arr), _System.array.Length(arr))
and there is no axiom that can be automatically instantiated that says
Seq#Take(x, Seq#Length(x)) == x
although there might be other mechanisms that can help prove this.

[btwael]

Hey @MikaelMayer, I'm aware of the workaround and thank you for explaining how things work in the background. With a small search, I added the axiom to the prelude and it helped in more sophisticated example.