1 files changed, 0 insertions, 36 deletions
diff --git a/Test/floats/test18.bpl b/Test/floats/test18.bpl
deleted file mode 100644
index 71eb5286..00000000
--- a/Test/floats/test18.bpl
+++ /dev/null
@@ -1,36 +0,0 @@
-//Translation from rlim_exit.c
-//Should verify
-//Unary - unsupported float operations (on my end)...
-
-procedure main() returns () {
-	var X : float;
-	var Y : float;
-	var S : float;
-	var R : float;
-	var D : float;
-	var i : int;
-	
-	Y := fp(0);
-	
-	i := 0;
-	while (i < 100000) {
-		havoc X;
-		havoc D;
-		assume(X >= fp(-128) && X <= fp(128));
-		assume(D >= fp(0) && D <= fp(16));
-		
-		S := Y;
-		Y := X;
-		R := X - S;
-		if (R <= fp(0)-D) {
-			Y := S - D;
-		}
-		else if(R >= D) {
-			Y := S + D;
-		}
-		
-		i := i + 1;
-	}
-	
-	assert(Y >= fp(-129) && Y <= fp(129));
-}
-\ No newline at end of file