1 files changed, 0 insertions, 43 deletions
diff --git a/Test/floats/test12.bpl b/Test/floats/test12.bpl
deleted file mode 100644
index c733b9f4..00000000
--- a/Test/floats/test12.bpl
+++ /dev/null
@@ -1,43 +0,0 @@
-//Translation from inv_Newton.c
-//Should Verify
-//Unfinished code!
-
-procedure inv(float(11 53)) returns(float(11 53)) {
-	var z : float(11 53);
-	var t : float(11 53);
-	var t : float(11 53);
-	
-	
-}
-
-procedure main() returns () {
-	var t : float(11 53);
-	var t : float(11 53);
-	
-	min[0] := fp(5);
-	min[1] := fp(10);
-	min[2] := fp(12);
-	min[3] := fp(30);
-	min[4] := fp(150);
-	
-	max[0] := fp(10);
-	max[1] := fp(12);
-	max[2] := fp(30);
-	max[3] := fp(150);
-	max[4] := fp(300);
-	
-	havoc t;
-	assume(t >= min[0] && t <= max[4]);
-	
-	i := 0;
-	while (i < 5) {
-		if (t <= max[i]) {
-			break;
-		}
-		i := i + 1;
-	}
-	
-	z := (t - min[i]) / (max[i] - min[i]);
-	
-	assert(z >= fp(0) && z <= fp(1));
-}
-\ No newline at end of file