diff --git a/mytest/WhileTest.scala b/mytest/WhileTest.scala
new file mode 100644
index 0000000000000000000000000000000000000000..4ec15bf42827d9c626c0aa50ba257abd9d4431a2
--- /dev/null
+++ b/mytest/WhileTest.scala
@@ -0,0 +1,14 @@
+object WhileTest {
+  def foo(x : Int) : Int = {
+    require(x >= 0)
+
+    var y : Int = x
+
+    while(y >= 0) {
+      y = y - 1
+      // assert(y >= -1)
+    }
+
+    y + 1
+  } ensuring(_ == 0)
+}