From bb5395b35dcea5078c9b38a2f091f26256faac34 Mon Sep 17 00:00:00 2001 From: Dietrich Date: Mon, 20 Jul 2015 22:27:32 -0600 Subject: Float type now works correctly for simple variable declaration and comparison. --- float_test3.bpl | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) (limited to 'float_test3.bpl') diff --git a/float_test3.bpl b/float_test3.bpl index 1b70ebf4..e93e7df7 100644 --- a/float_test3.bpl +++ b/float_test3.bpl @@ -1,6 +1,3 @@ procedure F() returns () { - var x : float; - var y : float; - y := x - x; - assert y == x; + assert fp(5) == fp(5 8 23); } \ No newline at end of file -- cgit v1.2.3