diff --git a/mytest/Epsilon3.scala b/mytest/Epsilon3.scala
new file mode 100644
index 0000000000000000000000000000000000000000..54b73ce93e644b753518a2f5ce1685fef474a8e1
--- /dev/null
+++ b/mytest/Epsilon3.scala
@@ -0,0 +1,13 @@
+import leon.Utils._
+
+object Epsilon3 {
+
+  def pos(): Int = {
+    epsilon((y: Int) => y > 0)
+  } ensuring(_ >= 0)
+
+  def posWrong(): Int = {
+    epsilon((y: Int) => y >= 0)
+  } ensuring(_ > 0)
+
+}
diff --git a/mytest/Epsilon4.scala b/mytest/Epsilon4.scala
new file mode 100644
index 0000000000000000000000000000000000000000..ede704be7ebc1b6a7db7f6560f40058930690801
--- /dev/null
+++ b/mytest/Epsilon4.scala
@@ -0,0 +1,29 @@
+import leon.Utils._
+
+object Epsilon4 {
+
+  sealed abstract class MyList
+  case class MyCons(head: Int, tail: MyList) extends MyList
+  case class MyNil() extends MyList
+
+  def size(lst: MyList): Int = (lst match {
+    case MyNil() => 0
+    case MyCons(_, xs) => 1 + size(xs)
+  })
+
+  def toSet(lst: MyList): Set[Int] = lst match {
+    case MyCons(x, xs) => toSet(xs) ++ Set(x)
+    case MyNil() => Set[Int]()
+  }
+
+  def toList(set: Set[Int]): MyList = if(set == Set.empty[Int]) MyNil() else {
+    val elem = epsilon((x : Int) => set contains x)
+    MyCons(elem, toList(set -- Set[Int](elem)))
+  }
+
+  //timeout, but this probably means that it is valid as expected
+  def property(lst: MyList): Boolean = (size(toList(toSet(lst))) <= size(lst)) holds
+
+  def wrongProperty0(lst: MyList): Boolean = (size(toList(toSet(lst))) == size(lst)) holds
+  def wrongProperty1(lst: MyList): Boolean = (toList(toSet(lst)) == lst) holds
+}
diff --git a/mytest/Epsilon5.scala b/mytest/Epsilon5.scala
new file mode 100644
index 0000000000000000000000000000000000000000..25d016e1bfa7cdf7b320a0e3022fbdedf5a9d0ed
--- /dev/null
+++ b/mytest/Epsilon5.scala
@@ -0,0 +1,15 @@
+import leon.Utils._
+
+object Epsilon5 {
+
+  def foo(x: Int, y: Int): Int = {
+    epsilon((z: Int) => z > x && z < y)
+  } ensuring(_ >= x)
+
+  def fooWrong(x: Int, y: Int): Int = {
+    epsilon((z: Int) => z >= x && z <= y)
+  } ensuring(_ > x)
+
+}
+
+// vim: set ts=4 sw=4 et:
diff --git a/mytest/Epsilon6.scala b/mytest/Epsilon6.scala
new file mode 100644
index 0000000000000000000000000000000000000000..a0d5b959c2b29329013208bded4ddb345af8eb2b
--- /dev/null
+++ b/mytest/Epsilon6.scala
@@ -0,0 +1,13 @@
+import leon.Utils._
+
+object Epsilon6 {
+
+  def fooWrong(): Int = {
+    epsilon((y: Int) => y > epsilon((z: Int) => z < y))
+  } ensuring(_ >= 0)
+
+  def foo(): Int = {
+    epsilon((y: Int) => y > epsilon((z: Int) => z < y))
+  } ensuring(res => res >= 0 || res < 0)
+
+}