1 files changed, 33 insertions, 4 deletions
diff --git a/float_test9.bpl b/float_test9.bpl
index 7423a3a0..c3a42e6b 100644
--- a/float_test9.bpl
+++ b/float_test9.bpl
@@ -1,5 +1,34 @@
- procedure F() returns () {
-	var x : float;
-	x := fp (0.5 23 8);
-	assert x == fp (0 -1);
+//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