1 files changed, 9 insertions, 10 deletions
diff --git a/Test/floats/float4.bpl b/Test/floats/float4.bpl
index 7bb24250..a1608572 100644
--- a/Test/floats/float4.bpl
+++ b/Test/floats/float4.bpl
@@ -1,11 +1,10 @@
-// RUN: %boogie -proverWarnings:1 "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-procedure foo() returns (r : float32) {
-	r := fp<8, 24>(NaN);
-	r := fp<8, 24>(+oo);
-	r := fp<8, 24>(-oo);
-	r := fp<8, 24>(+zero);
-	r := fp<8, 24>(-zero);
-	
-	return;
+// RUN: %boogie -proverWarnings:1 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+procedure foo() returns (r : float32) {
+	r := 0NaN8e24;
+	r := 0nan8e24;
+	r := 0+oo8e24;
+	r := 0-oo8e24;
+	
+	return;
 }
 \ No newline at end of file