diff --git a/src/main/scala/leon/purescala/Constructors.scala b/src/main/scala/leon/purescala/Constructors.scala
index 6d4d1575ec98e0c7adb4669624065fe3fa8988c4..9d69aab808a70589cd5da00d01ee0305232f8b74 100644
--- a/src/main/scala/leon/purescala/Constructors.scala
+++ b/src/main/scala/leon/purescala/Constructors.scala
@@ -59,12 +59,30 @@ object Constructors {
   def gives(scrutinee : Expr, cases : Seq[MatchCase]) : Gives =
     Gives(scrutinee, filterCases(scrutinee.getType, cases))
   
-  def passes(in : Expr, out : Expr, cases : Seq[MatchCase]) : Passes = {
-    Passes(in, out, filterCases(in.getType, cases))
+  def passes(in : Expr, out : Expr, cases : Seq[MatchCase]): Expr = {
+    val resultingCases = filterCases(in.getType, cases)
+    if (resultingCases.nonEmpty) {
+      Passes(in, out, resultingCases)
+    } else {
+      BooleanLiteral(true)
+    }
   }
 
-  def matchExpr(scrutinee : Expr, cases : Seq[MatchCase]) : MatchExpr = 
-    MatchExpr(scrutinee, filterCases(scrutinee.getType, cases))
+  def matchExpr(scrutinee : Expr, cases : Seq[MatchCase]) : Expr ={
+    val filtered = filterCases(scrutinee.getType, cases)
+    if (filtered.nonEmpty)
+      MatchExpr(scrutinee, filtered)
+    else 
+      Error(
+        cases match {
+          case Seq(hd, _*) => hd.rhs.getType
+          case Seq() => Untyped
+        },
+        "No case matches the scrutinee"
+      )
+  } 
+    
+   
 
   def and(exprs: Expr*): Expr = {
     val flat = exprs.flatMap(_ match {
diff --git a/src/main/scala/leon/purescala/Extractors.scala b/src/main/scala/leon/purescala/Extractors.scala
index 5ee3980484a788a6c32db86511eac260e5f79d33..3ba2da4f33be47a19f2c16c9420a78a3ba8eef03 100644
--- a/src/main/scala/leon/purescala/Extractors.scala
+++ b/src/main/scala/leon/purescala/Extractors.scala
@@ -226,7 +226,7 @@ object Extractors {
   }
 
   object MatchLike {
-    def unapply(m : MatchLike) : Option[(Expr, Seq[MatchCase], (Expr, Seq[MatchCase]) => MatchLike)] = {
+    def unapply(m : MatchLike) : Option[(Expr, Seq[MatchCase], (Expr, Seq[MatchCase]) => Expr)] = {
       Option(m) map { m => 
         (m.scrutinee, m.cases, m match {
           case _ : MatchExpr  => matchExpr
@@ -234,7 +234,7 @@ object Extractors {
           case _ : Passes     => 
             (s, cases) => {
               val Tuple(Seq(in, out)) = s
-              passes(in,out,cases)
+              passes(in, out, cases)
             }
         })
       }
diff --git a/src/main/scala/leon/purescala/TreeOps.scala b/src/main/scala/leon/purescala/TreeOps.scala
index 33d2b564ceaf7c3dc386a65b853484225555efb5..56249605f64c06323bd402917978b61226aae52f 100644
--- a/src/main/scala/leon/purescala/TreeOps.scala
+++ b/src/main/scala/leon/purescala/TreeOps.scala
@@ -2332,10 +2332,10 @@ object TreeOps {
               Seq(c)
           }}
 
-          var finalMatch = matchExpr(scrutinee, List(newCases.head))
+          var finalMatch = matchExpr(scrutinee, List(newCases.head)).asInstanceOf[MatchExpr]
 
           for (toAdd <- newCases.tail if !isMatchExhaustive(finalMatch)) {
-            finalMatch = matchExpr(scrutinee, finalMatch.cases :+ toAdd)
+            finalMatch = matchExpr(scrutinee, finalMatch.cases :+ toAdd).asInstanceOf[MatchExpr]
           }
 
           finalMatch
diff --git a/src/main/scala/leon/purescala/Trees.scala b/src/main/scala/leon/purescala/Trees.scala
index 88fd34b3e63ebb43ef16ae3cb7726483d44ef582..778306cbac9a397a99226770070a8c12ddbc4df8 100644
--- a/src/main/scala/leon/purescala/Trees.scala
+++ b/src/main/scala/leon/purescala/Trees.scala
@@ -192,7 +192,6 @@ object Trees {
   }
   
   case class Gives(scrutinee: Expr, cases : Seq[MatchCase]) extends MatchLike {
-    require(cases.nonEmpty)
     def asIncompleteMatch = {
       val theHole = SimpleCase(WildcardPattern(None), Hole(this.getType, Seq()))
       MatchExpr(scrutinee, cases :+ theHole)