summaryrefslogtreecommitdiff
path: root/Test/floats/float8.bpl
diff options
context:
space:
mode:
Diffstat (limited to 'Test/floats/float8.bpl')
-rw-r--r--Test/floats/float8.bpl8
1 files changed, 4 insertions, 4 deletions
diff --git a/Test/floats/float8.bpl b/Test/floats/float8.bpl
index 25c08e4d..bfb3b9e9 100644
--- a/Test/floats/float8.bpl
+++ b/Test/floats/float8.bpl
@@ -5,9 +5,9 @@ procedure main() returns () {
var y : float24e8;
var z : float24e8;
var r : float24e8;
- x := 0e40f24e8;
- y := x + 0e0f24e8;
- z := x - 0e0f24e8;
+ x := 0e167f24e8;
+ y := x + 0e127f24e8;
+ z := x - 0e127f24e8;
r := y - z;
- assert r == 0e1f24e8;
+ assert r == 0e128f24e8;
} \ No newline at end of file