diff options
Diffstat (limited to 'float_test2.bpl')
| -rw-r--r-- | float_test2.bpl | 16 |
1 files changed, 12 insertions, 4 deletions
diff --git a/float_test2.bpl b/float_test2.bpl index 956ac757..da74909b 100644 --- a/float_test2.bpl +++ b/float_test2.bpl @@ -1,5 +1,13 @@ -procedure F() returns () { - var x : float(11 53); - var y : float(11 53); - assert x == y; +//Translation from addsub_float_exact.c +//Should Verify +procedure main() returns () { + var x : float; + var y : float; + var z : float; + var r : float; + x := fp(1000000); + y := x + fp(1); + z := x - fp(1); + r := y - z; + assert r == fp(2); }
\ No newline at end of file |