Merge pull request #4078 from gbasler/topic/fix-analysis-budget

Avoid the `CNF budget exceeded` exception via smarter translation into CNF.

12 files changed, 673 insertions, 277 deletions

diff --git a/src/compiler/scala/tools/nsc/transform/patmat/Logic.scala b/src/compiler/scala/tools/nsc/transform/patmat/Logic.scala
index e6ddf8b758..75d2cfe0f2 100644
--- a/src/compiler/scala/tools/nsc/transform/patmat/Logic.scala
+++ b/src/compiler/scala/tools/nsc/transform/patmat/Logic.scala
@@ -16,8 +16,8 @@ trait Logic extends Debugging  {
   import PatternMatchingStats._
 
   private def max(xs: Seq[Int]) = if (xs isEmpty) 0 else xs max
-  private def alignedColumns(cols: Seq[AnyRef]): Seq[String] = {
-    def toString(x: AnyRef) = if (x eq null) "" else x.toString
+  private def alignedColumns(cols: Seq[Any]): Seq[String] = {
+    def toString(x: Any) = if (x == null) "" else x.toString
     if (cols.isEmpty || cols.tails.isEmpty) cols map toString
     else {
       val colLens = cols map (c => toString(c).length)
@@ -32,7 +32,7 @@ trait Logic extends Debugging  {
     }
   }
 
-  def alignAcrossRows(xss: List[List[AnyRef]], sep: String, lineSep: String = "\n"): String = {
+  def alignAcrossRows(xss: List[List[Any]], sep: String, lineSep: String = "\n"): String = {
     val maxLen = max(xss map (_.length))
     val padded = xss map (xs => xs ++ List.fill(maxLen - xs.length)(null))
     padded.transpose.map(alignedColumns).transpose map (_.mkString(sep)) mkString(lineSep)
@@ -46,7 +46,7 @@ trait Logic extends Debugging  {
     type Tree
 
     class Prop
-    case class Eq(p: Var, q: Const) extends Prop
+    final case class Eq(p: Var, q: Const) extends Prop
 
     type Const
 
@@ -105,43 +105,146 @@ trait Logic extends Debugging  {
 
     // would be nice to statically check whether a prop is equational or pure,
     // but that requires typing relations like And(x: Tx, y: Ty) : (if(Tx == PureProp && Ty == PureProp) PureProp else Prop)
-    case class And(a: Prop, b: Prop) extends Prop
-    case class Or(a: Prop, b: Prop) extends Prop
-    case class Not(a: Prop) extends Prop
+    final case class And(ops: Set[Prop]) extends Prop
+    object And {
+      def apply(ops: Prop*) = new And(ops.toSet)
+    }
+
+    final case class Or(ops: Set[Prop]) extends Prop
+    object Or {
+      def apply(ops: Prop*) = new Or(ops.toSet)
+    }
+
+    final case class Not(a: Prop) extends Prop
 
     case object True extends Prop
     case object False extends Prop
 
     // symbols are propositions
-    abstract case class Sym(variable: Var, const: Const) extends Prop {
+    final class Sym private[PropositionalLogic] (val variable: Var, val const: Const) extends Prop {
       private val id: Int = Sym.nextSymId
 
-      override def toString = variable +"="+ const +"#"+ id
+      override def toString = variable + "=" + const + "#" + id
     }
-    class UniqueSym(variable: Var, const: Const) extends Sym(variable, const)
+
     object Sym {
       private val uniques: HashSet[Sym] = new HashSet("uniques", 512)
       def apply(variable: Var, const: Const): Sym = {
-        val newSym = new UniqueSym(variable, const)
+        val newSym = new Sym(variable, const)
         (uniques findEntryOrUpdate newSym)
       }
-      private def nextSymId = {_symId += 1; _symId}; private var _symId = 0
+      def nextSymId = {_symId += 1; _symId}; private var _symId = 0
       implicit val SymOrdering: Ordering[Sym] = Ordering.by(_.id)
     }
 
-    def /\(props: Iterable[Prop]) = if (props.isEmpty) True else props.reduceLeft(And(_, _))
-    def \/(props: Iterable[Prop]) = if (props.isEmpty) False else props.reduceLeft(Or(_, _))
+    def /\(props: Iterable[Prop]) = if (props.isEmpty) True else And(props.toSeq: _*)
+    def \/(props: Iterable[Prop]) = if (props.isEmpty) False else Or(props.toSeq: _*)
+
+    /**
+     * Simplifies propositional formula according to the following rules:
+     * - eliminate double negation (avoids unnecessary Tseitin variables)
+     * - flatten trees of same connectives (avoids unnecessary Tseitin variables)
+     * - removes constants and connectives that are in fact constant because of their operands
+     * - eliminates duplicate operands
+     * - convert formula into NNF: all sub-expressions have a positive polarity
+     * which makes them amenable for the subsequent Plaisted transformation
+     * and increases chances to figure out that the formula is already in CNF
+     *
+     * Complexity: DFS over formula tree
+     *
+     * See http://www.decision-procedures.org/slides/propositional_logic-2x3.pdf
+     */
+    def simplify(f: Prop): Prop = {
+
+      // limit size to avoid blow up
+      def hasImpureAtom(ops: Seq[Prop]): Boolean = ops.size < 10 &&
+        ops.combinations(2).exists {
+          case Seq(a, Not(b)) if a == b => true
+          case Seq(Not(a), b) if a == b => true
+          case _                        => false
+        }
+
+      // push negation inside formula
+      def negationNormalFormNot(p: Prop): Prop = p match {
+        case And(ops) => Or(ops.map(negationNormalFormNot)) // De'Morgan
+        case Or(ops)  => And(ops.map(negationNormalFormNot)) // De'Morgan
+        case Not(p)   => negationNormalForm(p)
+        case True     => False
+        case False    => True
+        case s: Sym   => Not(s)
+      }
+
+      def negationNormalForm(p: Prop): Prop = p match {
+        case And(ops)     => And(ops.map(negationNormalForm))
+        case Or(ops)      => Or(ops.map(negationNormalForm))
+        case Not(negated) => negationNormalFormNot(negated)
+        case True
+             | False
+             | (_: Sym)   => p
+      }
+
+      def simplifyProp(p: Prop): Prop = p match {
+        case And(fv)     =>
+          // recurse for nested And (pulls all Ands up)
+          val ops = fv.map(simplifyProp) - True // ignore `True`
+
+          // build up Set in order to remove duplicates
+          val opsFlattened = ops.flatMap {
+            case And(fv) => fv
+            case f       => Set(f)
+          }.toSeq
+
+          if (hasImpureAtom(opsFlattened) || opsFlattened.contains(False)) {
+            False
+          } else {
+            opsFlattened match {
+              case Seq()  => True
+              case Seq(f) => f
+              case ops    => And(ops: _*)
+            }
+          }
+        case Or(fv)      =>
+          // recurse for nested Or (pulls all Ors up)
+          val ops = fv.map(simplifyProp) - False // ignore `False`
+
+          val opsFlattened = ops.flatMap {
+            case Or(fv) => fv
+            case f      => Set(f)
+          }.toSeq
+
+          if (hasImpureAtom(opsFlattened) || opsFlattened.contains(True)) {
+            True
+          } else {
+            opsFlattened match {
+              case Seq()  => False
+              case Seq(f) => f
+              case ops    => Or(ops: _*)
+            }
+          }
+        case Not(Not(a)) =>
+          simplify(a)
+        case Not(p)      =>
+          Not(simplify(p))
+        case p           =>
+          p
+      }
+
+      val nnf = negationNormalForm(f)
+      simplifyProp(nnf)
+    }
 
     trait PropTraverser {
       def apply(x: Prop): Unit = x match {
-        case And(a, b) => apply(a); apply(b)
-        case Or(a, b) => apply(a); apply(b)
+        case And(ops) => ops foreach apply
+        case Or(ops) => ops foreach apply
         case Not(a) => apply(a)
         case Eq(a, b) => applyVar(a); applyConst(b)
+        case s: Sym => applySymbol(s)
         case _ =>
       }
       def applyVar(x: Var): Unit = {}
       def applyConst(x: Const): Unit = {}
+      def applySymbol(x: Sym): Unit = {}
     }
 
     def gatherVariables(p: Prop): Set[Var] = {
@@ -152,36 +255,27 @@ trait Logic extends Debugging  {
       vars.toSet
     }
 
+    def gatherSymbols(p: Prop): Set[Sym] = {
+      val syms = new mutable.HashSet[Sym]()
+      (new PropTraverser {
+        override def applySymbol(s: Sym) = syms += s
+      })(p)
+      syms.toSet
+    }
+
     trait PropMap {
       def apply(x: Prop): Prop = x match { // TODO: mapConserve
-        case And(a, b) => And(apply(a), apply(b))
-        case Or(a, b) => Or(apply(a), apply(b))
+        case And(ops) => And(ops map apply)
+        case Or(ops) => Or(ops map apply)
         case Not(a) => Not(apply(a))
         case p => p
       }
     }
 
-    // to govern how much time we spend analyzing matches for unreachability/exhaustivity
-    object AnalysisBudget {
-      private val budgetProp = scala.sys.Prop[String]("scalac.patmat.analysisBudget")
-      private val budgetOff = "off"
-      val max: Int = {
-        val DefaultBudget = 256
-        budgetProp.option match {
-          case Some(`budgetOff`) =>
-            Integer.MAX_VALUE
-          case Some(x) =>
-            x.toInt
-          case None =>
-            DefaultBudget
-        }
-      }
-
-      abstract class Exception(val advice: String) extends RuntimeException("CNF budget exceeded")
-
-      object exceeded extends Exception(
-          s"(The analysis required more space than allowed. Please try with scalac -D${budgetProp.key}=${AnalysisBudget.max*2} or -D${budgetProp.key}=${budgetOff}.)")
-
+    // TODO: remove since deprecated
+    val budgetProp = scala.sys.Prop[String]("scalac.patmat.analysisBudget")
+    if (budgetProp.isSet) {
+      reportWarning(s"Please remove -D${budgetProp.key}, it is ignored.")
     }
 
     // convert finite domain propositional logic with subtyping to pure boolean propositional logic
@@ -202,7 +296,7 @@ trait Logic extends Debugging  {
     // TODO: for V1 representing x1 and V2 standing for x1.head, encode that
     //       V1 = Nil implies -(V2 = Ci) for all Ci in V2's domain (i.e., it is unassignable)
     // may throw an AnalysisBudget.Exception
-    def removeVarEq(props: List[Prop], modelNull: Boolean = false): (Formula, List[Formula]) = {
+    def removeVarEq(props: List[Prop], modelNull: Boolean = false): (Prop, List[Prop]) = {
       val start = if (Statistics.canEnable) Statistics.startTimer(patmatAnaVarEq) else null
 
       val vars = new mutable.HashSet[Var]
@@ -226,10 +320,10 @@ trait Logic extends Debugging  {
       props foreach gatherEqualities.apply
       if (modelNull) vars foreach (_.registerNull())
 
-      val pure = props map (p => eqFreePropToSolvable(rewriteEqualsToProp(p)))
+      val pure = props map (p => rewriteEqualsToProp(p))
 
-      val eqAxioms = formulaBuilder
-      @inline def addAxiom(p: Prop) = addFormula(eqAxioms, eqFreePropToSolvable(p))
+      val eqAxioms = mutable.ArrayBuffer[Prop]()
+      @inline def addAxiom(p: Prop) = eqAxioms += p
 
       debug.patmat("removeVarEq vars: "+ vars)
       vars.foreach { v =>
@@ -255,49 +349,30 @@ trait Logic extends Debugging  {
         }
       }
 
-      debug.patmat("eqAxioms:\n"+ cnfString(toFormula(eqAxioms)))
-      debug.patmat("pure:"+ pure.map(p => cnfString(p)).mkString("\n"))
+      debug.patmat(s"eqAxioms:\n${eqAxioms.mkString("\n")}")
+      debug.patmat(s"pure:${pure.mkString("\n")}")
 
       if (Statistics.canEnable) Statistics.stopTimer(patmatAnaVarEq, start)
 
-      (toFormula(eqAxioms), pure)
+      (And(eqAxioms: _*), pure)
     }
 
+    type Solvable
 
-    // an interface that should be suitable for feeding a SAT solver when the time comes
-    type Formula
-    type FormulaBuilder
-
-    // creates an empty formula builder to which more formulae can be added
-    def formulaBuilder: FormulaBuilder
-
-    // val f = formulaBuilder; addFormula(f, f1); ... addFormula(f, fN)
-    // toFormula(f) == andFormula(f1, andFormula(..., fN))
-    def addFormula(buff: FormulaBuilder, f: Formula): Unit
-    def toFormula(buff: FormulaBuilder): Formula
-
-    // the conjunction of formulae `a` and `b`
-    def andFormula(a: Formula, b: Formula): Formula
-
-    // equivalent formula to `a`, but simplified in a lightweight way (drop duplicate clauses)
-    def simplifyFormula(a: Formula): Formula
-
-    // may throw an AnalysisBudget.Exception
-    def propToSolvable(p: Prop): Formula = {
-      val (eqAxioms, pure :: Nil) = removeVarEq(List(p), modelNull = false)
-      andFormula(eqAxioms, pure)
+    def propToSolvable(p: Prop): Solvable = {
+      val (eqAxiom, pure :: Nil) = removeVarEq(List(p), modelNull = false)
+      eqFreePropToSolvable(And(eqAxiom, pure))
     }
 
-    // may throw an AnalysisBudget.Exception
-    def eqFreePropToSolvable(p: Prop): Formula
-    def cnfString(f: Formula): String
+    def eqFreePropToSolvable(f: Prop): Solvable
 
     type Model = Map[Sym, Boolean]
     val EmptyModel: Model
     val NoModel: Model
 
-    def findModelFor(f: Formula): Model
-    def findAllModelsFor(f: Formula): List[Model]
+    def findModelFor(solvable: Solvable): Model
+
+    def findAllModelsFor(solvable: Solvable): List[Model]
   }
 }
 
diff --git a/src/compiler/scala/tools/nsc/transform/patmat/MatchAnalysis.scala b/src/compiler/scala/tools/nsc/transform/patmat/MatchAnalysis.scala
index 21e90b1d78..8650f6ef90 100644
--- a/src/compiler/scala/tools/nsc/transform/patmat/MatchAnalysis.scala
+++ b/src/compiler/scala/tools/nsc/transform/patmat/MatchAnalysis.scala
@@ -397,7 +397,6 @@ trait MatchAnalysis extends MatchApproximation {
 
   trait MatchAnalyzer extends MatchApproximator  {
     def uncheckedWarning(pos: Position, msg: String) = currentRun.reporting.uncheckedWarning(pos, msg)
-    def warn(pos: Position, ex: AnalysisBudget.Exception, kind: String) = uncheckedWarning(pos, s"Cannot check match for $kind.\n${ex.advice}")
     def reportWarning(message: String) = global.reporter.warning(typer.context.tree.pos, message)
 
   // TODO: model dependencies between variables: if V1 corresponds to (x: List[_]) and V2 is (x.hd), V2 cannot be assigned when V1 = null or V1 = Nil
@@ -428,49 +427,44 @@ trait MatchAnalysis extends MatchApproximation {
       val propsCasesOk   = approximate(True)  map caseWithoutBodyToProp
       val propsCasesFail = approximate(False) map (t => Not(caseWithoutBodyToProp(t)))
 
-      try {
-        val (eqAxiomsFail, symbolicCasesFail) = removeVarEq(propsCasesFail, modelNull = true)
-        val (eqAxiomsOk, symbolicCasesOk)     = removeVarEq(propsCasesOk,   modelNull = true)
-        val eqAxioms = simplifyFormula(andFormula(eqAxiomsOk, eqAxiomsFail)) // I'm pretty sure eqAxiomsOk == eqAxiomsFail, but not 100% sure.
-
-        val prefix   = formulaBuilder
-        addFormula(prefix, eqAxioms)
-
-        var prefixRest = symbolicCasesFail
-        var current    = symbolicCasesOk
-        var reachable  = true
-        var caseIndex  = 0
-
-        debug.patmat("reachability, vars:\n"+ ((propsCasesFail flatMap gatherVariables).distinct map (_.describe) mkString ("\n")))
-        debug.patmat("equality axioms:\n"+ cnfString(eqAxiomsOk))
-
-        // invariant (prefixRest.length == current.length) && (prefix.reverse ++ prefixRest == symbolicCasesFail)
-        // termination: prefixRest.length decreases by 1
-        while (prefixRest.nonEmpty && reachable) {
-          val prefHead = prefixRest.head
-          caseIndex += 1
-          prefixRest = prefixRest.tail
-          if (prefixRest.isEmpty) reachable = true
-          else {
-            addFormula(prefix, prefHead)
-            current = current.tail
-            val model = findModelFor(andFormula(current.head, toFormula(prefix)))
+      val (eqAxiomsFail, symbolicCasesFail) = removeVarEq(propsCasesFail, modelNull = true)
+      val (eqAxiomsOk, symbolicCasesOk)     = removeVarEq(propsCasesOk, modelNull = true)
+      val eqAxioms = simplify(And(eqAxiomsOk, eqAxiomsFail)) // I'm pretty sure eqAxiomsOk == eqAxiomsFail, but not 100% sure.
 
-            // debug.patmat("trying to reach:\n"+ cnfString(current.head) +"\nunder prefix:\n"+ cnfString(prefix))
-            // if (NoModel ne model) debug.patmat("reached: "+ modelString(model))
+      val prefix = mutable.ArrayBuffer[Prop]()
+      prefix += eqAxioms
 
-            reachable = NoModel ne model
-          }
-        }
+      var prefixRest = symbolicCasesFail
+      var current = symbolicCasesOk
+      var reachable = true
+      var caseIndex = 0
+
+      debug.patmat("reachability, vars:\n" + ((propsCasesFail flatMap gatherVariables).distinct map (_.describe) mkString ("\n")))
+      debug.patmat(s"equality axioms:\n$eqAxiomsOk")
+
+      // invariant (prefixRest.length == current.length) && (prefix.reverse ++ prefixRest == symbolicCasesFail)
+      // termination: prefixRest.length decreases by 1
+      while (prefixRest.nonEmpty && reachable) {
+        val prefHead = prefixRest.head
+        caseIndex += 1
+        prefixRest = prefixRest.tail
+        if (prefixRest.isEmpty) reachable = true
+        else {
+          prefix += prefHead
+          current = current.tail
+          val and = And((current.head +: prefix): _*)
+          val model = findModelFor(eqFreePropToSolvable(and))
 
-        if (Statistics.canEnable) Statistics.stopTimer(patmatAnaReach, start)
+          // debug.patmat("trying to reach:\n"+ cnfString(current.head) +"\nunder prefix:\n"+ cnfString(prefix))
+          // if (NoModel ne model) debug.patmat("reached: "+ modelString(model))
 
-        if (reachable) None else Some(caseIndex)
-      } catch {
-        case ex: AnalysisBudget.Exception =>
-          warn(prevBinder.pos, ex, "unreachability")
-          None // CNF budget exceeded
+          reachable = NoModel ne model
+        }
       }
+
+      if (Statistics.canEnable) Statistics.stopTimer(patmatAnaReach, start)
+
+      if (reachable) None else Some(caseIndex)
     }
 
     // exhaustivity
@@ -518,24 +512,17 @@ trait MatchAnalysis extends MatchApproximation {
         // debug.patmat("\nvars:\n"+ (vars map (_.describe) mkString ("\n")))
         // debug.patmat("\nmatchFails as CNF:\n"+ cnfString(propToSolvable(matchFails)))
 
-        try {
-          // find the models (under which the match fails)
-          val matchFailModels = findAllModelsFor(propToSolvable(matchFails))
-
-          val scrutVar = Var(prevBinderTree)
-          val counterExamples = matchFailModels.flatMap(modelToCounterExample(scrutVar))
-          // sorting before pruning is important here in order to
-          // keep neg/t7020.scala stable
-          // since e.g. List(_, _) would cover List(1, _)
-          val pruned = CounterExample.prune(counterExamples.sortBy(_.toString)).map(_.toString)
-
-          if (Statistics.canEnable) Statistics.stopTimer(patmatAnaExhaust, start)
-          pruned
-        } catch {
-          case ex : AnalysisBudget.Exception =>
-            warn(prevBinder.pos, ex, "exhaustivity")
-            Nil // CNF budget exceeded
-        }
+        // find the models (under which the match fails)
+        val matchFailModels = findAllModelsFor(propToSolvable(matchFails))
+        val scrutVar = Var(prevBinderTree)
+        val counterExamples = matchFailModels.flatMap(modelToCounterExample(scrutVar))
+        // sorting before pruning is important here in order to
+        // keep neg/t7020.scala stable
+        // since e.g. List(_, _) would cover List(1, _)
+        val pruned = CounterExample.prune(counterExamples.sortBy(_.toString)).map(_.toString)
+
+        if (Statistics.canEnable) Statistics.stopTimer(patmatAnaExhaust, start)
+        pruned
       }
     }
 
diff --git a/src/compiler/scala/tools/nsc/transform/patmat/MatchOptimization.scala b/src/compiler/scala/tools/nsc/transform/patmat/MatchOptimization.scala
index e9c81f4728..b3aef8a20e 100644
--- a/src/compiler/scala/tools/nsc/transform/patmat/MatchOptimization.scala
+++ b/src/compiler/scala/tools/nsc/transform/patmat/MatchOptimization.scala
@@ -46,16 +46,16 @@ trait MatchOptimization extends MatchTreeMaking with MatchAnalysis {
         val cond = test.prop
 
         def simplify(c: Prop): Set[Prop] = c match {
-          case And(a, b)                  => simplify(a) ++ simplify(b)
-          case Or(_, _)                   => Set(False) // TODO: make more precise
-          case Not(Eq(Var(_), NullConst)) => Set(True)  // not worth remembering
+          case And(ops)                   => ops.toSet flatMap simplify
+          case Or(ops)                    => Set(False) // TODO: make more precise
+          case Not(Eq(Var(_), NullConst)) => Set(True) // not worth remembering
           case _                          => Set(c)
         }
         val conds = simplify(cond)
 
         if (conds(False)) false // stop when we encounter a definite "no" or a "not sure"
         else {
-          val nonTrivial = conds filterNot (_ == True)
+          val nonTrivial = conds - True
           if (nonTrivial nonEmpty) {
             tested ++= nonTrivial
 
diff --git a/src/compiler/scala/tools/nsc/transform/patmat/Solving.scala b/src/compiler/scala/tools/nsc/transform/patmat/Solving.scala
index 4330781013..1ba13c0617 100644
--- a/src/compiler/scala/tools/nsc/transform/patmat/Solving.scala
+++ b/src/compiler/scala/tools/nsc/transform/patmat/Solving.scala
@@ -6,145 +6,304 @@
 
 package scala.tools.nsc.transform.patmat
 
-import scala.collection.mutable
+import scala.collection.mutable.ArrayBuffer
 import scala.reflect.internal.util.Statistics
 import scala.language.postfixOps
+import scala.collection.mutable
 import scala.reflect.internal.util.Collections._
 
-// naive CNF translation and simple DPLL solver
+// a literal is a (possibly negated) variable
+class Lit(val v: Int) extends AnyVal {
+  def unary_- : Lit = Lit(-v)
+
+  def variable: Int = Math.abs(v)
+
+  def positive = v >= 0
+
+  override def toString(): String = s"Lit#$v"
+}
+
+object Lit {
+  def apply(v: Int): Lit = new Lit(v)
+
+  implicit val LitOrdering: Ordering[Lit] = Ordering.by(_.v)
+}
+
+/** Solve pattern matcher exhaustivity problem via DPLL.
+ */
 trait Solving extends Logic {
+
   import PatternMatchingStats._
-  trait CNF extends PropositionalLogic {
-    import scala.collection.mutable.ArrayBuffer
-    type FormulaBuilder = ArrayBuffer[Clause]
-    def formulaBuilder  = ArrayBuffer[Clause]()
-    def formulaBuilderSized(init: Int)  = new ArrayBuffer[Clause](init)
-    def addFormula(buff: FormulaBuilder, f: Formula): Unit = buff ++= f
-    def toFormula(buff: FormulaBuilder): Formula = buff
 
-    // CNF: a formula is a conjunction of clauses
-    type Formula = FormulaBuilder
-    def formula(c: Clause*): Formula = ArrayBuffer(c: _*)
+  trait CNF extends PropositionalLogic {
 
     type Clause  = Set[Lit]
+
     // a clause is a disjunction of distinct literals
     def clause(l: Lit*): Clause = l.toSet
 
-    type Lit
-    def Lit(sym: Sym, pos: Boolean = true): Lit
-
-    def andFormula(a: Formula, b: Formula): Formula = a ++ b
-    def simplifyFormula(a: Formula): Formula = a.distinct
-
-    private def merge(a: Clause, b: Clause) = a ++ b
-
-    // throws an AnalysisBudget.Exception when the prop results in a CNF that's too big
-    // TODO: be smarter/more efficient about this (http://lara.epfl.ch/w/sav09:tseitin_s_encoding)
-    def eqFreePropToSolvable(p: Prop): Formula = {
-      def negationNormalFormNot(p: Prop, budget: Int): Prop =
-        if (budget <= 0) throw AnalysisBudget.exceeded
-        else p match {
-          case And(a, b) =>  Or(negationNormalFormNot(a, budget - 1), negationNormalFormNot(b, budget - 1))
-          case Or(a, b)  => And(negationNormalFormNot(a, budget - 1), negationNormalFormNot(b, budget - 1))
-          case Not(p)    => negationNormalForm(p, budget - 1)
-          case True      => False
-          case False     => True
-          case s: Sym    => Not(s)
+    /** Conjunctive normal form (of a Boolean formula).
+     *  A formula in this form is amenable to a SAT solver
+     *  (i.e., solver that decides satisfiability of a formula).
+     */
+    type Cnf = Array[Clause]
+
+    class SymbolMapping(symbols: Set[Sym]) {
+      val variableForSymbol: Map[Sym, Int] = {
+        symbols.zipWithIndex.map {
+          case (sym, i) => sym -> (i + 1)
+        }.toMap
+      }
+
+      val symForVar: Map[Int, Sym] = variableForSymbol.map(_.swap)
+
+      val relevantVars: Set[Int] = symForVar.keySet.map(math.abs)
+
+      def lit(sym: Sym): Lit = Lit(variableForSymbol(sym))
+
+      def size = symbols.size
+    }
+
+    case class Solvable(cnf: Cnf, symbolMapping: SymbolMapping)
+
+    trait CnfBuilder {
+      private[this] val buff = ArrayBuffer[Clause]()
+
+      var literalCount: Int
+
+      /**
+       * @return new Tseitin variable
+       */
+      def newLiteral(): Lit = {
+        literalCount += 1
+        Lit(literalCount)
+      }
+
+      lazy val constTrue: Lit = {
+        val constTrue = newLiteral()
+        addClauseProcessed(clause(constTrue))
+        constTrue
+      }
+
+      def constFalse: Lit = -constTrue
+
+      def isConst(l: Lit): Boolean = l == constTrue || l == constFalse
+
+      def addClauseProcessed(clause: Clause) {
+        if (clause.nonEmpty) {
+          buff += clause
         }
+      }
 
-      def negationNormalForm(p: Prop, budget: Int = AnalysisBudget.max): Prop =
-        if (budget <= 0) throw AnalysisBudget.exceeded
-        else p match {
-          case And(a, b)      => And(negationNormalForm(a, budget - 1), negationNormalForm(b, budget - 1))
-          case Or(a, b)       =>  Or(negationNormalForm(a, budget - 1), negationNormalForm(b, budget - 1))
-          case Not(negated)   => negationNormalFormNot(negated, budget - 1)
-          case True
-             | False
-             | (_ : Sym)      => p
+      def buildCnf: Array[Clause] = buff.toArray
+
+    }
+
+    /** Plaisted transformation: used for conversion of a
+      * propositional formula into conjunctive normal form (CNF)
+      * (input format for SAT solver).
+      * A simple conversion into CNF via Shannon expansion would
+      * also be possible but it's worst-case complexity is exponential
+      * (in the number of variables) and thus even simple problems
+      * could become untractable.
+      * The Plaisted transformation results in an _equisatisfiable_
+      * CNF-formula (it generates auxiliary variables)
+      * but runs with linear complexity.
+      * The common known Tseitin transformation uses bi-implication,
+      * whereas the Plaisted transformation uses implication only, thus
+      * the resulting CNF formula has (on average) only half of the clauses
+      * of a Tseitin transformation.
+      * The Plaisted transformation uses the polarities of sub-expressions
+      * to figure out which part of the bi-implication can be omitted.
+      * However, if all sub-expressions have positive polarity
+      * (e.g., after transformation into negation normal form)
+      * then the conversion is rather simple and the pseudo-normalization
+      * via NNF increases chances only one side of the bi-implication
+      * is needed.
+      */
+    class TransformToCnf(symbolMapping: SymbolMapping) extends CnfBuilder {
+
+      // new literals start after formula symbols
+      var literalCount: Int = symbolMapping.size
+
+      def convertSym(sym: Sym): Lit = symbolMapping.lit(sym)
+
+      def apply(p: Prop): Solvable = {
+
+        def convert(p: Prop): Lit = {
+          p match {
+            case And(fv)  =>
+              and(fv.map(convert))
+            case Or(fv)   =>
+              or(fv.map(convert))
+            case Not(a)   =>
+              not(convert(a))
+            case sym: Sym =>
+              convertSym(sym)
+            case True     =>
+              constTrue
+            case False    =>
+              constFalse
+            case _: Eq    =>
+              throw new MatchError(p)
+          }
         }
 
-      val TrueF          = formula()
-      val FalseF         = formula(clause())
-      def lit(s: Sym)    = formula(clause(Lit(s)))
-      def negLit(s: Sym) = formula(clause(Lit(s, pos = false)))
-
-      def conjunctiveNormalForm(p: Prop, budget: Int = AnalysisBudget.max): Formula = {
-        def distribute(a: Formula, b: Formula, budget: Int): Formula =
-          if (budget <= 0) throw AnalysisBudget.exceeded
-          else
-            (a, b) match {
-              // true \/ _ = true
-              // _ \/ true = true
-              case (trueA, trueB) if trueA.size == 0 || trueB.size == 0 => TrueF
-              // lit \/ lit
-              case (a, b) if a.size == 1 && b.size == 1 => formula(merge(a(0), b(0)))
-              // (c1 /\ ... /\ cn) \/ d = ((c1 \/ d) /\ ... /\ (cn \/ d))
-              // d \/ (c1 /\ ... /\ cn) = ((d \/ c1) /\ ... /\ (d \/ cn))
-              case (cs, ds) =>
-                val (big, small) = if (cs.size > ds.size) (cs, ds) else (ds, cs)
-                big flatMap (c => distribute(formula(c), small, budget - (big.size*small.size)))
-            }
+        def and(bv: Set[Lit]): Lit = {
+          if (bv.isEmpty) {
+            // this case can actually happen because `removeVarEq` could add no constraints
+            constTrue
+          } else if (bv.size == 1) {
+            bv.head
+          } else if (bv.contains(constFalse)) {
+            constFalse
+          } else {
+            // op1 /\ op2 /\ ... /\ opx <==>
+            // (o -> op1) /\ (o -> op2) ... (o -> opx) /\ (!op1 \/ !op2 \/... \/ !opx \/ o)
+            // (!o \/ op1) /\ (!o \/ op2) ... (!o \/ opx) /\ (!op1 \/ !op2 \/... \/ !opx \/ o)
+            val new_bv = bv - constTrue // ignore `True`
+            val o = newLiteral() // auxiliary Tseitin variable
+            new_bv.map(op => addClauseProcessed(clause(op, -o)))
+            o
+          }
+        }
 
-        if (budget <= 0) throw AnalysisBudget.exceeded
-
-        p match {
-          case True        => TrueF
-          case False       => FalseF
-          case s: Sym      => lit(s)
-          case Not(s: Sym) => negLit(s)
-          case And(a, b)   =>
-            val cnfA = conjunctiveNormalForm(a, budget - 1)
-            val cnfB = conjunctiveNormalForm(b, budget - cnfA.size)
-            cnfA ++ cnfB
-          case Or(a, b)    =>
-            val cnfA = conjunctiveNormalForm(a)
-            val cnfB = conjunctiveNormalForm(b)
-            distribute(cnfA, cnfB, budget - (cnfA.size + cnfB.size))
+        def or(bv: Set[Lit]): Lit = {
+          if (bv.isEmpty) {
+            constFalse
+          } else if (bv.size == 1) {
+            bv.head
+          } else if (bv.contains(constTrue)) {
+            constTrue
+          } else {
+            // op1 \/ op2 \/ ... \/ opx <==>
+            // (op1 -> o) /\ (op2 -> o) ... (opx -> o) /\ (op1 \/ op2 \/... \/ opx \/ !o)
+            // (!op1 \/ o) /\ (!op2 \/ o) ... (!opx \/ o) /\ (op1 \/ op2 \/... \/ opx \/ !o)
+            val new_bv = bv - constFalse // ignore `False`
+            val o = newLiteral() // auxiliary Tseitin variable
+            addClauseProcessed(new_bv + (-o))
+            o
+          }
         }
+
+        // no need for auxiliary variable
+        def not(a: Lit): Lit = -a
+
+        // add intermediate variable since we want the formula to be SAT!
+        addClauseProcessed(clause(convert(p)))
+
+        Solvable(buildCnf, symbolMapping)
       }
+    }
 
-      val start = if (Statistics.canEnable) Statistics.startTimer(patmatCNF) else null
-      val res   = conjunctiveNormalForm(negationNormalForm(p))
+    class AlreadyInCNF(symbolMapping: SymbolMapping) {
 
-      if (Statistics.canEnable) Statistics.stopTimer(patmatCNF, start)
+      object ToLiteral {
+        def unapply(f: Prop): Option[Lit] = f match {
+          case Not(ToLiteral(lit)) => Some(-lit)
+          case sym: Sym            => Some(symbolMapping.lit(sym))
+          case _                   => None
+        }
+      }
 
-      if (Statistics.canEnable) patmatCNFSizes(res.size).value += 1
+      object ToDisjunction {
+        def unapply(f: Prop): Option[Array[Clause]] = f match {
+          case Or(fv)         =>
+            val cl = fv.foldLeft(Option(clause())) {
+              case (Some(clause), ToLiteral(lit)) =>
+                Some(clause + lit)
+              case (_, _)                         =>
+                None
+            }
+            cl.map(Array(_))
+          case True           => Some(Array()) // empty, no clauses needed
+          case False          => Some(Array(clause())) // empty clause can't be satisfied
+          case ToLiteral(lit) => Some(Array(clause(lit)))
+          case _              => None
+        }
+      }
+
+      /**
+       * Checks if propositional formula is already in CNF
+       */
+      object ToCnf {
+        def unapply(f: Prop): Option[Solvable] = f match {
+          case ToDisjunction(clauses) => Some(Solvable(clauses, symbolMapping) )
+          case And(fv)                =>
+            val clauses = fv.foldLeft(Option(mutable.ArrayBuffer[Clause]())) {
+              case (Some(cnf), ToDisjunction(clauses)) =>
+                Some(cnf ++= clauses)
+              case (_, _)                              =>
+                None
+            }
+            clauses.map(c => Solvable(c.toArray, symbolMapping))
+          case _                      => None
+        }
+      }
+    }
 
-//      debug.patmat("cnf for\n"+ p +"\nis:\n"+cnfString(res))
-      res
+    def eqFreePropToSolvable(p: Prop): Solvable = {
+
+      // collect all variables since after simplification / CNF conversion
+      // they could have been removed from the formula
+      val symbolMapping = new SymbolMapping(gatherSymbols(p))
+
+      val simplified = simplify(p)
+      val cnfExtractor = new AlreadyInCNF(symbolMapping)
+      simplified match {
+        case cnfExtractor.ToCnf(solvable) =>
+          // this is needed because t6942 would generate too many clauses with Tseitin
+          // already in CNF, just add clauses
+          solvable
+        case p                           =>
+          new TransformToCnf(symbolMapping).apply(p)
+      }
     }
   }
 
   // simple solver using DPLL
   trait Solver extends CNF {
-    // a literal is a (possibly negated) variable
-    def Lit(sym: Sym, pos: Boolean = true) = new Lit(sym, pos)
-    class Lit(val sym: Sym, val pos: Boolean) {
-      override def toString = if (!pos) "-"+ sym.toString else sym.toString
-      override def equals(o: Any) = o match {
-        case o: Lit => (o.sym eq sym) && (o.pos == pos)
-        case _ => false
-      }
-      override def hashCode = sym.hashCode + pos.hashCode
+    import scala.collection.mutable.ArrayBuffer
 
-      def unary_- = Lit(sym, !pos)
+    def cnfString(f: Array[Clause]): String = {
+      val lits: Array[List[String]] = f map (_.map(_.toString).toList)
+      val xss: List[List[String]] = lits toList
+      val aligned: String = alignAcrossRows(xss, "\\/", " /\\\n")
+      aligned
     }
 
-    def cnfString(f: Formula) = alignAcrossRows(f map (_.toList) toList, "\\/", " /\\\n")
-
     // adapted from http://lara.epfl.ch/w/sav10:simple_sat_solver (original by Hossein Hojjat)
+
+    // empty set of clauses is trivially satisfied
     val EmptyModel = Map.empty[Sym, Boolean]
+
+    // no model: originates from the encounter of an empty clause, i.e.,
+    // happens if all variables have been assigned in a way that makes the corresponding literals false
+    // thus there is no possibility to satisfy that clause, so the whole formula is UNSAT
     val NoModel: Model = null
 
+    // this model contains the auxiliary variables as well
+    type TseitinModel = Set[Lit]
+    val EmptyTseitinModel = Set.empty[Lit]
+    val NoTseitinModel: TseitinModel = null
+
     // returns all solutions, if any (TODO: better infinite recursion backstop -- detect fixpoint??)
-    def findAllModelsFor(f: Formula): List[Model] = {
+    def findAllModelsFor(solvable: Solvable): List[Model] = {
+      debug.patmat("find all models for\n"+ cnfString(solvable.cnf))
 
-      debug.patmat("find all models for\n"+ cnfString(f))
+      // we must take all vars from non simplified formula
+      // otherwise if we get `T` as formula, we don't expand the variables
+      // that are not in the formula...
+      val relevantVars: Set[Int] = solvable.symbolMapping.relevantVars
 
-      val vars: Set[Sym] = f.flatMap(_ collect {case l: Lit => l.sym}).toSet
       // debug.patmat("vars "+ vars)
       // the negation of a model -(S1=True/False /\ ... /\ SN=True/False) = clause(S1=False/True, ...., SN=False/True)
-      def negateModel(m: Model) = clause(m.toSeq.map{ case (sym, pos) => Lit(sym, !pos) } : _*)
+      // (i.e. the blocking clause - used for ALL-SAT)
+      def negateModel(m: TseitinModel) = {
+        // filter out auxiliary Tseitin variables
+        val relevantLits = m.filter(l => relevantVars.contains(l.variable))
+        relevantLits.map(lit => -lit)
+      }
 
       /**
        * The DPLL procedure only returns a minimal mapping from literal to value
@@ -157,11 +316,11 @@ trait Solving extends Logic {
        * The expansion step will amend both solutions with the unassigned variable
        * i.e., {a = true} will be expanded to {a = true, b = true} and {a = true, b = false}.
        */
-      def expandUnassigned(unassigned: List[Sym], model: Model): List[Model] = {
+      def expandUnassigned(unassigned: List[Int], model: TseitinModel): List[TseitinModel] = {
         // the number of solutions is doubled for every unassigned variable
         val expandedModels = 1 << unassigned.size
-        var current = mutable.ArrayBuffer[Model]()
-        var next = mutable.ArrayBuffer[Model]()
+        var current = mutable.ArrayBuffer[TseitinModel]()
+        var next = mutable.ArrayBuffer[TseitinModel]()
         current.sizeHint(expandedModels)
         next.sizeHint(expandedModels)
 
@@ -175,10 +334,10 @@ trait Solving extends Logic {
           for {
             model <- current
           } {
-            def force(l: Lit) = model + (l.sym -> l.pos)
+            def force(l: Lit) = model + l
 
-            next += force(Lit(s, pos = true))
-            next += force(Lit(s, pos = false))
+            next += force(Lit(s))
+            next += force(Lit(-s))
           }
 
           val tmp = current
@@ -191,67 +350,80 @@ trait Solving extends Logic {
         current.toList
       }
 
-      def findAllModels(f: Formula,
-                        models: List[Model],
-                        recursionDepthAllowed: Int = global.settings.YpatmatExhaustdepth.value): List[Model]=
+      def findAllModels(clauses: Array[Clause],
+                        models: List[TseitinModel],
+                        recursionDepthAllowed: Int = global.settings.YpatmatExhaustdepth.value): List[TseitinModel]=
         if (recursionDepthAllowed == 0) {
           val maxDPLLdepth = global.settings.YpatmatExhaustdepth.value
           reportWarning("(Exhaustivity analysis reached max recursion depth, not all missing cases are reported. " +
               s"Please try with scalac -Ypatmat-exhaust-depth ${maxDPLLdepth * 2} or -Ypatmat-exhaust-depth off.)")
           models
         } else {
-          val model = findModelFor(f)
+          debug.patmat("find all models for\n" + cnfString(clauses))
+          val model = findTseitinModelFor(clauses)
           // if we found a solution, conjunct the formula with the model's negation and recurse
-          if (model ne NoModel) {
-            val unassigned = (vars -- model.keySet).toList
+          if (model ne NoTseitinModel) {
+            // note that we should not expand the auxiliary variables (from Tseitin transformation)
+            // since they are existentially quantified in the final solution
+            val unassigned: List[Int] = (relevantVars -- model.map(lit => lit.variable)).toList
             debug.patmat("unassigned "+ unassigned +" in "+ model)
 
             val forced = expandUnassigned(unassigned, model)
             debug.patmat("forced "+ forced)
             val negated = negateModel(model)
-            findAllModels(f :+ negated, forced ++ models, recursionDepthAllowed - 1)
+            findAllModels(clauses :+ negated, forced ++ models, recursionDepthAllowed - 1)
           }
           else models
         }
 
-      findAllModels(f, Nil)
+      val tseitinModels: List[TseitinModel] = findAllModels(solvable.cnf, Nil)
+      val models: List[Model] = tseitinModels.map(projectToModel(_, solvable.symbolMapping.symForVar))
+      models
     }
 
-    private def withLit(res: Model, l: Lit): Model = if (res eq NoModel) NoModel else res + (l.sym -> l.pos)
-    private def dropUnit(f: Formula, unitLit: Lit): Formula = {
+    private def withLit(res: TseitinModel, l: Lit): TseitinModel = {
+      if (res eq NoTseitinModel) NoTseitinModel else res + l
+    }
+
+    /** Drop trivially true clauses, simplify others by dropping negation of `unitLit`.
+     *
+     *  Disjunctions that contain the literal we're making true in the returned model are trivially true.
+     *  Clauses can be simplified by dropping the negation of the literal we're making true
+     *  (since False \/ X == X)
+     */
+    private def dropUnit(clauses: Array[Clause], unitLit: Lit): Array[Clause] = {
       val negated = -unitLit
-      // drop entire clauses that are trivially true
-      // (i.e., disjunctions that contain the literal we're making true in the returned model),
-      // and simplify clauses by dropping the negation of the literal we're making true
-      // (since False \/ X == X)
-      val dropped = formulaBuilderSized(f.size)
-      for {
-        clause <- f
-        if !(clause contains unitLit)
-      } dropped += (clause - negated)
-      dropped
+      val simplified = new ArrayBuffer[Clause](clauses.size)
+      clauses foreach {
+        case trivial if trivial contains unitLit => // drop
+        case clause                              => simplified += clause - negated
+      }
+      simplified.toArray
     }
 
-    def findModelFor(f: Formula): Model = {
-      @inline def orElse(a: Model, b: => Model) = if (a ne NoModel) a else b
+    def findModelFor(solvable: Solvable): Model = {
+      projectToModel(findTseitinModelFor(solvable.cnf), solvable.symbolMapping.symForVar)
+    }
 
-      debug.patmat("DPLL\n"+ cnfString(f))
+    def findTseitinModelFor(clauses: Array[Clause]): TseitinModel = {
+      @inline def orElse(a: TseitinModel, b: => TseitinModel) = if (a ne NoTseitinModel) a else b
+
+      debug.patmat(s"DPLL\n${cnfString(clauses)}")
 
       val start = if (Statistics.canEnable) Statistics.startTimer(patmatAnaDPLL) else null
 
-      val satisfiableWithModel: Model =
-        if (f isEmpty) EmptyModel
-        else if(f exists (_.isEmpty)) NoModel
-        else f.find(_.size == 1) match {
+      val satisfiableWithModel: TseitinModel =
+        if (clauses isEmpty) EmptyTseitinModel
+        else if (clauses exists (_.isEmpty)) NoTseitinModel
+        else clauses.find(_.size == 1) match {
           case Some(unitClause) =>
             val unitLit = unitClause.head
-            // debug.patmat("unit: "+ unitLit)
-            withLit(findModelFor(dropUnit(f, unitLit)), unitLit)
+            withLit(findTseitinModelFor(dropUnit(clauses, unitLit)), unitLit)
           case _ =>
             // partition symbols according to whether they appear in positive and/or negative literals
-            val pos = new mutable.HashSet[Sym]()
-            val neg = new mutable.HashSet[Sym]()
-            mforeach(f)(lit => if (lit.pos) pos += lit.sym else neg += lit.sym)
+            val pos = new mutable.HashSet[Int]()
+            val neg = new mutable.HashSet[Int]()
+            mforeach(clauses)(lit => if (lit.positive) pos += lit.variable else neg += lit.variable)
 
             // appearing in both positive and negative
             val impures = pos intersect neg
@@ -259,23 +431,38 @@ trait Solving extends Logic {
             val pures = (pos ++ neg) -- impures
 
             if (pures nonEmpty) {
-              val pureSym = pures.head
+              val pureVar = pures.head
               // turn it back into a literal
               // (since equality on literals is in terms of equality
               //  of the underlying symbol and its positivity, simply construct a new Lit)
-              val pureLit = Lit(pureSym, pos(pureSym))
+              val pureLit = Lit(if (neg(pureVar)) -pureVar else pureVar)
               // debug.patmat("pure: "+ pureLit +" pures: "+ pures +" impures: "+ impures)
-              val simplified = f.filterNot(_.contains(pureLit))
-              withLit(findModelFor(simplified), pureLit)
+              val simplified = clauses.filterNot(_.contains(pureLit))
+              withLit(findTseitinModelFor(simplified), pureLit)
             } else {
-              val split = f.head.head
+              val split = clauses.head.head
               // debug.patmat("split: "+ split)
-              orElse(findModelFor(f :+ clause(split)), findModelFor(f :+ clause(-split)))
+              orElse(findTseitinModelFor(clauses :+ clause(split)), findTseitinModelFor(clauses :+ clause(-split)))
             }
         }
 
       if (Statistics.canEnable) Statistics.stopTimer(patmatAnaDPLL, start)
       satisfiableWithModel
     }
+
+    private def projectToModel(model: TseitinModel, symForVar: Map[Int, Sym]): Model =
+      if (model == NoTseitinModel) NoModel
+      else if (model == EmptyTseitinModel) EmptyModel
+      else {
+        val mappedModels = model.toList collect {
+          case lit if symForVar isDefinedAt lit.variable => (symForVar(lit.variable), lit.positive)
+        }
+        if (mappedModels.isEmpty) {
+          // could get an empty model if mappedModels is a constant like `True`
+          EmptyModel
+        } else {
+          mappedModels.toMap
+        }
+      }
   }
 }
diff --git a/src/intellij/test/files/neg/virtpatmat_exhaust_big.check b/src/intellij/test/files/neg/virtpatmat_exhaust_big.check
new file mode 100644
index 0000000000..fddc85a362
--- /dev/null
+++ b/src/intellij/test/files/neg/virtpatmat_exhaust_big.check
@@ -0,0 +1,7 @@
+virtpatmat_exhaust_big.scala:27: warning: match may not be exhaustive.
+It would fail on the following input: Z11()
+  def foo(z: Z) = z match {
+                  ^
+error: No warnings can be incurred under -Xfatal-warnings.
+one warning found
+one error found
diff --git a/src/intellij/test/files/neg/virtpatmat_exhaust_big.flags b/src/intellij/test/files/neg/virtpatmat_exhaust_big.flags
new file mode 100644
index 0000000000..b5a8748652
--- /dev/null
+++ b/src/intellij/test/files/neg/virtpatmat_exhaust_big.flags
@@ -0,0 +1 @@
+-Xfatal-warnings -unchecked
diff --git a/src/intellij/test/files/neg/virtpatmat_exhaust_big.scala b/src/intellij/test/files/neg/virtpatmat_exhaust_big.scala
new file mode 100644
index 0000000000..dd639eb56e
--- /dev/null
+++ b/src/intellij/test/files/neg/virtpatmat_exhaust_big.scala
@@ -0,0 +1,32 @@
+sealed abstract class Z
+object Z {
+   object     Z0    extends Z
+   case class Z1()  extends Z
+   object     Z2    extends Z
+   case class Z3()  extends Z
+   object     Z4    extends Z
+   case class Z5()  extends Z
+   object     Z6    extends Z
+   case class Z7()  extends Z
+   object     Z8    extends Z
+   case class Z9()  extends Z
+   object     Z10   extends Z
+   case class Z11() extends Z
+   object     Z12   extends Z
+   case class Z13() extends Z
+   object     Z14   extends Z
+   case class Z15() extends Z
+   object     Z16   extends Z
+   case class Z17() extends Z
+   object     Z18   extends Z
+   case class Z19() extends Z
+}
+
+object Test {
+  import Z._
+  def foo(z: Z) = z match {
+    case Z0  | Z1()  | Z2  | Z3()  | Z4  | Z5()  | Z6  | Z7()  | Z8  | Z9() |
+         Z10 | Z12 | Z13() | Z14 | Z15() | Z16 | Z17() | Z18 | Z19()
+         =>
+  }
+}
diff --git a/src/intellij/test/files/pos/virtpatmat_exhaust_big.scala b/src/intellij/test/files/pos/virtpatmat_exhaust_big.scala
new file mode 100644
index 0000000000..41aef3226e
--- /dev/null
+++ b/src/intellij/test/files/pos/virtpatmat_exhaust_big.scala
@@ -0,0 +1,34 @@
+sealed abstract class Z
+object Z {
+   object     Z0    extends Z
+   case class Z1()  extends Z
+   object     Z2    extends Z
+   case class Z3()  extends Z
+   object     Z4    extends Z
+   case class Z5()  extends Z
+   object     Z6    extends Z
+   case class Z7()  extends Z
+   object     Z8    extends Z
+   case class Z9()  extends Z
+   object     Z10   extends Z
+   case class Z11() extends Z
+   object     Z12   extends Z
+   case class Z13() extends Z
+   object     Z14   extends Z
+   case class Z15() extends Z
+   object     Z16   extends Z
+   case class Z17() extends Z
+   object     Z18   extends Z
+   case class Z19() extends Z
+}
+
+// drop any case and it will report an error
+object Test {
+  import Z._
+  def foo(z: Z) = z match {
+    case Z0  | Z1()  | Z2  | Z3()  | Z4  | Z5()  | Z6  | Z7()  | Z8  | Z9() |
+         Z10 | Z11() | Z12 | Z13() | Z14 | Z15() | Z16 | Z17() | Z18 | Z19()
+         =>
+  }
+}
+- 
diff --git a/test/files/neg/t6582_exhaust_big.check b/test/files/neg/t6582_exhaust_big.check
new file mode 100644
index 0000000000..9e2be038b5
--- /dev/null
+++ b/test/files/neg/t6582_exhaust_big.check
@@ -0,0 +1,7 @@
+t6582_exhaust_big.scala:27: warning: match may not be exhaustive.
+It would fail on the following input: Z11()
+  def foo(z: Z) = z match {
+                  ^
+error: No warnings can be incurred under -Xfatal-warnings.
+one warning found
+one error found
diff --git a/test/files/neg/t6582_exhaust_big.flags b/test/files/neg/t6582_exhaust_big.flags
new file mode 100644
index 0000000000..b5a8748652
--- /dev/null
+++ b/test/files/neg/t6582_exhaust_big.flags
@@ -0,0 +1 @@
+-Xfatal-warnings -unchecked
diff --git a/test/files/neg/t6582_exhaust_big.scala b/test/files/neg/t6582_exhaust_big.scala
new file mode 100644
index 0000000000..dd639eb56e
--- /dev/null
+++ b/test/files/neg/t6582_exhaust_big.scala
@@ -0,0 +1,32 @@
+sealed abstract class Z
+object Z {
+   object     Z0    extends Z
+   case class Z1()  extends Z
+   object     Z2    extends Z
+   case class Z3()  extends Z
+   object     Z4    extends Z
+   case class Z5()  extends Z
+   object     Z6    extends Z
+   case class Z7()  extends Z
+   object     Z8    extends Z
+   case class Z9()  extends Z
+   object     Z10   extends Z
+   case class Z11() extends Z
+   object     Z12   extends Z
+   case class Z13() extends Z
+   object     Z14   extends Z
+   case class Z15() extends Z
+   object     Z16   extends Z
+   case class Z17() extends Z
+   object     Z18   extends Z
+   case class Z19() extends Z
+}
+
+object Test {
+  import Z._
+  def foo(z: Z) = z match {
+    case Z0  | Z1()  | Z2  | Z3()  | Z4  | Z5()  | Z6  | Z7()  | Z8  | Z9() |
+         Z10 | Z12 | Z13() | Z14 | Z15() | Z16 | Z17() | Z18 | Z19()
+         =>
+  }
+}
diff --git a/test/files/pos/t6582_exhaust_big.scala b/test/files/pos/t6582_exhaust_big.scala
new file mode 100644
index 0000000000..7bb8879805
--- /dev/null
+++ b/test/files/pos/t6582_exhaust_big.scala
@@ -0,0 +1,33 @@
+sealed abstract class Z
+object Z {
+   object     Z0    extends Z
+   case class Z1()  extends Z
+   object     Z2    extends Z
+   case class Z3()  extends Z
+   object     Z4    extends Z
+   case class Z5()  extends Z
+   object     Z6    extends Z
+   case class Z7()  extends Z
+   object     Z8    extends Z
+   case class Z9()  extends Z
+   object     Z10   extends Z
+   case class Z11() extends Z
+   object     Z12   extends Z
+   case class Z13() extends Z
+   object     Z14   extends Z
+   case class Z15() extends Z
+   object     Z16   extends Z
+   case class Z17() extends Z
+   object     Z18   extends Z
+   case class Z19() extends Z
+}
+
+// drop any case and it will report an error
+object Test {
+  import Z._
+  def foo(z: Z) = z match {
+    case Z0  | Z1()  | Z2  | Z3()  | Z4  | Z5()  | Z6  | Z7()  | Z8  | Z9() |
+         Z10 | Z11() | Z12 | Z13() | Z14 | Z15() | Z16 | Z17() | Z18 | Z19()
+         =>
+  }
+}