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

The exhaustivity checks in the pattern matcher build a propositional
formula that must be converted into conjunctive normal form (CNF) in
order to be amenable to the following DPLL decision procedure.
However, the simple conversion into CNF via negation normal form and
Shannon expansion that was used has exponential worst-case complexity
and thus even simple problems could become untractable.

A better approach is to use a transformation into an _equisatisfiable_
CNF-formula (by generating auxiliary variables) that runs with linear
complexity. The commonly known Tseitin transformation uses bi-
implication. I have choosen for an enhancement: the Plaisted
transformation which 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.

I implemented only optimizations that had a substantial
effect on formula size:
- formula simplification, extraction of multi argument operands
- if a formula is already in CNF then the Tseitin/Plaisted
  transformation is omitted
- Plaisted via NNF
- omitted: (sharing of sub-formulas is also not implemented)
- omitted: (clause subsumption)

11 files changed, 646 insertions, 268 deletions

diff --git a/src/compiler/scala/tools/nsc/transform/patmat/Logic.scala b/src/compiler/scala/tools/nsc/transform/patmat/Logic.scala
index d10b8eb84f..75d2cfe0f2 100644
--- a/src/compiler/scala/tools/nsc/transform/patmat/Logic.scala
+++ b/src/compiler/scala/tools/nsc/transform/patmat/Logic.scala
@@ -11,7 +11,6 @@ import scala.language.postfixOps
 import scala.collection.mutable
 import scala.reflect.internal.util.Statistics
 import scala.reflect.internal.util.HashSet
-import scala.annotation.tailrec
 
 trait Logic extends Debugging  {
   import PatternMatchingStats._
@@ -104,21 +103,16 @@ trait Logic extends Debugging  {
       def implications: List[(Sym, List[Sym], List[Sym])]
     }
 
-    private def propToLinkedHashSet(ops: Seq[Prop]) = {
-      val set = new mutable.LinkedHashSet[Prop]()
-      ops.foreach(set += _)
-      set
-    }
-
     // 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)
-    final case class And(ops: mutable.LinkedHashSet[Prop]) extends Prop
+    final case class And(ops: Set[Prop]) extends Prop
     object And {
-      def apply(ops: Prop*) = new And(propToLinkedHashSet(ops))
+      def apply(ops: Prop*) = new And(ops.toSet)
     }
-    final case class Or(ops: mutable.LinkedHashSet[Prop]) extends Prop
+
+    final case class Or(ops: Set[Prop]) extends Prop
     object Or {
-      def apply(ops: Prop*) = new Or(propToLinkedHashSet(ops))
+      def apply(ops: Prop*) = new Or(ops.toSet)
     }
 
     final case class Not(a: Prop) extends Prop
@@ -146,6 +140,98 @@ trait Logic extends Debugging  {
     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 {
@@ -153,10 +239,12 @@ trait Logic extends Debugging  {
         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] = {
@@ -167,6 +255,14 @@ 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(ops) => And(ops map apply)
@@ -176,27 +272,10 @@ trait Logic extends Debugging  {
       }
     }
 
-    // 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
@@ -217,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]
@@ -241,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 =>
@@ -270,49 +349,30 @@ trait Logic extends Debugging  {
         }
       }
 
-      debug.patmat(s"eqAxioms:\n$eqAxioms")
+      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/Solving.scala b/src/compiler/scala/tools/nsc/transform/patmat/Solving.scala
index c5475b50c0..1ba13c0617 100644
--- a/src/compiler/scala/tools/nsc/transform/patmat/Solving.scala
+++ b/src/compiler/scala/tools/nsc/transform/patmat/Solving.scala
@@ -6,148 +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(ps) => Or (ps map (negationNormalFormNot(_, budget - 1)))
-          case Or(ps)  => And(ps map (negationNormalFormNot(_, 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 Or(ps)        => Or (ps map (negationNormalForm(_, budget - 1)))
-          case And(ps)       => And(ps map (negationNormalForm(_, 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(ps)   =>
-            val formula = formulaBuilder
-            ps foreach { p =>
-              val cnf = conjunctiveNormalForm(p, budget - 1)
-              addFormula(formula, cnf)
-            }
-            toFormula(formula)
-          case Or(ps)    =>
-            ps map (conjunctiveNormalForm(_)) reduceLeft { (a, b) =>
-              distribute(a, b, budget - (a.size + b.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
+        }
+      }
 
-//      debug.patmat("cnf for\n"+ p +"\nis:\n"+cnfString(res))
-      res
+      /**
+       * 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
+        }
+      }
+    }
+
+    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
@@ -160,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)
 
@@ -178,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
@@ -194,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
@@ -262,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()
+         =>
+  }
+}