diff --git a/src/main/scala/leon/purescala/TreeOps.scala b/src/main/scala/leon/purescala/TreeOps.scala
index 2938be18e9524f4a9684ffffdd2e51e978125b51..0e63a4a27465728906a133625b24d15d0398635a 100644
--- a/src/main/scala/leon/purescala/TreeOps.scala
+++ b/src/main/scala/leon/purescala/TreeOps.scala
@@ -960,24 +960,30 @@ object TreeOps {
       val (expr, ctx) = pre(eIn, cIn)
 
       val (newExpr, newC) = expr match {
+        case t: Terminal =>
+          (expr, ctx)
+
         case UnaryOperator(e, builder) =>
           val (e1, c) = rec(e, ctx)
-
           val newE = builder(e1)
+
           (newE, combiner(newE, ctx, Seq(c)))
+
         case BinaryOperator(e1, e2, builder) =>
           val (ne1, c1) = rec(e1, ctx)
           val (ne2, c2) = rec(e2, ctx)
-
           val newE = builder(ne1, ne2)
+
           (newE, combiner(newE, ctx, Seq(c1, c2)))
+
         case NAryOperator(es, builder) =>
           val (nes, cs) = es.map(e => rec(e, ctx)).unzip
-
           val newE = builder(nes)
+
           (newE, combiner(newE, ctx, cs))
+
         case e =>
-          sys.error("Expression "+e+" ["+e.getClass+"] has no defined extractor")
+          sys.error("Expression "+e+" ["+e.getClass+"] is not extractable")
       }
 
       post(newExpr, newC)
diff --git a/src/main/scala/leon/purescala/Trees.scala b/src/main/scala/leon/purescala/Trees.scala
index 246f335ada8a1c0d084ce1ac7e355db619805320..4ba80bdc838dd0dbf7633694f24ae1e1683e083e 100644
--- a/src/main/scala/leon/purescala/Trees.scala
+++ b/src/main/scala/leon/purescala/Trees.scala
@@ -6,6 +6,7 @@ object Trees {
   import Common._
   import TypeTrees._
   import Definitions._
+  import Extractors._
 
   /* EXPRESSIONS */
 
@@ -42,7 +43,9 @@ object Trees {
 
   case class Epsilon(pred: Expr) extends Expr with ScalacPositional
 
-  case class Choose(vars: List[Identifier], pred: Expr) extends Expr with ScalacPositional
+  case class Choose(vars: List[Identifier], pred: Expr) extends Expr with ScalacPositional with UnaryExtractable {
+    def extract = Some((pred, (e: Expr) => Choose(vars, e)))
+  }
 
   /* Like vals */
   case class Let(binder: Identifier, value: Expr, body: Expr) extends Expr {