1 files changed, 34 insertions, 0 deletions
diff --git a/Test/floats/float19.bpl b/Test/floats/float19.bpl
new file mode 100644
index 00000000..c3a42e6b
--- /dev/null
+++ b/Test/floats/float19.bpl
@@ -0,0 +1,34 @@
+//Translation from feedback_diverge.c
+//Should give an error
+//Not sure on this one...
+
+procedure main() returns () {
+	var A : float;
+	var B : float;
+	var X : float;
+	var i : int;
+	var rand : int;
+	
+	A := fp(0);
+	B := fp(0);
+	
+	i := 0;
+	while (i < 3600000) {
+		
+		havoc rand;
+		if (rand != 0) {
+			havoc X;
+			assume(X >= fp(-20) && X <= fp(20));
+		}
+		else {
+			X := B;
+		}
+		
+		B := B - (B * fp(2.0) - A - X) * fp(.005);
+		A := X;
+		
+		i := i + 1;
+	}
+	
+	assert(A >= fp(-100) && A <= fp(100));
+}
+\ No newline at end of file