diff --git a/src/main/scala/leon/verification/DefaultTactic.scala b/src/main/scala/leon/verification/DefaultTactic.scala
index 2bcd2eb0b6aba3f7d8c52fc2999d25b4befd8e19..bba6f4fa2789e75cbabfff59b2bab6ed2ccd65cc 100644
--- a/src/main/scala/leon/verification/DefaultTactic.scala
+++ b/src/main/scala/leon/verification/DefaultTactic.scala
@@ -46,9 +46,9 @@ class DefaultTactic(vctx: VerificationContext) extends Tactic(vctx) {
       fd.body match {
         case Some(body) =>
           val calls = collectWithPC {
-            case e @ Error(_, "Match is non-exhaustive") =>
-              (e, VCKinds.ExhaustiveMatch, BooleanLiteral(false))
 
+            case m @ MatchExpr(scrut, cases) =>
+              (m, VCKinds.ExhaustiveMatch, orJoin(cases map (matchCaseCondition(scrut, _))))
 
             case e @ Error(_, _) =>
               (e, VCKinds.Assert, BooleanLiteral(false))
@@ -77,8 +77,8 @@ class DefaultTactic(vctx: VerificationContext) extends Tactic(vctx) {
           }(body)
 
           calls.map {
-            case ((e, kind, errorCond), path) =>
-              val vc = implies(and(precOrTrue(fd), path), errorCond)
+            case ((e, kind, correctnessCond), path) =>
+              val vc = implies(and(precOrTrue(fd), path), correctnessCond)
 
               VC(vc, fd, kind, this).setPos(e)
           }
diff --git a/src/regression/resources/regression/verification/purescala/invalid/MatchExh.scala b/src/regression/resources/regression/verification/purescala/invalid/MatchExh.scala
new file mode 100644
index 0000000000000000000000000000000000000000..0f7f7d7360738be250e6a50fa89ff0aa6d4ed7e5
--- /dev/null
+++ b/src/regression/resources/regression/verification/purescala/invalid/MatchExh.scala
@@ -0,0 +1,35 @@
+import leon.lang._
+import leon.collection._
+
+object MatchExh {
+  
+  def exh1(i: Int) = i match {
+    case 1 => 2
+    case 0 => 2
+    case _ => 2
+  }
+
+  def exh2[A](l: List[A]) = l match {
+    case Nil() => 0
+    case Cons(a, Nil()) => 1
+    case Cons(a, _) => 2
+  }
+
+  def err1(i: Int) = i match {
+    case 1 => 2
+    case 0 => 42
+  }
+
+  def err2[A](l: List[A]) = l match {
+    case Nil() => 0
+    case Cons(a, Nil()) => 1
+    case Cons(a, Cons(b, _)) if a == b => 2
+  }
+
+  def err3(l: List[BigInt]) = l match {
+    case Nil() => 0
+    case Cons(BigInt(0), Nil()) => 0
+    case Cons(_, Cons(_, _)) => 1
+  }
+
+}
diff --git a/src/regression/resources/regression/verification/purescala/valid/MatchExh.scala b/src/regression/resources/regression/verification/purescala/valid/MatchExh.scala
new file mode 100644
index 0000000000000000000000000000000000000000..77251bc8cfc010b5adee1e662b4dfb7b1efd656a
--- /dev/null
+++ b/src/regression/resources/regression/verification/purescala/valid/MatchExh.scala
@@ -0,0 +1,18 @@
+import leon.lang._
+import leon.collection._
+
+object MatchExh {
+  
+  def exh1(i: Int) = i match {
+    case 1 => 2
+    case 0 => 2
+    case _ => 2
+  }
+
+  def exh2[A](l: List[A]) = l match {
+    case Nil() => 0
+    case Cons(a, Nil()) => 1
+    case Cons(a, _) => 2
+  }
+
+}