Crash with bad trigger

[ajewellamz]

Dafny version

4.7 4.8 4.9

Code to produce this issue

predicate method SequenceEqual<T(==)>(seq1 : seq<T>, seq2 : seq<T>, start1 : nat, start2 : nat, size : nat)
  : (ret : bool)
    requires start1 + size <= |seq1|
    requires start2 + size <= |seq2|
  {
    forall i : nat  {:trigger i} | 0 <= i < size :: seq1[start1+i] == seq2[start2+i]
  }

Command to run and resulting output

dafny verify --function-syntax 3 seqeq.dfy

Unhandled exception. System.ArgumentException

What happened?

I expected an error, but not a crash.

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

Mac