diff --git a/src/main/scala/leon/plugin/CodeExtraction.scala b/src/main/scala/leon/plugin/CodeExtraction.scala
index cde76c0fa1b1b7f38c54aa1809628c1d0396db98..c08d745721bf331a029129459c4daab0299fa22b 100644
--- a/src/main/scala/leon/plugin/CodeExtraction.scala
+++ b/src/main/scala/leon/plugin/CodeExtraction.scala
@@ -535,6 +535,17 @@ trait CodeExtraction extends Extractors {
             }
           }
         }
+        case epsi@ExEpsilonExpression(tpe, varSym, predBody) => {
+          val pstpe = scalaType2PureScala(unit, silent)(tpe)
+          val previousVarSubst: Option[Function0[Expr]] = varSubsts.get(varSym) //save the previous in case of nested epsilon
+          varSubsts(varSym) = (() => EpsilonVariable((epsi.pos.line, epsi.pos.column)).setType(pstpe))
+          val c1 = rec(predBody)
+          previousVarSubst match {
+            case Some(f) => varSubsts(varSym) = f
+            case None => varSubsts.remove(varSym)
+          }
+          Epsilon(c1).setType(pstpe).setPosInfo(epsi.pos.line, epsi.pos.column)
+        }
         case ExSomeConstruction(tpe, arg) => {
           // println("Got Some !" + tpe + ":" + arg)
           val underlying = scalaType2PureScala(unit, silent)(tpe)
diff --git a/src/main/scala/leon/plugin/Extractors.scala b/src/main/scala/leon/plugin/Extractors.scala
index 4bd9f9bf3bb34940a0bf0ea552a89df60b177ec3..78e66bf6c9ef5a2a8a1e0f23a2a3c4e30a85d19c 100644
--- a/src/main/scala/leon/plugin/Extractors.scala
+++ b/src/main/scala/leon/plugin/Extractors.scala
@@ -160,6 +160,22 @@ trait Extractors {
     //  }
     //}
 
+
+    object ExEpsilonExpression {
+      def unapply(tree: Apply) : Option[(Type, Symbol, Tree)] = tree match {
+        case Apply(
+              TypeApply(Select(Select(funcheckIdent, utilsName), epsilonName), typeTree :: Nil),
+              Function((vd @ ValDef(_, _, _, EmptyTree)) :: Nil, predicateBody) :: Nil) => {
+          if (utilsName.toString == "Utils" && epsilonName.toString == "epsilon")
+            Some((typeTree.tpe, vd.symbol, predicateBody))
+          else 
+            None
+        }
+        case _ => None
+      }
+    }
+
+
     object ExValDef {
       /** Extracts val's in the head of blocks. */
       def unapply(tree: ValDef): Option[(Symbol,Tree,Tree)] = tree match {
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index 9cc5b7b626a866430398cbd38a0faadb7b54cdee..f2382841b120af7738e808c2dbce3c4a7b8a5a4f 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -145,6 +145,15 @@ object PrettyPrinter {
       sb.append("._" + i)
       sb
     }
+
+    case e@Epsilon(pred) => {
+      var nsb = sb
+      nsb.append("epsilon(x" + e.posIntInfo._1 + "_" + e.posIntInfo._2 + ". ")
+      nsb = pp(pred, nsb, lvl)
+      nsb.append(")")
+      nsb
+    }
+
     case OptionSome(a) => {
       var nsb = sb
       nsb.append("Some(")
@@ -323,6 +332,7 @@ object PrettyPrinter {
     }
 
     case ResultVariable() => sb.append("#res")
+    case EpsilonVariable((row, col)) => sb.append("x" + row + "_" + col)
     case Not(expr) => ppUnary(sb, expr, "\u00AC(", ")", lvl)               // \neg
 
     case e @ Error(desc) => {
diff --git a/src/main/scala/leon/purescala/Trees.scala b/src/main/scala/leon/purescala/Trees.scala
index 09f91e3795562854af4fb9b72c98ef6f68afaea3..cb0ce8a1867232d277df2892ca522a9fd1ed8645 100644
--- a/src/main/scala/leon/purescala/Trees.scala
+++ b/src/main/scala/leon/purescala/Trees.scala
@@ -40,6 +40,8 @@ object Trees {
    * the expected type. */
   case class Error(description: String) extends Expr with Terminal with ScalacPositional
 
+  case class Epsilon(pred: Expr) extends Expr with ScalacPositional
+
   /* Like vals */
   case class Let(binder: Identifier, value: Expr, body: Expr) extends Expr {
     binder.markAsLetBinder
@@ -263,6 +265,8 @@ object Trees {
   // represents the result in post-conditions
   case class ResultVariable() extends Expr with Terminal
 
+  case class EpsilonVariable(pos: (Int, Int)) extends Expr with Terminal
+
   /* Literals */
   sealed abstract class Literal[T] extends Expr with Terminal {
     val value: T
@@ -404,6 +408,7 @@ object Trees {
       case CaseClassInstanceOf(cd, e) => Some((e, CaseClassInstanceOf(cd, _)))
       case Assignment(id, e) => Some((e, Assignment(id, _)))
       case TupleSelect(t, i) => Some((t, TupleSelect(_, i)))
+      case e@Epsilon(t) => Some((t, (expr: Expr) => Epsilon(expr).setType(e.getType).setPosInfo(e)))
       case _ => None
     }
   }