summaryrefslogtreecommitdiff
path: root/float_test5.bpl
diff options
context:
space:
mode:
authorGravatar Checkmate50 <dgeisler50@gmail.com>2015-09-17 03:14:27 -0600
committerGravatar Checkmate50 <dgeisler50@gmail.com>2015-09-17 03:14:27 -0600
commit28a20e6eba2919e008f70874b4c12a3ce7ad049c (patch)
tree58050f22ea944eb07620195303d757424f50b2a9 /float_test5.bpl
parentbb5395b35dcea5078c9b38a2f091f26256faac34 (diff)
Added initial support for float addition
Diffstat (limited to 'float_test5.bpl')
-rw-r--r--float_test5.bpl4
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