diff options
| author |  leino <unknown> | 2015-06-12 15:59:39 -0700 |
|---|---|---|
| committer | leino <unknown> | 2015-06-12 15:59:39 -0700 |
| commit | cd93fd9d44d0f3f178c95d97ed2c8fd9146604e4 (patch) | |
| tree | 3f55ff9ee8ae3d002663444e1fcbc9d3524a2537 /Test/dafny4 | |
| parent | 19176cf2d4ae511bcfb32ea2d417dae83861728a (diff) | |
| parent | e054e59a6deda9793b66cf78374b75f7d557bef8 (diff) | |
Merge
Diffstat (limited to 'Test/dafny4')
| -rw-r--r-- | Test/dafny4/LargeConstants.dfy | 14 | ||||
| -rw-r--r-- | Test/dafny4/LargeConstants.dfy.expect | 2 |
2 files changed, 16 insertions, 0 deletions
diff --git a/Test/dafny4/LargeConstants.dfy b/Test/dafny4/LargeConstants.dfy new file mode 100644 index 00000000..18435c30 --- /dev/null +++ b/Test/dafny4/LargeConstants.dfy @@ -0,0 +1,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 {
+}
diff --git a/Test/dafny4/LargeConstants.dfy.expect b/Test/dafny4/LargeConstants.dfy.expect new file mode 100644 index 00000000..4ef2de53 --- /dev/null +++ b/Test/dafny4/LargeConstants.dfy.expect @@ -0,0 +1,2 @@ +
+Dafny program verifier finished with 6 verified, 0 errors
|