1 files changed, 19 insertions, 4 deletions
diff --git a/float_test4.bpl b/float_test4.bpl
index 1252dc71..a7aa8c4b 100644
--- a/float_test4.bpl
+++ b/float_test4.bpl
@@ -1,5 +1,20 @@
- procedure F() returns () {
-	var x : float;
-	x := fp (.5 8 23);
-	assert x == fp (-1 0);
+//Translation from drift_tenth.c
+//Should Verify
+//FAILS; note that it succeeds when tick == fp(.1)
+
+procedure main() returns () {
+	var tick : float;
+	var time : float;
+	var i: int;
+	
+	tick := fp(1)/fp(10);
+	time := fp(0);
+	
+	i := 0;
+	while (i < 10)
+	{
+		time := time + tick;
+		i := i + 1;
+	}
+	assert(time == fp(1));
 }
 \ No newline at end of file