Bring back match exhaustiveness checks

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)
           }

src/regression/resources/regression/verification/purescala/invalid/MatchExh.scala

+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
+  }
+
+}

src/regression/resources/regression/verification/purescala/valid/MatchExh.scala

+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
+  }
+
+}