diff --git a/e.dfy b/e.dfy
new file mode 100644
index 0000000..914be8c
--- /dev/null
+++ b/e.dfy
@@ -0,0 +1,10 @@
+method Main() {
+  var e := 9999;
+  while e > 0
+    decreases e
+    invariant e >= 0
+    {
+      print "e";
+      e := e - 1;
+    }
+}
\ No newline at end of file