blob: 72c9ab81ef8433abc3f1450773cf5bf42ce718b3 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
|
// RUN: %dafny "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
// Dafny counts columns from 0, but Boogie from one, so for a while there were small bugs with that.
predicate P(x: int)
static method A(x:int) requires x > 0 { // error os 's'
assert (forall y: int :: P(y)); // error on '('
assert x != 1; // error on '!'
assert x in {}; // error on 'i'
}
|
