diff --git a/src/main/scala/leon/purescala/Extractors.scala b/src/main/scala/leon/purescala/Extractors.scala
index 3ba2da4f33be47a19f2c16c9420a78a3ba8eef03..a5c591bddf75a1bc76546a5815d25105b9f1f1ba 100644
--- a/src/main/scala/leon/purescala/Extractors.scala
+++ b/src/main/scala/leon/purescala/Extractors.scala
@@ -141,6 +141,18 @@ object Extractors {
           builder(es(0), newcases)
         }
       ))
+      case Passes(in, out, cases) => Some((
+        in +: out +: cases.flatMap { _.expressions },
+        { case Seq(in, out, es@_*) => {
+          var i = 0
+          val newcases = for (caze <- cases) yield caze match {
+            case SimpleCase(b, _) => i+=1; SimpleCase(b, es(i-1)) 
+            case GuardedCase(b, _, _) => i+=2; GuardedCase(b, es(i-1), es(i-2)) 
+          }
+
+          Passes(in, out, newcases)
+        }}
+      ))
       case LetDef(fd, body) =>
         fd.body match {
           case Some(b) =>
@@ -231,11 +243,6 @@ object Extractors {
         (m.scrutinee, m.cases, m match {
           case _ : MatchExpr  => matchExpr
           case _ : Gives      => gives
-          case _ : Passes     => 
-            (s, cases) => {
-              val Tuple(Seq(in, out)) = s
-              passes(in, out, cases)
-            }
         })
       }
     }
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index b31c3db9fa7a21618865296a6998b6816b2fc4c4..899605eb1fd8f28f649f0b308645becc35ce84d8 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -228,7 +228,7 @@ class PrettyPrinter(opts: PrinterOptions, val sb: StringBuffer = new StringBuffe
       
       case p@Passes(in, out, tests) =>
         optP {
-          p"""|${p.scrutinee} passes {
+          p"""|($in, $out) passes {
               |  ${nary(tests, "\n")}
               |}"""
         }
diff --git a/src/main/scala/leon/purescala/TreeOps.scala b/src/main/scala/leon/purescala/TreeOps.scala
index b3bb309d75bbc39c4394b34d70df3c32e6a5d2f9..29377f7748386185dc06d678b2d7253201b30c7d 100644
--- a/src/main/scala/leon/purescala/TreeOps.scala
+++ b/src/main/scala/leon/purescala/TreeOps.scala
@@ -355,6 +355,7 @@ object TreeOps {
           case Let(i,_,_) => subvs - i
           case Choose(is,_) => subvs -- is
           case MatchLike(_, cses, _) => subvs -- (cses.map(_.pattern.binders).foldLeft(Set[Identifier]())((a, b) => a ++ b))
+          case Passes(_, _ , cses)   => subvs -- (cses.map(_.pattern.binders).foldLeft(Set[Identifier]())((a, b) => a ++ b))
           case Lambda(args, body) => subvs -- args.map(_.id)
           case Forall(args, body) => subvs -- args.map(_.id)
           case _ => subvs
@@ -431,6 +432,9 @@ object TreeOps {
       case m @ MatchLike(s, cses, builder) =>
         Some(builder(s, cses.map(freshenCase(_))).copiedFrom(m))
 
+      case p @ Passes(in, out, cses) =>
+        Some(Passes(in, out, cses.map(freshenCase(_))).copiedFrom(p))
+
       case l @ Let(i,e,b) =>
         val newID = FreshIdentifier(i.name, true).copiedFrom(i)
         Some(Let(newID, e, replace(Map(Variable(i) -> Variable(newID)), b)))
@@ -614,6 +618,7 @@ object TreeOps {
       case l @ Let(i,e,b) => rec(b, s + (i -> rec(e, s)))
       case i @ IfExpr(t1,t2,t3) => IfExpr(rec(t1, s),rec(t2, s),rec(t3, s))
       case m @ MatchLike(scrut,cses,builder) => builder(rec(scrut, s), cses.map(inCase(_, s))).setPos(m)
+      case p @ Passes(in, out, cses) => Passes(rec(in, s), rec(out,s), cses.map(inCase(_, s))).setPos(p)
       case n @ NAryOperator(args, recons) => {
         var change = false
         val rargs = args.map(a => {
@@ -1619,6 +1624,9 @@ object TreeOps {
 
         case Same(MatchLike(s1, cs1, _), MatchLike(s2, cs2, _)) =>
           cs1.size == cs2.size && isHomo(s1, s2) && casesMatch(cs1,cs2)
+          
+        case (Passes(in1, out1, cs1), Passes(in2, out2, cs2)) =>
+          cs1.size == cs2.size && isHomo(in1,in2) && isHomo(out1,out2) && casesMatch(cs1,cs2)
 
         case (FunctionInvocation(tfd1, args1), FunctionInvocation(tfd2, args2)) =>
           // TODO: Check type params
diff --git a/src/main/scala/leon/purescala/Trees.scala b/src/main/scala/leon/purescala/Trees.scala
index 778306cbac9a397a99226770070a8c12ddbc4df8..70410503470c814559c266769489e21a06a7fd1f 100644
--- a/src/main/scala/leon/purescala/Trees.scala
+++ b/src/main/scala/leon/purescala/Trees.scala
@@ -198,11 +198,10 @@ object Trees {
     }
   } 
   
-  case class Passes(in: Expr, out : Expr, cases : Seq[MatchCase]) extends MatchLike {
+  case class Passes(in: Expr, out : Expr, cases : Seq[MatchCase]) extends Expr {
     require(cases.nonEmpty)
 
-    override def getType = BooleanType
-    val scrutinee = Tuple(Seq(in, out))
+    val getType = BooleanType
     
     def asConstraint = {
       val defaultCase = SimpleCase(WildcardPattern(None), out)