diff options
| author |  Rustan Leino <unknown> | 2014-02-10 20:36:10 -0800 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2014-02-10 20:36:10 -0800 |
| commit | 32f7e8341013b32c3cdc3548b2d6826a9013f7d1 (patch) | |
| tree | 986973fcfa53e24e0a3e3f24176fd090cd8c515e /Test | |
| parent | 087b8f5366d279eef5c7979ca93ced3080f77888 (diff) | |
Updated test suite after a Boogie bug fix for reals
Diffstat (limited to 'Test')
| -rw-r--r-- | Test/dafny0/Answer | 5 | ||||
| -rw-r--r-- | Test/dafny0/RealTypes.dfy | 2 |
2 files changed, 5 insertions, 2 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 863d749c..29f7b8cc 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -157,8 +157,11 @@ Execution trace: (0,0): anon0
RealTypes.dfy(10,23): anon3_Else
(0,0): anon2
+RealTypes.dfy(19,12): Error: assertion violation
+Execution trace:
+ (0,0): anon0
-Dafny program verifier finished with 5 verified, 3 errors
+Dafny program verifier finished with 4 verified, 4 errors
-------------------- Definedness.dfy --------------------
Definedness.dfy(8,7): Error: possible division by zero
diff --git a/Test/dafny0/RealTypes.dfy b/Test/dafny0/RealTypes.dfy index 95da5ac0..c2d88074 100644 --- a/Test/dafny0/RealTypes.dfy +++ b/Test/dafny0/RealTypes.dfy @@ -16,7 +16,7 @@ method R3() { ghost var x := 1.5;
ghost var y := real(3);
assert x == y / 2.0000000;
- assert x == y / 2.000000000000000000000000001; // Should error
+ assert x == y / 2.000000000000000000000000001; // error
}
// Check that real value in decreases clause doesn't scare Dafny
|