1 files changed, 32 insertions, 3 deletions
diff --git a/float_test5.bpl b/float_test5.bpl
index be72b988..ce5d2bc7 100644
--- a/float_test5.bpl
+++ b/float_test5.bpl
@@ -1,4 +1,33 @@
-procedure F() returns () {
-	var x : float;
-	assert x - x == fp(0);
+//Translation from filter1.c
+//Should Verify
+
+procedure main() returns () {
+	var E0 : float(11 53);
+	var E1 : float(11 53);
+	var S : float(11 53);
+	var i : int;
+	var rand : int;
+	
+	E1 := fp(0 11 53);
+	S := fp(0 11 53);
+	
+	i := 0;
+	while (i <= 1000000)
+	{
+		havoc E0;
+		assume(E0 >= fp(-1 11 53) && E0 <= fp(1 11 53));
+		
+		havoc rand;
+		if (rand != 0) {
+			S := fp(0 11 53);
+		}
+		else {
+			S := fp(0.999 11 53) * S + E0 - E1;
+		}
+		E1 := E0;
+		
+		//assert(1==0);
+		assert(S >= fp(-1 11 53) && S <= fp(1 11 53));
+		i := i + 1;
+	}
 }
 \ No newline at end of file