From 59052004251c655e06951eb4615938259fdf4844 Mon Sep 17 00:00:00 2001 From: Checkmate50 Date: Tue, 19 Jul 2016 12:33:21 -0600 Subject: Modified the float tests to match the updated syntax --- Test/floats/float8.bpl | 24 ++++++++++++------------ 1 file changed, 12 insertions(+), 12 deletions(-) (limited to 'Test/floats/float8.bpl') 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 -- cgit v1.2.3