1 files changed, 21 insertions, 21 deletions
diff --git a/Test/floats/float11.bpl b/Test/floats/float11.bpl
index 424c5a2d..de148424 100644
--- a/Test/floats/float11.bpl
+++ b/Test/floats/float11.bpl
@@ -1,22 +1,22 @@
-// RUN: %boogie -proverWarnings:1 "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-
-function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_INT(int) returns (float32);
-function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_REAL(real) returns (float32);
-
-procedure main() returns () {
-	var tick : float32;
-	var time : float32;
-	var i: int;
-	
-	tick := TO_FLOAT32_INT(1)/TO_FLOAT32_INT(10);
-	time := TO_FLOAT32_INT(0);
-	
-	i := 0;
-	while (i < 10)
-	{
-		time := time + tick;
-		i := i + 1;
-	}
-	assert time == TO_FLOAT32_INT(1);
+// RUN: %boogie -proverWarnings:1 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_INT(int) returns (float24e8);
+function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_REAL(real) returns (float24e8);
+
+procedure main() returns () {
+	var tick : float24e8;
+	var time : float24e8;
+	var i: int;
+	
+	tick := TO_FLOAT32_INT(1)/TO_FLOAT32_INT(10);
+	time := TO_FLOAT32_INT(0);
+	
+	i := 0;
+	while (i < 10)
+	{
+		time := time + tick;
+		i := i + 1;
+	}
+	assert time == TO_FLOAT32_INT(1);
 }
 \ No newline at end of file