From 28a20e6eba2919e008f70874b4c12a3ce7ad049c Mon Sep 17 00:00:00 2001
From: Checkmate50 <dgeisler50@gmail.com>
Date: Thu, 17 Sep 2015 03:14:27 -0600
Subject: Added initial support for float addition

---
 float_test5.bpl | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'float_test5.bpl')

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
-- 
cgit v1.2.3