diff options
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
|