diff options
author | Checkmate50 <dgeisler50@gmail.com> | 2015-09-17 03:14:27 -0600 |
---|---|---|
committer | Checkmate50 <dgeisler50@gmail.com> | 2015-09-17 03:14:27 -0600 |
commit | 28a20e6eba2919e008f70874b4c12a3ce7ad049c (patch) | |
tree | 58050f22ea944eb07620195303d757424f50b2a9 /float_test5.bpl | |
parent | bb5395b35dcea5078c9b38a2f091f26256faac34 (diff) |
Added initial support for float addition
Diffstat (limited to 'float_test5.bpl')
-rw-r--r-- | float_test5.bpl | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/float_test5.bpl b/float_test5.bpl index 2f565b27..c3d279f2 100644 --- a/float_test5.bpl +++ b/float_test5.bpl @@ -1,5 +1,5 @@ procedure F() returns () { var x : float; - x := fp (0 0); - assert x == fp (0 0 8 30); + var y : float; + assert x + y == fp(0); }
\ No newline at end of file |