blob: 18435c3096b939e7e0453f8da5b14ef391409216 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
|
// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
lemma largeIsLarge()
ensures 0x8000000000000000 > 0 {
}
lemma SmallIsSmall()
ensures -0x8000000000000000 < 0 {
}
lemma ShouldCancelOut()
ensures -0x8000000000000000 + 0x8000000000000000 == 0 {
}
|
