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/dafny0/RealTypes.dfy | |
| parent | 087b8f5366d279eef5c7979ca93ced3080f77888 (diff) | |
Updated test suite after a Boogie bug fix for reals
Diffstat (limited to 'Test/dafny0/RealTypes.dfy')
| -rw-r--r-- | Test/dafny0/RealTypes.dfy | 2 |
1 files changed, 1 insertions, 1 deletions
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
|