search

dafny-lang / dafny

Dafny is a verification-aware programming language
https://dafny.org
Other
2.93k stars 262 forks source link

Crash with bad trigger #5898

Open ajewellamz opened 2 weeks ago

ajewellamz commented 2 weeks ago

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