diff options
Diffstat (limited to 'Test/floats/float8.bpl')
| -rw-r--r-- | Test/floats/float8.bpl | 24 |
1 files changed, 12 insertions, 12 deletions
diff --git a/Test/floats/float8.bpl b/Test/floats/float8.bpl index 78c11a2b..25c08e4d 100644 --- a/Test/floats/float8.bpl +++ b/Test/floats/float8.bpl @@ -1,13 +1,13 @@ -// RUN: %boogie -proverWarnings:1 "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-procedure main() returns () {
- var x : float32;
- var y : float32;
- var z : float32;
- var r : float32;
- x := fp<8, 24>(3221225472bv32);
- y := x + fp<8, 24>(1bv32);
- z := x - fp<8, 24>(1bv32);
- r := y - z;
- assert r == fp<8, 24>(2bv32);
+// RUN: %boogie -proverWarnings:1 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +procedure main() returns () { + var x : float24e8; + var y : float24e8; + var z : float24e8; + var r : float24e8; + x := 0e40f24e8; + y := x + 0e0f24e8; + z := x - 0e0f24e8; + r := y - z; + assert r == 0e1f24e8; }
\ No newline at end of file |