From 80f3d4ed1bb221adbd3c7162acea10920b9fab73 Mon Sep 17 00:00:00 2001
From: Checkmate50 <dgeisler50@gmail.com>
Date: Wed, 23 Sep 2015 04:08:00 -0600
Subject: Modified BigFloat to avoid evaluating the floating point value before
 sending it to z3

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

(limited to 'float_test6.bpl')

diff --git a/float_test6.bpl b/float_test6.bpl
index 307da9f7..423bc45a 100644
--- a/float_test6.bpl
+++ b/float_test6.bpl
@@ -1,5 +1,5 @@
 procedure F() returns () {
 	var x : float;
-	x := fp(1) + fp(1);
-	assert x == fp(2);
+	var y : float;
+	assert (x + x) + (y + y) == fp(0);
 }
\ No newline at end of file
-- 
cgit v1.2.3