1 files changed, 43 insertions, 0 deletions
diff --git a/Test/floats/test12.bpl b/Test/floats/test12.bpl
new file mode 100644
index 00000000..c733b9f4
--- /dev/null
+++ b/Test/floats/test12.bpl
@@ -0,0 +1,43 @@
+//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