diff options
Diffstat (limited to 'float_test.bpl')
| -rw-r--r-- | float_test.bpl | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/float_test.bpl b/float_test.bpl index fbf8e4e3..e893e098 100644 --- a/float_test.bpl +++ b/float_test.bpl @@ -1,13 +1,13 @@ //Translation from addsub_double_exact.c //Should Verify procedure main() returns () { - var x : float(11 53); - var y : float(11 53); - var z : float(11 53); - var r : float(11 53); - x := fp(10000000 11 53); - y := x + fp(1 11 53); - z := x - fp(1 11 53); + var x : float<11, 53>; + var y : float<11, 53>; + var z : float<11, 53>; + var r : float<11, 53>; + x := fp<11, 53> (10000000bv64); + y := x + fp<11, 53>(1bv64); + z := x - fp<11, 53>(1bv64); r := y - z; - assert r == fp(2 11 53); + assert r == fp<11, 53> (2bv64); }
\ No newline at end of file |