blob: 308fbb9afa439a93716cedd471dc315c8ef273bf (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
|
// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
// There is a bug in Dafny that causes the error from `L` to be reported at
// position 0 in this file, instead of on a curly brace.
lemma L()
ensures false {
calc { true; }
}
// Empty calc statements work fine, though:
lemma L'()
ensures false {
calc { }
}
|
