diff --git a/src/main/scala/leon/plugin/CodeExtraction.scala b/src/main/scala/leon/plugin/CodeExtraction.scala
index a0c7579410e87dfea059495303eadc5c555920ae..32e600e957dc07934216c2dbd1bee619705a23de 100644
--- a/src/main/scala/leon/plugin/CodeExtraction.scala
+++ b/src/main/scala/leon/plugin/CodeExtraction.scala
@@ -570,6 +570,10 @@ trait CodeExtraction extends Extractors {
             case Some(f) => varSubsts(varSym) = f
             case None => varSubsts.remove(varSym)
           }
+          if(containsEpsilon(c1)) {
+            unit.error(epsi.pos, "Usage of nested epsilon is not allowed.")
+            throw ImpureCodeEncounteredException(epsi)
+          }
           Epsilon(c1).setType(pstpe).setPosInfo(epsi.pos.line, epsi.pos.column)
         }
         case ExSomeConstruction(tpe, arg) => {
diff --git a/src/main/scala/leon/purescala/Trees.scala b/src/main/scala/leon/purescala/Trees.scala
index f9d0498f0fd46c867817778fb6ba9a845498755f..638db0c2024152c46b9f735263b11e9ce01b5ca2 100644
--- a/src/main/scala/leon/purescala/Trees.scala
+++ b/src/main/scala/leon/purescala/Trees.scala
@@ -818,6 +818,18 @@ object Trees {
     treeCatamorphism(convert, combine, compute, expr)
   }
 
+  def containsEpsilon(expr: Expr): Boolean = {
+    def convert(t : Expr) : Boolean = t match {
+      case (l : Epsilon) => true
+      case _ => false
+    }
+    def combine(c1 : Boolean, c2 : Boolean) : Boolean = c1 || c2
+    def compute(t : Expr, c : Boolean) = t match {
+      case (l : Epsilon) => true
+      case _ => c
+    }
+    treeCatamorphism(convert, combine, compute, expr)
+  }
   def containsLetDef(expr: Expr): Boolean = {
     def convert(t : Expr) : Boolean = t match {
       case (l : LetDef) => true
diff --git a/testcases/regression/Epsilon6.scala b/testcases/regression/Epsilon6.scala
deleted file mode 100644
index a0d5b959c2b29329013208bded4ddb345af8eb2b..0000000000000000000000000000000000000000
--- a/testcases/regression/Epsilon6.scala
+++ /dev/null
@@ -1,13 +0,0 @@
-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)
-
-}