1 files changed, 20 insertions, 0 deletions
diff --git a/Test/floats/test10.bpl b/Test/floats/test10.bpl
new file mode 100644
index 00000000..566f7a56
--- /dev/null
+++ b/Test/floats/test10.bpl
@@ -0,0 +1,20 @@
+//Translation from loop.c
+//Should return an error?  (The real case does as well...)
+
+procedure main() returns () {
+	var x : float;
+	var y : float;
+	var z : float;
+	
+	x := fp(1);
+	y := fp(10000000);
+	z := fp(42);
+	
+	while (x < y) {
+		x := x + fp(1);
+		y := y - fp(1);
+		z := z + fp(1);
+	}
+	
+	assert(z >= fp(0) && z <= fp(10000000));
+}
+\ No newline at end of file