diff --git a/mytest/Epsilon1.scala b/mytest/Epsilon1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..1d83db59a4cee11aa8256f46e42e6d6f8018ee5e
--- /dev/null
+++ b/mytest/Epsilon1.scala
@@ -0,0 +1,9 @@
+import leon.Utils._
+
+object Epsilon1 {
+
+  def foo(x: Int): Int = {
+    epsilon((y: Int) => y >= x)
+  } ensuring(_ > x)
+
+}