Merge pull request #650 from adriaanm/topic-virtpatmat

Unreachability analysis for pattern matches

Thanks for reviewing, @retronym!

13 files changed, 916 insertions, 365 deletions

diff --git a/src/compiler/scala/reflect/internal/settings/MutableSettings.scala b/src/compiler/scala/reflect/internal/settings/MutableSettings.scala
index 45ba4ed3e6..8640a23aa7 100644
--- a/src/compiler/scala/reflect/internal/settings/MutableSettings.scala
+++ b/src/compiler/scala/reflect/internal/settings/MutableSettings.scala
@@ -44,4 +44,5 @@ abstract class MutableSettings extends AbsSettings {
   def maxClassfileName: IntSetting
   def Xexperimental: BooleanSetting
   def XoldPatmat: BooleanSetting
+  def XnoPatmatAnalysis: BooleanSetting
 }
\ No newline at end of file
diff --git a/src/compiler/scala/reflect/runtime/Settings.scala b/src/compiler/scala/reflect/runtime/Settings.scala
index bbe4d60e9c..b247797c6c 100644
--- a/src/compiler/scala/reflect/runtime/Settings.scala
+++ b/src/compiler/scala/reflect/runtime/Settings.scala
@@ -35,4 +35,5 @@ class Settings extends internal.settings.MutableSettings {
   val Xexperimental = new BooleanSetting(false)
   val deepCloning = new BooleanSetting (false)
   val XoldPatmat = new BooleanSetting(false)
+  val XnoPatmatAnalysis = new BooleanSetting(false)
 }
diff --git a/src/compiler/scala/tools/nsc/settings/ScalaSettings.scala b/src/compiler/scala/tools/nsc/settings/ScalaSettings.scala
index efde2cee25..88a89d54eb 100644
--- a/src/compiler/scala/tools/nsc/settings/ScalaSettings.scala
+++ b/src/compiler/scala/tools/nsc/settings/ScalaSettings.scala
@@ -109,6 +109,7 @@ trait ScalaSettings extends AbsScalaSettings
   val sourceReader  = StringSetting     ("-Xsource-reader", "classname", "Specify a custom method for reading source files.", "")
 
   val XoldPatmat    = BooleanSetting    ("-Xoldpatmat", "Use the pre-2.10 pattern matcher. Otherwise, the 'virtualizing' pattern matcher is used in 2.10.")
+  val XnoPatmatAnalysis = BooleanSetting ("-Xno-patmat-analysis", "Don't perform exhaustivity/unreachability analysis. Also, ignore @switch annotation.")
 
   /** Compatibility stubs for options whose value name did
    *  not previously match the option name.
diff --git a/src/compiler/scala/tools/nsc/typechecker/PatternMatching.scala b/src/compiler/scala/tools/nsc/typechecker/PatternMatching.scala
index b36a92a186..48985213d1 100644
--- a/src/compiler/scala/tools/nsc/typechecker/PatternMatching.scala
+++ b/src/compiler/scala/tools/nsc/typechecker/PatternMatching.scala
@@ -14,6 +14,7 @@ import scala.tools.nsc.transform.TypingTransformers
 import scala.tools.nsc.transform.Transform
 import scala.collection.mutable.HashSet
 import scala.collection.mutable.HashMap
+import scala.tools.nsc.util.Statistics
 
 /** Translate pattern matching.
   *
@@ -26,11 +27,9 @@ import scala.collection.mutable.HashMap
   * Cases are combined into a pattern match using the `orElse` combinator (the implicit failure case is expressed using the monad's `zero`).
   *
   * TODO:
-  *  - exhaustivity
-  *  - DCE (unreachability/refutability/optimization)
   *  - use TypeTags for type testing
-  *  - Array patterns
-  *  - implement spec more closely (see TODO's)
+  *  - DCE (on irrefutable patterns)
+  *  - update spec and double check it's implemented correctly (see TODO's)
   *
   * (longer-term) TODO:
   *  - user-defined unapplyProd
@@ -38,6 +37,8 @@ import scala.collection.mutable.HashMap
   *  - recover exhaustivity and unreachability checking using a variation on the type-safe builder pattern
   */
 trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL {   // self: Analyzer =>
+  import Statistics._
+
   val global: Global               // need to repeat here because otherwise last mixin defines global as
                                    // SymbolTable. If we had DOT this would not be an issue
   import global._                  // the global environment
@@ -45,6 +46,8 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL
 
   val phaseName: String = "patmat"
 
+  def patmatDebug(msg: String) = println(msg)
+
   def newTransformer(unit: CompilationUnit): Transformer =
     if (opt.virtPatmat) new MatchTransformer(unit)
     else noopTransformer
@@ -173,13 +176,15 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL
       // (that would require more sophistication when generating trees,
       //  and the only place that emits Matches after typers is for exception handling anyway)
       if(phase.id >= currentRun.uncurryPhase.id) debugwarn("running translateMatch at "+ phase +" on "+ selector +" match "+ cases)
-      // println("translating "+ cases.mkString("{", "\n", "}"))
+      // patmatDebug("translating "+ cases.mkString("{", "\n", "}"))
 
       def repeatedToSeq(tp: Type): Type = (tp baseType RepeatedParamClass) match {
         case TypeRef(_, RepeatedParamClass, arg :: Nil) => seqType(arg)
         case _                                          => tp
       }
 
+      val start = startTimer(patmatNanos)
+
       val selectorTp = repeatedToSeq(elimAnonymousClass(selector.tpe.widen.withoutAnnotations))
 
       val origPt  = match_.tpe
@@ -203,7 +208,10 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL
 
       val selectorSym  = freshSym(selector.pos, pureType(selectorTp)) setFlag SYNTH_CASE
       // pt = Any* occurs when compiling test/files/pos/annotDepMethType.scala  with -Xexperimental
-      combineCases(selector, selectorSym, cases map translateCase(selectorSym, pt), pt, matchOwner, matchFailGenOverride)
+      val combined = combineCases(selector, selectorSym, cases map translateCase(selectorSym, pt), pt, matchOwner, matchFailGenOverride)
+
+      stopTimer(patmatNanos, start)
+      combined
     }
 
     // return list of typed CaseDefs that are supported by the backend (typed/bind/wildcard)
@@ -297,9 +305,9 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL
         // as b.info may be based on a Typed type ascription, which has not been taken into account yet by the translation
         // (it will later result in a type test when `tp` is not a subtype of `b.info`)
         // TODO: can we simplify this, together with the Bound case?
-        (extractor.subPatBinders, extractor.subPatTypes).zipped foreach { case (b, tp) => b setInfo tp } // println("changing "+ b +" : "+ b.info +" -> "+ tp);
+        (extractor.subPatBinders, extractor.subPatTypes).zipped foreach { case (b, tp) => b setInfo tp } // patmatDebug("changing "+ b +" : "+ b.info +" -> "+ tp);
 
-        // println("translateExtractorPattern checking parameter type: "+ (patBinder, patBinder.info.widen, extractor.paramType, patBinder.info.widen <:< extractor.paramType))
+        // patmatDebug("translateExtractorPattern checking parameter type: "+ (patBinder, patBinder.info.widen, extractor.paramType, patBinder.info.widen <:< extractor.paramType))
         // example check: List[Int] <:< ::[Int]
         // TODO: extractor.paramType may contain unbound type params (run/t2800, run/t3530)
         val (typeTestTreeMaker, patBinderOrCasted) =
@@ -337,7 +345,7 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL
         case WildcardPattern() => noFurtherSubPats()
         case UnApply(unfun, args) =>
           // TODO: check unargs == args
-          // println("unfun: "+ (unfun.tpe, unfun.symbol.ownerChain, unfun.symbol.info, patBinder.info))
+          // patmatDebug("unfun: "+ (unfun.tpe, unfun.symbol.ownerChain, unfun.symbol.info, patBinder.info))
           translateExtractorPattern(ExtractorCall(unfun, args))
 
         /** A constructor pattern is of the form c(p1, ..., pn) where n ≥ 0.
@@ -403,7 +411,7 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL
       */
 
         case Bind(n, p) => // this happens in certain ill-formed programs, there'll be an error later
-          // println("WARNING: Bind tree with unbound symbol "+ patTree)
+          // patmatDebug("WARNING: Bind tree with unbound symbol "+ patTree)
           noFurtherSubPats() // there's no symbol -- something's wrong... don't fail here though (or should we?)
 
         // case Star(_) | ArrayValue | This => error("stone age pattern relics encountered!")
@@ -476,13 +484,13 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL
                 // this fails to resolve overloading properly...
                 // Apply(typedOperator(Select(orig, extractor)), List(Ident(nme.SELECTOR_DUMMY))) // no need to set the type of the dummy arg, it will be replaced anyway
 
-                // println("funtpe after = "+ fun.tpe.finalResultType)
-                // println("orig: "+(orig, orig.tpe))
+                // patmatDebug("funtpe after = "+ fun.tpe.finalResultType)
+                // patmatDebug("orig: "+(orig, orig.tpe))
                 val tgt = typed(orig, EXPRmode | QUALmode | POLYmode, HasMember(extractor.name)) // can't specify fun.tpe.finalResultType as the type for the extractor's arg,
                 // as it may have been inferred incorrectly (see t602, where it's  com.mosol.sl.Span[Any], instead of  com.mosol.sl.Span[?K])
-                // println("tgt = "+ (tgt, tgt.tpe))
+                // patmatDebug("tgt = "+ (tgt, tgt.tpe))
                 val oper = typed(Select(tgt, extractor.name), EXPRmode | FUNmode | POLYmode | TAPPmode, WildcardType)
-                // println("oper: "+ (oper, oper.tpe))
+                // patmatDebug("oper: "+ (oper, oper.tpe))
                 Apply(oper, List(Ident(nme.SELECTOR_DUMMY))) // no need to set the type of the dummy arg, it will be replaced anyway
             }
           } finally context.undetparams = savedUndets
@@ -598,8 +606,8 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL
       // private val orig            = fun match {case tpt: TypeTree => tpt.original case _ => fun}
       // private val origExtractorTp = unapplyMember(orig.symbol.filter(sym => reallyExists(unapplyMember(sym.tpe))).tpe).tpe
       // private val extractorTp     = if (wellKinded(fun.tpe)) fun.tpe else existentialAbstraction(origExtractorTp.typeParams, origExtractorTp.resultType)
-      // println("ExtractorCallProd: "+ (fun.tpe, existentialAbstraction(origExtractorTp.typeParams, origExtractorTp.resultType)))
-      // println("ExtractorCallProd: "+ (fun.tpe, args map (_.tpe)))
+      // patmatDebug("ExtractorCallProd: "+ (fun.tpe, existentialAbstraction(origExtractorTp.typeParams, origExtractorTp.resultType)))
+      // patmatDebug("ExtractorCallProd: "+ (fun.tpe, args map (_.tpe)))
       private def constructorTp = fun.tpe
 
       def isTyped    = fun.isTyped
@@ -627,14 +635,14 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL
 
         def indexInCPA(acc: Symbol) =
           constrParamAccessors indexWhere { orig =>
-            // println("compare: "+ (orig, acc, orig.name, acc.name, (acc.name == orig.name), (acc.name startsWith (orig.name append "$"))))
+            // patmatDebug("compare: "+ (orig, acc, orig.name, acc.name, (acc.name == orig.name), (acc.name startsWith (orig.name append "$"))))
             val origName  = orig.name.toString.trim
             val accName = acc.name.toString.trim
             (accName == origName) || (accName startsWith (origName + "$"))
           }
 
-        // println("caseFieldAccessors: "+ (accessors, binder.caseFieldAccessors map indexInCPA))
-        // println("constrParamAccessors: "+ constrParamAccessors)
+        // patmatDebug("caseFieldAccessors: "+ (accessors, binder.caseFieldAccessors map indexInCPA))
+        // patmatDebug("constrParamAccessors: "+ constrParamAccessors)
 
         val accessorsSorted = accessors sortBy indexInCPA
         if (accessorsSorted isDefinedAt (i-1)) REF(binder) DOT accessorsSorted(i-1)
@@ -793,6 +801,8 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL
       None
 
     abstract class TreeMaker {
+      def pos: Position
+
       /** captures the scope and the value of the bindings in patterns
        * important *when* the substitution happens (can't accumulate and do at once after the full matcher has been constructed)
        */
@@ -804,7 +814,7 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL
 
       private[TreeMakers] def incorporateOuterSubstitution(outerSubst: Substitution): Unit = {
         if (currSub ne null) {
-          println("BUG: incorporateOuterSubstitution called more than once for "+ (this, currSub, outerSubst))
+          // patmatDebug("BUG: incorporateOuterSubstitution called more than once for "+ (this, currSub, outerSubst))
           Thread.dumpStack()
         }
         else currSub = outerSubst >> substitution
@@ -820,16 +830,22 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL
     }
 
     case class TrivialTreeMaker(tree: Tree) extends TreeMaker with NoNewBinders {
+      def pos = tree.pos
+
       def chainBefore(next: Tree)(casegen: Casegen): Tree = tree
     }
 
     case class BodyTreeMaker(body: Tree, matchPt: Type) extends TreeMaker with NoNewBinders {
+      def pos = body.pos
+
       def chainBefore(next: Tree)(casegen: Casegen): Tree = // assert(next eq EmptyTree)
         atPos(body.pos)(casegen.one(substitution(body))) // since SubstOnly treemakers are dropped, need to do it here
       override def toString = "B"+(body, matchPt)
     }
 
     case class SubstOnlyTreeMaker(prevBinder: Symbol, nextBinder: Symbol) extends TreeMaker {
+      val pos = NoPosition
+
       val localSubstitution = Substitution(prevBinder, CODE.REF(nextBinder))
       def chainBefore(next: Tree)(casegen: Casegen): Tree = substitution(next)
       override def toString = "S"+ localSubstitution
@@ -837,10 +853,10 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL
 
     abstract class FunTreeMaker extends TreeMaker {
       val nextBinder: Symbol
+      def pos = nextBinder.pos
     }
 
     abstract class CondTreeMaker extends FunTreeMaker {
-      val pos: Position
       val prevBinder: Symbol
       val nextBinderTp: Type
       val cond: Tree
@@ -962,11 +978,9 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL
         - A parameterized type pattern scala.Array[T1], where T1 is a type pattern. // TODO
           This type pattern matches any non-null instance of type scala.Array[U1], where U1 is a type matched by T1.
     **/
-    case class TypeTestTreeMaker(prevBinder: Symbol, testedBinder: Symbol, expectedTp: Type, nextBinderTp: Type)(_pos: Position, extractorArgTypeTest: Boolean = false) extends CondTreeMaker {
-      val pos = _pos
-
+    case class TypeTestTreeMaker(prevBinder: Symbol, testedBinder: Symbol, expectedTp: Type, nextBinderTp: Type)(override val pos: Position, extractorArgTypeTest: Boolean = false) extends CondTreeMaker {
       import TypeTestTreeMaker._
-      // println("TTTM"+(prevBinder, extractorArgTypeTest, testedBinder, expectedTp, nextBinderTp))
+      // patmatDebug("TTTM"+(prevBinder, extractorArgTypeTest, testedBinder, expectedTp, nextBinderTp))
 
       lazy val outerTestNeeded = (
           !((expectedTp.prefix eq NoPrefix) || expectedTp.prefix.typeSymbol.isPackageClass)
@@ -985,6 +999,9 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL
           if (outerTestNeeded) and(typeTest(testedBinder, expectedTp), outerTest(testedBinder, expectedTp))
           else typeTest(testedBinder, expectedTp)
 
+        // propagate expected type
+        @inline def expTp(t: Tree): t.type = t setType expectedTp
+
         // true when called to type-test the argument to an extractor
         // don't do any fancy equality checking, just test the type
         if (extractorArgTypeTest) default
@@ -994,11 +1011,10 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL
           case SingleType(_, sym)                       => and(equalsTest(CODE.REF(sym), testedBinder), typeTest(testedBinder, expectedTp.widen))
           // must use == to support e.g. List() == Nil
           case ThisType(sym) if sym.isModule            => and(equalsTest(CODE.REF(sym), testedBinder), typeTest(testedBinder, expectedTp.widen))
-          case ConstantType(const)                      => equalsTest(Literal(const), testedBinder)
-
-          case ThisType(sym)                            => eqTest(This(sym), testedBinder)
           case ConstantType(Constant(null)) if testedBinder.info.widen <:< AnyRefClass.tpe
-                                                        => eqTest(CODE.NULL, testedBinder)
+                                                        => eqTest(expTp(CODE.NULL), testedBinder)
+          case ConstantType(const)                      => equalsTest(expTp(Literal(const)), testedBinder)
+          case ThisType(sym)                            => eqTest(expTp(This(sym)), testedBinder)
 
           // TODO: verify that we don't need to special-case Array
           // I think it's okay:
@@ -1023,7 +1039,7 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL
     }
 
     // need to substitute to deal with existential types -- TODO: deal with existentials better, don't substitute (see RichClass during quick.comp)
-    case class EqualityTestTreeMaker(prevBinder: Symbol, patTree: Tree, pos: Position) extends CondTreeMaker {
+    case class EqualityTestTreeMaker(prevBinder: Symbol, patTree: Tree, override val pos: Position) extends CondTreeMaker {
       val nextBinderTp = prevBinder.info.widen
 
       // NOTE: generate `patTree == patBinder`, since the extractor must be in control of the equals method (also, patBinder may be null)
@@ -1056,6 +1072,8 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL
     }
 
     case class GuardTreeMaker(guardTree: Tree) extends TreeMaker with NoNewBinders {
+      val pos = guardTree.pos
+
       def chainBefore(next: Tree)(casegen: Casegen): Tree = casegen.flatMapGuard(substitution(guardTree), next)
       override def toString = "G("+ guardTree +")"
     }
@@ -1090,19 +1108,21 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL
       fixerUpper(owner, scrut.pos){
         val ptDefined    = if (isFullyDefined(pt)) pt else NoType
         def matchFailGen = (matchFailGenOverride orElse Some(CODE.MATCHERROR(_: Tree)))
-        // println("combining cases: "+ (casesNoSubstOnly.map(_.mkString(" >> ")).mkString("{", "\n", "}")))
+        // patmatDebug("combining cases: "+ (casesNoSubstOnly.map(_.mkString(" >> ")).mkString("{", "\n", "}")))
 
         def isSwitchAnnotation(tpe: Type) = tpe hasAnnotation SwitchClass
         def isUncheckedAnnotation(tpe: Type) = tpe hasAnnotation UncheckedClass
 
-        val (unchecked, requireSwitch) = scrut match {
-          case Typed(_, tpt) =>
-            (isUncheckedAnnotation(tpt.tpe),
-             // matches with two or fewer cases need not apply for switchiness (if-then-else will do)
-             isSwitchAnnotation(tpt.tpe) && casesNoSubstOnly.lengthCompare(2) > 0)
-          case _ =>
-            (false, false)
-        }
+        val (unchecked, requireSwitch) =
+          if (settings.XnoPatmatAnalysis.value) (true, false)
+          else scrut match {
+            case Typed(_, tpt) =>
+              (isUncheckedAnnotation(tpt.tpe),
+               // matches with two or fewer cases need not apply for switchiness (if-then-else will do)
+               isSwitchAnnotation(tpt.tpe) && casesNoSubstOnly.lengthCompare(2) > 0)
+            case _ =>
+              (false, false)
+          }
 
         emitSwitch(scrut, scrutSym, casesNoSubstOnly, pt, matchFailGenOverride).getOrElse{
           if (requireSwitch) typer.context.unit.warning(scrut.pos, "could not emit switch for @switch annotated match")
@@ -1145,12 +1165,12 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL
         t match {
           case Function(_, _) if t.symbol == NoSymbol =>
             t.symbol = currentOwner.newAnonymousFunctionValue(t.pos)
-            // println("new symbol for "+ (t, t.symbol.ownerChain))
+            // patmatDebug("new symbol for "+ (t, t.symbol.ownerChain))
           case Function(_, _) if (t.symbol.owner == NoSymbol) || (t.symbol.owner == origOwner) =>
-            // println("fundef: "+ (t, t.symbol.ownerChain, currentOwner.ownerChain))
+            // patmatDebug("fundef: "+ (t, t.symbol.ownerChain, currentOwner.ownerChain))
             t.symbol.owner = currentOwner
           case d : DefTree if (d.symbol != NoSymbol) && ((d.symbol.owner == NoSymbol) || (d.symbol.owner == origOwner)) => // don't indiscriminately change existing owners! (see e.g., pos/t3440, pos/t3534, pos/unapplyContexts2)
-            // println("def: "+ (d, d.symbol.ownerChain, currentOwner.ownerChain))
+            // patmatDebug("def: "+ (d, d.symbol.ownerChain, currentOwner.ownerChain))
             if(d.symbol.isLazy) { // for lazy val's accessor -- is there no tree??
               assert(d.symbol.lazyAccessor != NoSymbol && d.symbol.lazyAccessor.owner == d.symbol.owner, d.symbol.lazyAccessor)
               d.symbol.lazyAccessor.owner = currentOwner
@@ -1160,16 +1180,16 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL
 
             d.symbol.owner = currentOwner
           // case _ if (t.symbol != NoSymbol) && (t.symbol ne null) =>
-          //   println("untouched "+ (t, t.getClass, t.symbol.ownerChain, currentOwner.ownerChain))
+          // patmatDebug("untouched "+ (t, t.getClass, t.symbol.ownerChain, currentOwner.ownerChain))
           case _ =>
         }
         super.traverse(t)
       }
 
       // override def apply
-      // println("before fixerupper: "+ xTree)
+      // patmatDebug("before fixerupper: "+ xTree)
       // currentRun.trackerFactory.snapshot()
-      // println("after fixerupper")
+      // patmatDebug("after fixerupper")
       // currentRun.trackerFactory.snapshot()
     }
   }
@@ -1234,7 +1254,7 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL
       def _asInstanceOf(t: Tree, tp: Type, force: Boolean = false): Tree = if (!force && (t.tpe ne NoType) && t.isTyped && typesConform(t.tpe, tp)) t else mkCast(t, tp)
       def _asInstanceOf(b: Symbol, tp: Type): Tree = if (typesConform(b.info, tp)) REF(b) else mkCast(REF(b), tp)
       def _isInstanceOf(b: Symbol, tp: Type): Tree = gen.mkIsInstanceOf(REF(b), tp.withoutAnnotations, true, false)
-      //   if (typesConform(b.info, tpX)) { println("warning: emitted spurious isInstanceOf: "+(b, tp)); TRUE }
+      //   if (typesConform(b.info, tpX)) { patmatDebug("warning: emitted spurious isInstanceOf: "+(b, tp)); TRUE }
 
       // duplicated out of frustration with cast generation
       def mkZero(tp: Type): Tree = {
@@ -1315,11 +1335,11 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL
       // def andThen_: (prev: List[Test]): List[Test] =
       //   prev.filterNot(this <:< _) :+ this
 
-      private val reusedBy = new collection.mutable.HashSet[Test]
+      // private val reusedBy = new collection.mutable.HashSet[Test]
       var reuses: Option[Test] = None
       def registerReuseBy(later: Test): Unit = {
         assert(later.reuses.isEmpty, later.reuses)
-        reusedBy += later
+        // reusedBy += later
         later.reuses = Some(this)
       }
 
@@ -1414,19 +1434,51 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL
 
 
     // returns (tree, tests), where `tree` will be used to refer to `root` in `tests`
-    abstract class TreeMakersToConds(val root: Symbol, val cases: List[List[TreeMaker]]) {
+    abstract class TreeMakersToConds(val root: Symbol) {
+      def discard() = {
+        pointsToBound.clear()
+        trees.clear()
+        normalize  = EmptySubstitution
+        accumSubst = EmptySubstitution
+      }
       // a variable in this set should never be replaced by a tree that "does not consist of a selection on a variable in this set" (intuitively)
-      private val pointsToBound            = collection.mutable.HashSet(root)
+      private val pointsToBound = collection.mutable.HashSet(root)
+      private val trees         = collection.mutable.HashSet.empty[Tree]
 
       // the substitution that renames variables to variables in pointsToBound
       private var normalize: Substitution  = EmptySubstitution
 
       // replaces a variable (in pointsToBound) by a selection on another variable in pointsToBound
+      // in the end, instead of having x1, x1.hd, x2, x2.hd, ... flying around,
+      // we want something like x1, x1.hd, x1.hd.tl, x1.hd.tl.hd, so that we can easily recognize when
+      // we're testing the same variable
       // TODO check:
       //   pointsToBound -- accumSubst.from == Set(root) && (accumSubst.from.toSet -- pointsToBound) isEmpty
       private var accumSubst: Substitution = EmptySubstitution
 
-      private val trees = new collection.mutable.HashSet[Tree]
+      private def updateSubstitution(subst: Substitution) = {
+        // find part of substitution that replaces bound symbols by new symbols, and reverse that part
+        // so that we don't introduce new aliases for existing symbols, thus keeping the set of bound symbols minimal
+        val (boundSubst, unboundSubst) = (subst.from zip subst.to) partition {
+          case (f, t) =>
+            t.isInstanceOf[Ident] && (t.symbol ne NoSymbol) && pointsToBound(f)
+        }
+        val (boundFrom, boundTo) = boundSubst.unzip
+        val (unboundFrom, unboundTo) = unboundSubst.unzip
+
+        // reverse substitution that would otherwise replace a variable we already encountered by a new variable
+        // NOTE: this forgets the more precise type we have for these later variables, but that's probably okay
+        normalize >>= Substitution(boundTo map (_.symbol), boundFrom map (CODE.REF(_)))
+        // patmatDebug("normalize: "+ normalize)
+
+        val okSubst = Substitution(unboundFrom, unboundTo map (normalize(_))) // it's important substitution does not duplicate trees here -- it helps to keep hash consing simple, anyway
+        pointsToBound ++= ((okSubst.from, okSubst.to).zipped filter { (f, t) => pointsToBound exists (sym => t.exists(_.symbol == sym)) })._1
+        // patmatDebug("pointsToBound: "+ pointsToBound)
+
+        accumSubst >>= okSubst
+        // patmatDebug("accumSubst: "+ accumSubst)
+      }
+
 
       // TODO: improve, e.g., for constants
       def sameValue(a: Tree, b: Tree): Boolean = (a eq b) || ((a, b) match {
@@ -1437,7 +1489,7 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL
       // hashconsing trees (modulo value-equality)
       def unique(t: Tree, tpOverride: Type = NoType): Tree =
         trees find (a => a.equalsStructure0(t)(sameValue)) match {
-          case Some(orig) => orig // println("unique: "+ (t eq orig, orig));
+          case Some(orig) => orig // patmatDebug("unique: "+ (t eq orig, orig));
           case _ =>
             trees += t
             if (tpOverride != NoType) t setType tpOverride
@@ -1454,7 +1506,7 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL
       // produce the unique tree used to refer to this binder
       // the type of the binder passed to the first invocation
       // determines the type of the tree that'll be returned for that binder as of then
-      def binderToUniqueTree(b: Symbol) =
+      final def binderToUniqueTree(b: Symbol) =
         unique(accumSubst(normalize(CODE.REF(b))), b.tpe)
 
       @inline def /\(conds: Iterable[Cond]) = if (conds.isEmpty) Top else conds.reduceLeft(AndCond(_, _))
@@ -1462,23 +1514,32 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL
 
       // note that the sequencing of operations is important: must visit in same order as match execution
       // binderToUniqueTree uses the type of the first symbol that was encountered as the type for all future binders
-      def treeMakerToCond(tm: TreeMaker): Cond = {
+      final protected def treeMakerToCond(tm: TreeMaker, condMaker: CondMaker): Cond = {
         updateSubstitution(tm.substitution)
+        condMaker(tm)(treeMakerToCond(_, condMaker))
+      }
+
+      final protected def treeMakerToCondNoSubst(tm: TreeMaker, condMaker: CondMaker): Cond =
+        condMaker(tm)(treeMakerToCondNoSubst(_, condMaker))
 
+      type CondMaker = TreeMaker => (TreeMaker => Cond) => Cond
+      final def makeCond(tm: TreeMaker)(recurse: TreeMaker => Cond): Cond = {
         tm match {
           case ttm@TypeTestTreeMaker(prevBinder, testedBinder, pt, _)   =>
             object condStrategy extends TypeTestTreeMaker.TypeTestCondStrategy {
               type Result                                           = Cond
               def and(a: Result, b: Result)                         = AndCond(a, b)
               def outerTest(testedBinder: Symbol, expectedTp: Type) = Top // TODO OuterEqCond(testedBinder, expectedType)
-              def typeTest(b: Symbol, pt: Type)                     = TypeCond(binderToUniqueTree(b), uniqueTp(pt))
+              def typeTest(b: Symbol, pt: Type) = { // a type test implies the tested path is non-null (null.isInstanceOf[T] is false for all T)
+                val p = binderToUniqueTree(b);                        AndCond(NonNullCond(p), TypeCond(p, uniqueTp(pt)))
+              }
               def nonNullTest(testedBinder: Symbol)                 = NonNullCond(binderToUniqueTree(testedBinder))
               def equalsTest(pat: Tree, testedBinder: Symbol)       = EqualityCond(binderToUniqueTree(testedBinder), unique(pat))
               def eqTest(pat: Tree, testedBinder: Symbol)           = EqualityCond(binderToUniqueTree(testedBinder), unique(pat)) // TODO: eq, not ==
             }
             ttm.renderCondition(condStrategy)
           case EqualityTestTreeMaker(prevBinder, patTree, _)        => EqualityCond(binderToUniqueTree(prevBinder), unique(patTree))
-          case AlternativesTreeMaker(_, altss, _)                   => \/(altss map (alts => /\(alts map treeMakerToCond)))
+          case AlternativesTreeMaker(_, altss, _)                   => \/(altss map (alts => /\(alts map recurse)))
           case ProductExtractorTreeMaker(testedBinder, None, subst) => NonNullCond(binderToUniqueTree(testedBinder))
           case ExtractorTreeMaker(_, _, _, _)
              | GuardTreeMaker(_)
@@ -1488,47 +1549,24 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL
         }
       }
 
-      private def updateSubstitution(subst: Substitution) = {
-        // find part of substitution that replaces bound symbols by new symbols, and reverse that part
-        // so that we don't introduce new aliases for existing symbols, thus keeping the set of bound symbols minimal
-        val (boundSubst, unboundSubst) = (subst.from zip subst.to) partition {case (f, t) =>
-            t.isInstanceOf[Ident] && (t.symbol ne NoSymbol) && pointsToBound(f)
-          }
-        val (boundFrom, boundTo) = boundSubst.unzip
-        val (unboundFrom, unboundTo) = unboundSubst.unzip
-
-        // reverse substitution that would otherwise replace a variable we already encountered by a new variable
-        // NOTE: this forgets the more precise we have for these later variables, but that's probably okay
-        normalize >>= Substitution(boundTo map (_.symbol), boundFrom map (CODE.REF(_)))
-        // println("normalize: "+ normalize)
+      final def approximateMatch(cases: List[List[TreeMaker]], condMaker: CondMaker = makeCond): List[List[Test]] = cases.map { _ map (tm => Test(treeMakerToCond(tm, condMaker), tm)) }
 
-        val okSubst = Substitution(unboundFrom, unboundTo map (normalize(_))) // it's important substitution does not duplicate trees here -- it helps to keep hash consing simple, anyway
-        pointsToBound ++= ((okSubst.from, okSubst.to).zipped filter { (f, t) => pointsToBound exists (sym => t.exists(_.symbol == sym)) })._1
-        // println("pointsToBound: "+ pointsToBound)
-
-        accumSubst >>= okSubst
-        // println("accumSubst: "+ accumSubst)
-      }
-
-      def approximateTreeMaker(tm: TreeMaker): Test =
-        Test(treeMakerToCond(tm), tm)
-
-      def approximateMatch: List[List[Test]] = cases.map { _ map approximateTreeMaker }
+      final def approximateMatchAgain(cases: List[List[TreeMaker]], condMaker: CondMaker = makeCond): List[List[Test]] = cases.map { _ map (tm => Test(treeMakerToCondNoSubst(tm, condMaker), tm)) }
     }
 
     def approximateMatch(root: Symbol, cases: List[List[TreeMaker]]): List[List[Test]] = {
-      object approximator extends TreeMakersToConds(root, cases)
-      approximator.approximateMatch
+      object approximator extends TreeMakersToConds(root)
+      approximator.approximateMatch(cases)
     }
 
     def showTreeMakers(cases: List[List[TreeMaker]]) = {
-      println("treeMakers:")
-      println(alignAcrossRows(cases, ">>"))
+      patmatDebug("treeMakers:")
+      patmatDebug(alignAcrossRows(cases, ">>"))
     }
 
     def showTests(testss: List[List[Test]]) = {
-      println("tests: ")
-      println(alignAcrossRows(testss, "&"))
+      patmatDebug("tests: ")
+      patmatDebug(alignAcrossRows(testss, "&"))
     }
   }
 
@@ -1563,18 +1601,33 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL
     class Prop
     case class Eq(p: Var, q: Const) extends Prop
 
-    type Const
+    type Const <: AbsConst
+
+    trait AbsConst {
+      def implies(other: Const): Boolean
+      def excludes(other: Const): Boolean
+    }
+
     type Var <: AbsVar
 
     trait AbsVar {
-      // if the domain is enumerable, at least one assignment must be true
-      def domainEnumerable: Boolean
-      def domain: Option[Set[Const]]
+      // indicate we may later require a prop for V = C
+      def registerEquality(c: Const): Unit
+
+      // indicates null is part of the domain
+      def considerNull: Unit
+
+      // compute the domain and return it (call considerNull first!)
+      def domainSyms: Option[Set[Sym]]
 
       // for this var, call it V, turn V = C into the equivalent proposition in boolean logic
+      // registerEquality(c) must have been called prior to this call
+      // in fact, all equalities relevant to this variable must have been registered
       def propForEqualsTo(c: Const): Prop
 
-      def equalitySyms: Set[Sym]
+      // populated by registerEquality
+      // once equalitySyms has been called, must not call registerEquality anymore
+      def equalitySyms: List[Sym]
     }
 
     // would be nice to statically check whether a prop is equational or pure,
@@ -1586,12 +1639,17 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL
     case object True extends Prop
     case object False extends Prop
 
-    private def nextSymId = {_symId += 1; _symId}; private var _symId = 0
-
     // symbols are propositions
     case class Sym(val variable: Var, val const: Const) extends Prop {
-      override val toString = variable +"="+ const +"#"+ nextSymId
+      private[this] val id = nextSymId
+      override def toString = variable +"="+ const +"#"+ id
     }
+    private def nextSymId = {_symId += 1; _symId}; private var _symId = 0
+
+
+    @inline def /\(props: Iterable[Prop]) = if (props.isEmpty) True else props.reduceLeft(And(_, _))
+    @inline def \/(props: Iterable[Prop]) = if (props.isEmpty) False else props.reduceLeft(Or(_, _))
+
 
     trait PropTraverser {
       def apply(x: Prop): Unit = x match {
@@ -1605,6 +1663,14 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL
       def applyConst(x: Const): Unit = {}
     }
 
+    def gatherVariables(p: Prop): Set[Var] = {
+      val vars = new HashSet[Var]()
+      (new PropTraverser {
+        override def applyVar(v: Var) = vars += v
+      })(p)
+      vars.toSet
+    }
+
     trait PropMap {
       def apply(x: Prop): Prop = x match { // TODO: mapConserve
         case And(a, b) => And(apply(a), apply(b))
@@ -1614,287 +1680,670 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL
       }
     }
 
-    // plan: (aka TODO)
+    // convert finite domain propositional logic with subtyping to pure boolean propositional logic
+    // a type test or a value equality test are modelled as a variable being equal to some constant
+    // a variable V may be assigned multiple constants, as long as they do not contradict each other
+    // according to subtyping, e.g., V = ConstantType(1) and V = Int are valid assignments
+    // we rewrite V = C to a fresh boolean symbol, and model what we know about the variable's domain
+    // in a prelude (the equality axioms)
+    //   1. a variable with a closed domain (of a sealed type) must be assigned one of the instantiatable types in its domain
+    //   2. for each variable V in props, and each constant C it is compared to,
+    //      compute which assignments imply each other (as in the example above: V = 1 implies V = Int)
+    //      and which assignments are mutually exclusive (V = String implies -(V = Int))
+    //
+    // note that this is a conservative approximation: V = Constant(A) and V = Constant(B)
+    // are considered mutually exclusive (and thus both cases are considered reachable in {case A => case B =>}),
+    // even though A may be equal to B   (and thus the second case is not "dynamically reachable")
+    //
+    // 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)
+    def removeVarEq(props: List[Prop], considerNull: Boolean = false): (Prop, List[Prop]) = {
+      val start = startTimer(patmatAnaVarEq)
 
-    // convert finite domain propositional logic to boolean propositional logic
-    // for all c in C, there is a corresponding (meta-indexed) proposition Qv(c) that represents V = c,
-    // the only property of equality that is encoded is that a variable can at most be equal to one of the c in C:
-    // thus, for each distinct c, c', c'',... in C, a clause `not (Qv(c) /\ (Qv(c') \/ ... \/ Qv(c'')))` is added
-    def removeVarEq(prop: Prop): Prop = {
       val vars = new collection.mutable.HashSet[Var]
 
-      object dropEquational extends PropMap {
+      object gatherEqualities extends PropTraverser {
+        override def apply(p: Prop) = p match {
+          case Eq(v, c) =>
+            vars += v
+            v.registerEquality(c)
+          case _ => super.apply(p)
+        }
+      }
+
+      object rewriteEqualsToProp extends PropMap {
         override def apply(p: Prop) = p match {
-          case Eq(v, c) => vars += v; v.propForEqualsTo(c)
+          case Eq(v, c) => v.propForEqualsTo(c)
           case _ => super.apply(p)
         }
       }
 
-      // dropEquational populates vars, and for each var in vars. var.equalitySyms
-      val pure = dropEquational(prop)
+      props foreach gatherEqualities.apply
+      if (considerNull) vars foreach (_.considerNull)
 
-      // X = C is translated to P_X=C
-      // X = C' is translated to P_X=C'
-      // need to enforce X cannot simultaneously equal C and C'
-      // thus, all equality syms are mutually exclusive
-      // X = A, B, C, D --> Not(And(A, B)) /\ Not(And(A, C)) /\ Not(And(A, D))
-      //                 /\ Not(And(B, C)) /\ Not(And(B, D))
-      //                 /\ Not(And(C, D))
-      // equivalently Or(Not(A), Not(B)) /\ Or(...)
+      val pure = props map rewriteEqualsToProp.apply
 
       var eqAxioms: Prop = True
-      def mutex(a: Sym)(b: Sym) =
-        eqAxioms = And(eqAxioms, Or(Not(a), Not(b)))
+      @inline def addAxiom(p: Prop) = eqAxioms = And(eqAxioms, p)
 
-      // at least one assignment from the domain must be true
-      def assigned(dom: Set[Sym]) =
-        eqAxioms = And(eqAxioms, dom.reduceLeft(Or))
+      case class ExcludedPair(a: Const, b: Const) {
+        override def equals(o: Any) = o match {
+          case ExcludedPair(aa, bb) => (a == aa && b == bb) || (a == bb && b == aa)
+          case _ => false
+        }
+        // make ExcludedPair(a, b).hashCode == ExcludedPair(b, a).hashCode
+        override def hashCode = a.hashCode ^ b.hashCode
+      }
 
-      // println("vars: "+ vars)
+      // patmatDebug("vars: "+ vars)
       vars.foreach { v =>
-        // is the domain enumerable? then create equality syms for all elements in the domain and
-        // assert at least one of them must be selected
-        // if v.domain.isEmpty, we must consider the domain to be infinite
-        v.domain foreach { dom =>
-          // get the Syms for the constants in the domain (making fresh ones for those not encountered in the formula)
-          val domProps = dom map {c => v.propForEqualsTo(c)}
-          val domSyms  = new collection.mutable.HashSet[Sym]()
-          object collectSyms extends PropTraverser {
-            override def apply(p: Prop) = p match {
-              case domSym: Sym => domSyms += domSym
-              case _ => super.apply(p)
-            }
+        val excludedPair = new collection.mutable.HashSet[ExcludedPair]
+
+        // if v.domainSyms.isEmpty, we must consider the domain to be infinite
+        // otherwise, since the domain fully partitions the type of the value,
+        // exactly one of the types (and whatever it implies, imposed separately) must be chosen
+        // consider X ::= A | B | C, and A => B
+        // coverage is formulated as: A \/ B \/ C and the implications are
+        v.domainSyms foreach { dsyms => addAxiom(\/(dsyms)) }
+
+        val syms = v.equalitySyms
+        // patmatDebug("eqSyms "+(v, syms))
+        syms foreach { sym =>
+          // if we've already excluded the pair at some point (-A \/ -B), then don't exclude the symmetric one (-B \/ -A)
+          // (nor the positive implications -B \/ A, or -A \/ B, which would entail the equality axioms falsifying the whole formula)
+          val todo = syms filterNot (b => (b.const == sym.const) || excludedPair(ExcludedPair(b.const, sym.const)))
+          val (excluded, notExcluded) = todo partition (b => sym.const.excludes(b.const))
+          val implied = notExcluded filter (b => sym.const.implies(b.const))
+          // patmatDebug("implications: "+ (sym.const, excluded, implied, syms))
+
+          // when this symbol is true, what must hold...
+          implied  foreach (impliedSym => addAxiom(Or(Not(sym), impliedSym)))
+
+          // ... and what must not?
+          excluded foreach {excludedSym =>
+            excludedPair += ExcludedPair(sym.const, excludedSym.const)
+            addAxiom(Or(Not(sym), Not(excludedSym)))
           }
-          domProps foreach collectSyms.apply
-
-          // TODO: an empty domain means involved type tests can never be true --> always non-exhaustive?
-          if (domSyms.nonEmpty) assigned(domSyms.toSet)
-        }
-
-        // recover mutual-exclusivity (a variable can never be assigned two different constants)
-        var syms = v.equalitySyms.toList
-        while (syms.nonEmpty) {
-          syms.tail.foreach(mutex(syms.head))
-          syms = syms.tail
         }
       }
 
-      // println("eqAxioms:\n"+ cnfString(conjunctiveNormalForm(negationNormalForm(eqAxioms))))
-      // println("pure:\n"+ cnfString(conjunctiveNormalForm(negationNormalForm(pure))))
+      // patmatDebug("eqAxioms:\n"+ cnfString(eqFreePropToSolvable(eqAxioms)))
+      // patmatDebug("pure:\n"+ cnfString(eqFreePropToSolvable(pure)))
+
+      stopTimer(patmatAnaVarEq, start)
 
-      And(eqAxioms, pure)
+      (eqAxioms, pure)
     }
 
-    // convert propositional logic formula to CNF
-    // http://www.dcs.warwick.ac.uk/people/academic/Ranko.Lazic/fsv/fsv6.pdf
-    def negationNormalForm(p: Prop): Prop = p match {
-      case And(a, b)      => And(negationNormalForm(a), negationNormalForm(b))
-      case Or(a, b)       => Or(negationNormalForm(a), negationNormalForm(b))
-      case Not(And(a, b)) => negationNormalForm(Or(Not(a), Not(b)))
-      case Not(Or(a, b))  => negationNormalForm(And(Not(a), Not(b)))
-      case Not(Not(p))    => negationNormalForm(p)
-      case Not(True)      => False
-      case Not(False)     => True
-      case True
-         | False
-         | (_ : Sym)
-         | Not(_ : Sym)   => p
+
+    type Formula
+    def andFormula(a: Formula, b: Formula): Formula
+
+    class CNFBudgetExceeded extends RuntimeException("CNF budget exceeded")
+
+    // may throw an CNFBudgetExceeded
+    def propToSolvable(p: Prop) = {
+      val (eqAxioms, pure :: Nil) = removeVarEq(List(p), considerNull = false)
+      eqFreePropToSolvable(And(eqAxioms, pure))
     }
 
+    def eqFreePropToSolvable(p: Prop): Formula
+    def cnfString(f: Formula): String
+
+    type Model = Map[Sym, Boolean]
+    val EmptyModel: Model
+    val NoModel: Model
+
+    def findModelFor(f: Formula): Model
+    def findAllModelsFor(f: Formula): List[Model]
+  }
+
+  trait CNF extends Logic {
     // CNF: a formula is a conjunction of clauses
-    type Formula = List[Clause] ; def formula(c: Clause*): Formula = c.toList
+    type Formula = Array[Clause]
+    def formula(c: Clause*): Formula = c.toArray
+    def andFormula(a: Formula, b: Formula): Formula = a ++ b
 
     // a clause is a disjunction of distinct literals
-    type Clause  = Set[Lit]     ; def clause(l: Lit*): Clause = l.toSet
+    type Clause = Set[Lit]
+    def clause(l: Lit*): Clause = l.toSet
+    @inline private def merge(a: Clause, b: Clause) = a ++ b
+
+    type Lit
+    def Lit(sym: Sym, pos: Boolean = true): Lit
+
+    // throws an CNFBudgetExceeded when the prop results in a CNF that's too big
+    def eqFreePropToSolvable(p: Prop): Formula = {
+      // TODO: for now, reusing the normalization from DPLL
+      def negationNormalForm(p: Prop): Prop = p match {
+        case And(a, b)      => And(negationNormalForm(a), negationNormalForm(b))
+        case Or(a, b)       => Or(negationNormalForm(a), negationNormalForm(b))
+        case Not(And(a, b)) => negationNormalForm(Or(Not(a), Not(b)))
+        case Not(Or(a, b))  => negationNormalForm(And(Not(a), Not(b)))
+        case Not(Not(p))    => negationNormalForm(p)
+        case Not(True)      => False
+        case Not(False)     => True
+        case True
+           | False
+           | (_ : Sym)
+           | Not(_ : Sym)   => p
+      }
+
+      val TrueF          = formula()
+      val FalseF         = formula(clause())
+      def lit(s: Sym)    = formula(clause(Lit(s)))
+      def negLit(s: Sym) = formula(clause(Lit(s, false)))
+
+      def conjunctiveNormalForm(p: Prop, budget: Int = 256): Formula = {
+        def distribute(a: Formula, b: Formula, budget: Int): Formula =
+          if (budget <= 0) throw new CNFBudgetExceeded
+          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)))
+            }
 
-    // a literal is a (possibly negated) variable
-    case class Lit(sym: Sym, pos: Boolean = true) {
-      override def toString = if (!pos) "-"+ sym.toString else sym.toString
-      def unary_- = Lit(sym, !pos)
+        if (budget <= 0) throw new CNFBudgetExceeded
+
+        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))
+        }
+      }
+
+      val start = startTimer(patmatCNF)
+      val res = conjunctiveNormalForm(negationNormalForm(p))
+      stopTimer(patmatCNF, start)
+      patmatCNFSizes(res.size) += 1
+
+//      patmatDebug("cnf for\n"+ p +"\nis:\n"+cnfString(res))
+      res
     }
 
-    val TrueF          = formula()
-    val FalseF         = formula(clause())
-    def lit(s: Sym)    = formula(clause(Lit(s)))
-    def negLit(s: Sym) = formula(clause(Lit(s, false)))
+  }
 
-    def conjunctiveNormalForm(p: Prop): Formula = {
-      def distribute(a: Formula, b: Formula): Formula = (a, b) match {
-        // true \/ _ = true
-        case (TrueF, _) => TrueF
-        // _ \/ true = true
-        case (_, TrueF) => TrueF
-        // lit \/ lit
-        case (List(a), List(b)) => formula(a ++ b)
-        // (c1 /\ ... /\ cn) \/ d = ((c1 \/ d) /\ ... /\ (cn \/ d))
-        case (cs, d) if cs.tail nonEmpty => cs flatMap (c => distribute(formula(c), d))
-        // d \/ (c1 /\ ... /\ cn) = ((d \/ c1) /\ ... /\ (d \/ cn))
-        case (d, cs) if cs.tail nonEmpty => cs flatMap (c => distribute(d, formula(c)))
+  trait DPLLSolver 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 == sym) && (o.pos == pos)
+        case _ => false
       }
+      override def hashCode = sym.hashCode + pos.hashCode
 
-      p match {
-        case True        => TrueF
-        case False       => FalseF
-        case s: Sym      => lit(s)
-        case Not(s: Sym) => negLit(s)
-        case And(a, b)   => conjunctiveNormalForm(a) ++ conjunctiveNormalForm(b)
-        case Or(a, b)    => distribute(conjunctiveNormalForm(a), conjunctiveNormalForm(b))
-      }
+      def unary_- = Lit(sym, !pos)
     }
 
-    def normalize(p: Prop) = conjunctiveNormalForm(negationNormalForm(removeVarEq(p)))
     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)
-    type Model = Map[Sym, Boolean]
     val EmptyModel = Map.empty[Sym, Boolean]
+    val NoModel: Model = null
 
     // returns all solutions, if any (TODO: better infinite recursion backstop -- detect fixpoint??)
-    def fullDPLL(f: Formula): List[Model] = {
+    def findAllModelsFor(f: Formula): List[Model] = {
+      val vars: Set[Sym] = f.flatMap(_ collect {case l: Lit => l.sym}).toSet
+      // patmatDebug("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) } : _*)
 
-      def findAllModels(f: Formula, models: List[Model], recursionDepthAllowed: Int = 20): List[Model]=
+      def findAllModels(f: Formula, models: List[Model], recursionDepthAllowed: Int = 10): List[Model]=
         if (recursionDepthAllowed == 0) models
         else {
-          val (ok, model) = DPLL(f)
+          // patmatDebug("solving\n"+ cnfString(f))
+          val model = findModelFor(f)
           // if we found a solution, conjunct the formula with the model's negation and recurse
-          if (ok) findAllModels(f :+ negateModel(model), model :: models, recursionDepthAllowed - 1)
+          if (model ne NoModel) {
+            val unassigned = (vars -- model.keySet).toList
+            // patmatDebug("unassigned "+ unassigned +" in "+ model)
+            def force(lit: Lit) = {
+              val model = withLit(findModelFor(dropUnit(f, lit)), lit)
+              if (model ne NoModel) List(model)
+              else Nil
+            }
+            val forced = unassigned flatMap { s =>
+              force(Lit(s, true)) ++ force(Lit(s, false))
+            }
+            // patmatDebug("forced "+ forced)
+            val negated = negateModel(model)
+            findAllModels(f :+ negated, model :: (forced ++ models), recursionDepthAllowed - 1)
+          }
           else models
         }
 
       findAllModels(f, Nil)
     }
 
-    def DPLL(f: Formula): (Boolean, Model) = {
-      @inline def withLit(res: (Boolean, Model), l: Lit) = (res._1, res._2 + (l.sym -> l.pos))
-      @inline def orElse(a: (Boolean, Model), b: => (Boolean, Model)) = if (a._1) a else b
-
-//      println("dpll\n"+ cnfString(f))
-
-      if (f isEmpty) (true, EmptyModel)
-      else if(f exists (_.isEmpty)) (false, EmptyModel)
-      else f.find(_.size == 1) map { unitClause =>
-        val unitLit = unitClause.head
-//        println("unit: "+ unitLit)
-        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 simplified = f.filterNot(_.contains(unitLit)).map(_ - negated)
-        withLit(DPLL(simplified), unitLit)
-      } getOrElse {
-        // partition symbols according to whether they appear in positive and/or negative literals
-        val pos = new HashSet[Sym]()
-        val neg = new HashSet[Sym]()
-        f.foreach{_.foreach{ lit =>
-          if (lit.pos) pos += lit.sym else neg += lit.sym
-        }}
-        // appearing in both positive and negative
-        val impures = pos intersect neg
-        // appearing only in either positive/negative positions
-        val pures = (pos ++ neg) -- impures
-
-        if (pures nonEmpty) {
-          val pureSym = 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))
-//          println("pure: "+ pureLit +" pures: "+ pures +" impures: "+ impures)
-          val simplified = f.filterNot(_.contains(pureLit))
-          withLit(DPLL(simplified), pureLit)
-        } else {
-          val split = f.head.head
-//          println("split: "+ split)
-          orElse(DPLL(f :+ clause(split)), DPLL(f :+ clause(-split)))
+    @inline private def withLit(res: Model, l: Lit): Model = if (res eq NoModel) NoModel else res + (l.sym -> l.pos)
+    @inline private def dropUnit(f: Formula, unitLit: Lit) = {
+      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)
+      f.filterNot(_.contains(unitLit)).map(_ - negated)
+    }
+
+    def findModelFor(f: Formula): Model = {
+      @inline def orElse(a: Model, b: => Model) = if (a ne NoModel) a else b
+
+      // patmatDebug("dpll\n"+ cnfString(f))
+
+      val start = startTimer(patmatAnaDPLL)
+
+      val satisfiableWithModel: Model =
+        if (f isEmpty) EmptyModel
+        else if(f exists (_.isEmpty)) NoModel
+        else f.find(_.size == 1) match {
+          case Some(unitClause) =>
+            val unitLit = unitClause.head
+            // patmatDebug("unit: "+ unitLit)
+            withLit(findModelFor(dropUnit(f, unitLit)), unitLit)
+          case _ =>
+            // partition symbols according to whether they appear in positive and/or negative literals
+            val pos = new HashSet[Sym]()
+            val neg = new HashSet[Sym]()
+            f.foreach{_.foreach{ lit =>
+              if (lit.pos) pos += lit.sym else neg += lit.sym
+            }}
+            // appearing in both positive and negative
+            val impures = pos intersect neg
+            // appearing only in either positive/negative positions
+            val pures = (pos ++ neg) -- impures
+
+            if (pures nonEmpty) {
+              val pureSym = 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))
+              // patmatDebug("pure: "+ pureLit +" pures: "+ pures +" impures: "+ impures)
+              val simplified = f.filterNot(_.contains(pureLit))
+              withLit(findModelFor(simplified), pureLit)
+            } else {
+              val split = f.head.head
+              // patmatDebug("split: "+ split)
+              orElse(findModelFor(f :+ clause(split)), findModelFor(f :+ clause(-split)))
+            }
         }
-      }
+
+        stopTimer(patmatAnaDPLL, start)
+
+        satisfiableWithModel
     }
   }
 
+
   /**
    * Represent a match as a formula in propositional logic that encodes whether the match matches (abstractly: we only consider types)
    *
    */
   trait SymbolicMatchAnalysis extends TreeMakerApproximation with Logic { self: CodegenCore =>
+    def prepareNewAnalysis() = { Var.resetUniques(); Const.resetUniques() }
+
     object Var {
       private var _nextId = 0
       def nextId = {_nextId += 1; _nextId}
 
+      def resetUniques() = {_nextId = 0; uniques.clear()}
       private val uniques = new collection.mutable.HashMap[Tree, Var]
       def apply(x: Tree): Var = uniques getOrElseUpdate(x, new Var(x, x.tpe))
     }
     class Var(val path: Tree, fullTp: Type, checked: Boolean = true) extends AbsVar {
+      private[this] val id: Int = Var.nextId
+
+      // private[this] var canModify: Option[Array[StackTraceElement]] = None
+      @inline private[this] def ensureCanModify = {} //if (canModify.nonEmpty) patmatDebug("BUG!"+ this +" modified after having been observed: "+ canModify.get.mkString("\n"))
+
+      @inline private[this] def observed = {} //canModify = Some(Thread.currentThread.getStackTrace)
+
+      // don't access until all potential equalities have been registered using registerEquality
+      private[this] val symForEqualsTo = new collection.mutable.HashMap[Const, Sym]
+
       // when looking at the domain, we only care about types we can check at run time
       val domainTp: Type = checkableType(fullTp)
 
+      private[this] var _considerNull = false
+      def considerNull: Unit = { ensureCanModify; if (NullTp <:< domainTp) _considerNull = true }
+
       // case None => domain is unknown,
       // case Some(List(tps: _*)) => domain is exactly tps
       // we enumerate the subtypes of the full type, as that allows us to filter out more types statically,
       // once we go to run-time checks (on Const's), convert them to checkable types
       // TODO: there seems to be bug for singleton domains (variable does not show up in model)
-      val domain = if (checked) enumerateSubtypes(fullTp).map(_.map(Const).toSet) else None
-
-      def describe = toString + ": "+ fullTp + domain.map(_.map(_.tp).mkString(" ::= ", " | ", "")).getOrElse(" ::= ??") +" // = "+ path
-      def domainEnumerable = domain.nonEmpty
+      lazy val domain: Option[Set[Const]] =
+        if (!checked) None
+        else {
+          val subConsts = enumerateSubtypes(fullTp).map{ tps =>
+            tps.toSet[Type].map{ tp =>
+              val domainC = TypeConst(tp)
+              registerEquality(domainC)
+              domainC
+            }
+          }
 
-      private val domMap = new collection.mutable.HashMap[Const, Sym]
-      private def symForEqualsTo(c: Const) = {
-        domMap getOrElseUpdate(c, {
-            // println("creating symbol for equality "+ this +" = "+ c)
-            Sym(this, c)
-          })
-      }
+          val allConsts =
+            if (! _considerNull) subConsts
+            else {
+              registerEquality(NullConst)
+              subConsts map (_ + NullConst)
+            }
 
-      // for this var, call it V, turn V = C into the equivalent proposition in boolean logic
-      // over all executions of this method on the same Var object,
-      def propForEqualsTo(c: Const): Prop = {
-        domain match {
-          case None => symForEqualsTo(c)
-          case Some(domainConsts) =>
-            val domainTps = domainConsts map (_.tp)
-            val checkedTp = c.tp
-            // find all the domain types that could make the type test true
-            // if the checked type is a supertype of the lub of the domain,
-            // we'll end up \/'ing the whole domain together,
-            // but must not simplify to True, as the type test may also fail...
-            val matches = domainTps.filter(_ <:< checkedTp).map{ tp => symForEqualsTo(Const(tp)) }
-            // println("type-equals-prop for "+ this +" = "+ c +": "+ (checkedTp, domainTp, domainTps) +" matches: "+ matches)
-
-            if (matches isEmpty) False else matches.reduceLeft(Or)
+          observed; allConsts
         }
-      }
 
-      def equalitySyms: Set[Sym] = domMap.values.toSet
+      // accessing after calling considerNull will result in inconsistencies
+      lazy val domainSyms: Option[Set[Sym]] = domain map { _ map symForEqualsTo }
 
-      private[this] val id: Int = Var.nextId
+
+      // populate equalitySyms
+      // don't care about the result, but want only one fresh symbol per distinct constant c
+      def registerEquality(c: Const): Unit = {ensureCanModify; symForEqualsTo getOrElseUpdate(c, Sym(this, c))}
+
+      // don't access until all potential equalities have been registered using registerEquality
+      lazy val equalitySyms = {observed; symForEqualsTo.values.toList}
+
+      // return the symbol that represents this variable being equal to the constant `c`, if it exists, otherwise False (for robustness)
+      // (registerEquality(c) must have been called prior, either when constructing the domain or from outside)
+      def propForEqualsTo(c: Const): Prop = {observed; symForEqualsTo.getOrElse(c, False)}
+
+
+      // don't call until all equalities have been registered and considerNull has been called (if needed)
+      def describe = toString + ": " + fullTp + domain.map(_.mkString(" ::= ", " | ", "// "+ symForEqualsTo.keys)).getOrElse(symForEqualsTo.keys.mkString(" ::= ", " | ", " | ...")) + " // = " + path
       override def toString = "V"+ id
     }
 
+
     // all our variables range over types
     // a literal constant becomes ConstantType(Constant(v)) when the type allows it (roughly, anyval + string + null)
     // equality between variables: SingleType(x) (note that pattern variables cannot relate to each other -- it's always patternVar == nonPatternVar)
-    case class Const(tp: Type) {
-      override def toString = tp.toString
+    object Const {
+      def resetUniques() = {_nextTypeId = 0; _nextValueId = 0; uniques.clear()} // patmatDebug("RESET")
+
+      private var _nextTypeId = 0
+      def nextTypeId = {_nextTypeId += 1; _nextTypeId}
+
+      private var _nextValueId = 0
+      def nextValueId = {_nextValueId += 1; _nextValueId}
+
+      private val uniques = new collection.mutable.HashMap[Type, Const]
+      private[SymbolicMatchAnalysis] def unique(tp: Type, mkFresh: => Const): Const =
+        uniques.get(tp).getOrElse(
+          uniques.find {case (oldTp, oldC) => oldTp =:= tp} match {
+            case Some((_, c)) => c
+            case _ =>
+              val fresh = mkFresh
+              uniques(tp) = fresh
+              fresh
+          })
+    }
 
-      def toValueString = tp match {
-        case ConstantType(c) => c.escapedStringValue
-        case _ => tp.toString
+    sealed abstract class Const extends AbsConst {
+      protected def tp: Type
+      protected def wideTp: Type
+
+      def isAny = wideTp.typeSymbol == AnyClass
+
+      final def implies(other: Const): Boolean = {
+        val r = (this, other) match {
+          case (_: ValueConst, _: ValueConst) => this == other // hashconsed
+          case (_: ValueConst, _: TypeConst)  => tp <:< other.tp
+          case (_: TypeConst,  _)             => tp <:< other.tp
+          case _                              => false
+        }
+        // if(r) patmatDebug("implies    : "+(this, other))
+        // else  patmatDebug("NOT implies: "+(this, other))
+        r
+      }
+
+      // does V = C preclude V having value `other`?  V = null is an exclusive assignment,
+      // but V = 1 does not preclude V = Int, or V = Any
+      final def excludes(other: Const): Boolean = {
+        val r = (this, other) match {
+          case (_, NullConst)                 => true
+          case (NullConst, _)                 => true
+          // this causes false negative for unreachability, but that's ok:
+          // example: val X = 1; val Y = 1; (2: Int) match { case X => case Y => /* considered reachable */ }
+          case (_: ValueConst, _: ValueConst) => this != other
+          case (_: ValueConst, _: TypeConst)  => !((tp <:< other.tp) || (other.tp <:< wideTp))
+          case (_: TypeConst,  _: ValueConst) => !((other.tp <:< tp) || (tp <:< other.wideTp))
+          case (_: TypeConst,  _: TypeConst)  => !((tp <:< other.tp) || (other.tp <:< tp))
+          case _                              => false
+        }
+        // if(r) patmatDebug("excludes    : "+(this, other))
+        // else  patmatDebug("NOT excludes: "+(this, other))
+        r
       }
+
+      // note: use reference equality on Const since they're hash-consed (doing type equality all the time is too expensive)
+      // the equals inherited from AnyRef does just this
+    }
+
+
+    object TypeConst {
+      def apply(tp: Type) = {
+        if (tp =:= NullTp) NullConst
+        else if (tp.isInstanceOf[SingletonType]) ValueConst.fromType(tp)
+        else Const.unique(tp, new TypeConst(tp))
+      }
+      def unapply(c: TypeConst): Some[Type] = Some(c.tp)
+    }
+
+    // corresponds to a type test that does not imply any value-equality (well, except for outer checks, which we don't model yet)
+    sealed class TypeConst(val tp: Type) extends Const {
+      assert(!(tp =:= NullTp))
+      private[this] val id: Int = Const.nextTypeId
+
+      val wideTp = tp.widen
+
+      override def toString = tp.toString //+"#"+ id
+    }
+
+    // p is a unique type or a constant value
+    object ValueConst {
+      def fromType(tp: Type) = {
+        assert(tp.isInstanceOf[SingletonType])
+        val toString = tp match {
+          case ConstantType(c) => c.escapedStringValue
+          case _ => tp.toString
+        }
+        Const.unique(tp, new ValueConst(tp, tp.widen, toString))
+      }
+      def apply(p: Tree) = {
+        val tp = p.tpe.normalize
+        if (tp =:= NullTp) NullConst
+        else {
+          val wideTp = {
+            if (p.hasSymbol && p.symbol.isStable) tp.asSeenFrom(tp.prefix, p.symbol.owner).widen
+            else tp.widen
+          }
+
+          val narrowTp =
+            if (tp.isInstanceOf[SingletonType]) tp
+            else p match {
+              case Literal(c) =>
+                if (c.tpe.typeSymbol == UnitClass) c.tpe
+                else ConstantType(c)
+              case p if p.symbol.isStable =>
+                singleType(tp.prefix, p.symbol)
+              case x =>
+                // TODO: better type
+                x.tpe.narrow
+            }
+
+          val toString =
+            if (p.hasSymbol && p.symbol.isStable) p.symbol.name.toString // tp.toString
+            else p.toString //+"#"+ id
+
+          Const.unique(narrowTp, new ValueConst(narrowTp, checkableType(wideTp), toString)) // must make wide type checkable so that it is comparable to types from TypeConst
+        }
+      }
+    }
+    sealed class ValueConst(val tp: Type, val wideTp: Type, override val toString: String) extends Const {
+      // patmatDebug("VC"+(tp, wideTp, toString))
+      assert(!(tp =:= NullTp))
+      private[this] val id: Int = Const.nextValueId
+    }
+
+    lazy val NullTp = ConstantType(Constant(null))
+    case object NullConst extends Const {
+      protected def tp     = NullTp
+      protected def wideTp = NullTp
+
+      def isValue = true
+      override def toString = "null"
+    }
+
+
+    // turns a case (represented as a list of abstract tests)
+    // into a proposition that is satisfiable if the case may match
+    def symbolicCase(tests: List[Test], modelNull: Boolean = false): Prop = {
+      def symbolic(t: Cond): Prop = t match {
+        case AndCond(a, b) => And(symbolic(a), symbolic(b))
+        case OrCond(a, b) => Or(symbolic(a), symbolic(b))
+        case Top => True
+        case Havoc => False
+        case TypeCond(p, pt) => Eq(Var(p), TypeConst(checkableType(pt)))
+        case EqualityCond(p, q) => Eq(Var(p), ValueConst(q))
+        case NonNullCond(p) => if (!modelNull) True else Not(Eq(Var(p), NullConst))
+      }
+
+      val testsBeforeBody = tests.takeWhile(t => !t.treeMaker.isInstanceOf[BodyTreeMaker])
+      /\(testsBeforeBody.map(t => symbolic(t.cond)))
     }
 
+    // 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
+    // right now hackily implement this by pruning counter-examples
+    // unreachability would also benefit from a more faithful representation
+
+    // reachability (dead code)
+
+    // computes the first 0-based case index that is unreachable (if any)
+    // a case is unreachable if it implies its preceding cases
+    // call C the formula that is satisfiable if the considered case matches
+    // call P the formula that is satisfiable if the cases preceding it match
+    // the case is reachable if there is a model for -P /\ C,
+    // thus, the case is unreachable if there is no model for -(-P /\ C),
+    // or, equivalently, P \/ -C, or C => P
+    def unreachableCase(prevBinder: Symbol, cases: List[List[TreeMaker]], pt: Type): Option[Int] = {
+      // customize TreeMakersToConds (which turns a tree of tree makers into a more abstract DAG of tests)
+      // when approximating the current case (which we hope is reachable), be optimistic about the unknowns
+      object reachabilityApproximation extends TreeMakersToConds(prevBinder) {
+        def makeCondOptimistic(tm: TreeMaker)(recurse: TreeMaker => Cond): Cond = tm match {
+          // for unreachability, let's assume a guard always matches (unless we statically determined otherwise)
+          // otherwise, a guarded case would be considered unreachable
+          case GuardTreeMaker(guard) =>
+            guard.tpe match {
+              case ConstantType(Constant(false)) => Havoc // not the best name; however, symbolically, 'Havoc' becomes 'False'
+              case _ => Top
+            }
+          // similar to a guard, user-defined extractors should not cause us to freak out
+          // if we're not 100% sure it does not match (i.e., its result type is None or Constant(false) -- TODO),
+          // let's stay optimistic and assume it does
+          case ExtractorTreeMaker(_, _, _, _)
+             | ProductExtractorTreeMaker(_, Some(_), _)  => Top
+          // TODO: consider length-checks
+          case _ =>
+            makeCond(tm)(recurse)
+        }
+
+        // be pessimistic when approximating the prefix of the current case
+        // we hope the prefix fails so that we might get to the current case, which we hope is not dead
+        def makeCondPessimistic(tm: TreeMaker)(recurse: TreeMaker => Cond): Cond = makeCond(tm)(recurse)
+      }
+
+      val start = startTimer(patmatAnaReach)
+
+      // use the same approximator so we share variables,
+      // but need different conditions depending on whether we're conservatively looking for failure or success
+      val testCasesOk   = reachabilityApproximation.approximateMatch(cases, reachabilityApproximation.makeCondOptimistic)
+      val testCasesFail = reachabilityApproximation.approximateMatchAgain(cases, reachabilityApproximation.makeCondPessimistic)
+
+      reachabilityApproximation.discard()
+      prepareNewAnalysis()
+
+      val propsCasesOk   = testCasesOk   map (t => symbolicCase(t, modelNull = true))
+      val propsCasesFail = testCasesFail map (t => Not(symbolicCase(t, modelNull = true)))
+      val (eqAxiomsFail, symbolicCasesFail) = removeVarEq(propsCasesFail, considerNull = true)
+      val (eqAxiomsOk, symbolicCasesOk)     = removeVarEq(propsCasesOk,   considerNull = true)
+
+      try {
+        // most of the time eqAxiomsFail == eqAxiomsOk, but the different approximations might cause different variables to disapper in general
+        val eqAxiomsCNF =
+          if (eqAxiomsFail == eqAxiomsOk) eqFreePropToSolvable(eqAxiomsFail)
+          else eqFreePropToSolvable(And(eqAxiomsFail, eqAxiomsOk))
+
+        var prefix     = eqAxiomsCNF
+        var prefixRest = symbolicCasesFail
+        var current    = symbolicCasesOk
+        var reachable  = true
+        var caseIndex  = 0
+
+  //      patmatDebug("reachability, vars:\n"+ ((propsCasesFail flatMap gatherVariables) map (_.describe) mkString ("\n")))
+  //      patmatDebug("equality axioms:\n"+ cnfString(eqAxiomsCNF))
+
+        // 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 = andFormula(eqFreePropToSolvable(prefHead), prefix)
+            current = current.tail
+            val model = findModelFor(andFormula(eqFreePropToSolvable(current.head), prefix))
+
+  //          patmatDebug("trying to reach:\n"+ cnfString(current.head) +"\nunder prefix:\n"+ cnfString(prefix))
+  //          if (ok) patmatDebug("reached: "+ modelString(model))
+
+            reachable = model ne NoModel
+          }
+        }
+
+        stopTimer(patmatAnaReach, start)
+
+        if (reachable) None else Some(caseIndex)
+      } catch {
+        case e : CNFBudgetExceeded =>
+//          debugWarn(util.Position.formatMessage(prevBinder.pos, "Cannot check match for reachability", false))
+//          e.printStackTrace()
+          None // CNF budget exceeded
+      }
+    }
+
+    // exhaustivity
+
     // make sure it's not a primitive, else (5: Byte) match { case 5 => ... } sees no Byte
     // TODO: domain of feasibly enumerable built-in types (enums, char?)
     def enumerateSubtypes(tp: Type): Option[List[Type]] =
       tp.typeSymbol match {
         case BooleanClass =>
-          // println("enum bool "+ tp)
+          // patmatDebug("enum bool "+ tp)
           Some(List(ConstantType(Constant(true)), ConstantType(Constant(false))))
         // TODO case _ if tp.isTupleType => // recurse into component types
         case sym if !sym.isSealed || isPrimitiveValueClass(sym) =>
-          // println("enum unsealed "+ (tp, sym, sym.isSealed, isPrimitiveValueClass(sym)))
+          // patmatDebug("enum unsealed "+ (tp, sym, sym.isSealed, isPrimitiveValueClass(sym)))
           None
         case sym =>
           val subclasses = (
@@ -1902,7 +2351,7 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL
             // symbols which are both sealed and abstract need not be covered themselves, because
             // all of their children must be and they cannot otherwise be created.
             filterNot (x => x.isSealed && x.isAbstractClass && !isPrimitiveValueClass(x)))
-          // println("subclasses "+ (sym, subclasses))
+          // patmatDebug("subclasses "+ (sym, subclasses))
 
           val tpApprox = typer.infer.approximateAbstracts(tp)
           val pre = tpApprox.prefix
@@ -1914,20 +2363,14 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL
               // however, must approximate abstract types in
               val subTp       = appliedType(pre.memberType(sym), sym.typeParams.map(_ => WildcardType))
               val subTpApprox = typer.infer.approximateAbstracts(subTp) // TODO: needed?
-              // println("subtp"+(subTpApprox <:< tpApprox, subTpApprox, tpApprox))
+              // patmatDebug("subtp"+(subTpApprox <:< tpApprox, subTpApprox, tpApprox))
               if (subTpApprox <:< tpApprox) Some(checkableType(subTp))
               else None
             })
-          // println("enum sealed "+ (tp, tpApprox) + " as "+ validSubTypes)
+          // patmatDebug("enum sealed "+ (tp, tpApprox) + " as "+ validSubTypes)
           Some(validSubTypes)
       }
 
-    def narrowTypeOf(p: Tree) = p match {
-      case Literal(c) => ConstantType(c)
-      case Ident(_) if p.symbol.isStable => singleType(p.tpe.prefix, p.symbol)
-      case x => x.tpe.narrow
-    }
-
     // approximate a type to the static type that is fully checkable at run time,
     // hiding statically known but dynamically uncheckable information using existential quantification
     // TODO: this is subject to the availability of TypeTags (since an abstract type with a type tag is checkable at run time)
@@ -1944,7 +2387,7 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL
         }
       }
       val res = toCheckable(tp)
-      // println("checkable "+(tp, res))
+      // patmatDebug("checkable "+(tp, res))
       res
     }
 
@@ -1955,7 +2398,7 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL
       val checkable = (
            (isTupleType(tp) && tupleComponents(tp).exists(tp => !uncheckableType(tp)))
         || enumerateSubtypes(tp).nonEmpty)
-      // if (!checkable) println("deemed uncheckable: "+ tp)
+      // if (!checkable) patmatDebug("deemed uncheckable: "+ tp)
       !checkable
     }
 
@@ -1966,10 +2409,11 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL
       // - back off (to avoid crying exhaustive too often) when:
       //    - there are guards -->
       //    - there are extractor calls (that we can't secretly/soundly) rewrite
+      val start = startTimer(patmatAnaExhaust)
       var backoff = false
-      object exhaustivityApproximation extends TreeMakersToConds(prevBinder, cases) {
-        override def treeMakerToCond(tm: TreeMaker): Cond = tm match {
-          case p@ExtractorTreeMaker(extractor, Some(lenCheck), testedBinder, _) =>
+      object exhaustivityApproximation extends TreeMakersToConds(prevBinder) {
+        def makeCondExhaustivity(tm: TreeMaker)(recurse: TreeMaker => Cond): Cond = tm match {
+          case p @ ExtractorTreeMaker(extractor, Some(lenCheck), testedBinder, _) =>
             p.checkedLength match {
               // pattern: `List()`  (interpret as `Nil`)
               // TODO: make it more general List(1, 2) => 1 :: 2 :: Nil
@@ -1977,47 +2421,36 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL
                 EqualityCond(binderToUniqueTree(p.prevBinder), unique(Ident(NilModule) setType NilModule.tpe))
               case _ =>
                 backoff = true
-                super.treeMakerToCond(tm)
+                makeCond(tm)(recurse)
             }
           case ExtractorTreeMaker(_, _, _, _) =>
-//            println("backing off due to "+ tm)
+// patmatDebug("backing off due to "+ tm)
             backoff = true
-            super.treeMakerToCond(tm)
+            makeCond(tm)(recurse)
           case GuardTreeMaker(guard) =>
             guard.tpe match {
               case ConstantType(Constant(true)) => Top
               case ConstantType(Constant(false)) => Havoc
               case _ =>
-//                println("can't statically interpret guard: "+(guard, guard.tpe))
+// patmatDebug("can't statically interpret guard: "+(guard, guard.tpe))
                 backoff = true
                 Havoc
             }
           case _ =>
-            super.treeMakerToCond(tm)
+            makeCond(tm)(recurse)
         }
       }
 
-      def symbolic(t: Cond): Prop = t match {
-        case AndCond(a, b) => And(symbolic(a), symbolic(b))
-        case OrCond(a, b) => Or(symbolic(a), symbolic(b))
-        case Top => True
-        case Havoc => False
-        case TypeCond(p, pt) => Eq(Var(p), Const(checkableType(pt)))
-        case EqualityCond(p, q) => Eq(Var(p), Const(narrowTypeOf(q)))
-        case NonNullCond(p) => True // ignoring nullness because it generates too much noise Not(Eq(Var(p), Const(NullClass.tpe)))
-      }
+      val tests = exhaustivityApproximation.approximateMatch(cases, exhaustivityApproximation.makeCondExhaustivity)
 
-      def symbolicCase(tests: List[Test]) = {
-        val testsBeforeBody = tests.takeWhile(t => !t.treeMaker.isInstanceOf[BodyTreeMaker])
-        testsBeforeBody.map(t => symbolic(t.cond)).foldLeft(True: Prop)(And)
-      }
+      if (backoff) Nil else {
+        val prevBinderTree = exhaustivityApproximation.binderToUniqueTree(prevBinder)
 
-      val tests = exhaustivityApproximation.approximateMatch
+        exhaustivityApproximation.discard()
+        prepareNewAnalysis()
 
-      if (backoff) Nil else {
-        val symbolicCases = tests map symbolicCase
+        val symbolicCases = tests map (symbolicCase(_, modelNull = false))
 
-        val prevBinderTree = exhaustivityApproximation.binderToUniqueTree(prevBinder)
 
         // TODO: null tests generate too much noise, so disabled them -- is there any way to bring them back?
         // assuming we're matching on a non-null scrutinee (prevBinder), when does the match fail?
@@ -2030,33 +2463,35 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL
         // val matchFails = And(symbolic(nonNullScrutineeCond), Not(symbolicCases reduceLeft (Or(_, _))))
 
         // when does the match fail?
-        val matchFails = Not(symbolicCases reduceLeft (Or(_, _)))
-
+        val matchFails = Not(\/(symbolicCases))
 
   // debug output:
-        // println("analysing:")
+        // patmatDebug("analysing:")
         // showTreeMakers(cases)
         // showTests(tests)
         //
-        // def gatherVariables(p: Prop): Set[Var] = {
-        //   val vars = new HashSet[Var]()
-        //   (new PropTraverser {
-        //     override def applyVar(v: Var) = vars += v
-        //   })(p)
-        //   vars.toSet
-        // }
         // val vars = gatherVariables(matchFails)
-        // println("\nvars:\n"+ (vars map (_.describe) mkString ("\n")))
+        // patmatDebug("\nvars:\n"+ (vars map (_.describe) mkString ("\n")))
         //
-        // println("\nmatchFails as CNF:\n"+ cnfString(normalize(matchFails)))
+        // patmatDebug("\nmatchFails as CNF:\n"+ cnfString(propToSolvable(matchFails)))
+
+        try {
+          // find the models (under which the match fails)
+          val matchFailModels = findAllModelsFor(propToSolvable(matchFails))
 
-        // find the models (under which the match fails)
-        val matchFailModels = fullDPLL(normalize(matchFails))
+          val scrutVar = Var(prevBinderTree)
+          val counterExamples = matchFailModels.map(modelToCounterExample(scrutVar))
 
-        val scrutVar = Var(prevBinderTree)
-        val counterExamples = matchFailModels.map(modelToCounterExample(scrutVar))
+          val pruned = CounterExample.prune(counterExamples).map(_.toString).sorted
 
-        CounterExample.prune(counterExamples).map(_.toString).sorted
+          stopTimer(patmatAnaExhaust, start)
+          pruned
+        } catch {
+          case e : CNFBudgetExceeded =>
+            // patmatDebug(util.Position.formatMessage(prevBinder.pos, "Cannot check match for exhaustivity", false))
+            // e.printStackTrace()
+            Nil // CNF budget exceeded
+        }
       }
     }
 
@@ -2072,13 +2507,14 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL
       protected[SymbolicMatchAnalysis] def flattenConsArgs: List[CounterExample] = Nil
       def coveredBy(other: CounterExample): Boolean = this == other || other == WildcardExample
     }
-    case class ValueExample(c: Const) extends CounterExample { override def toString = c.toValueString }
+    case class ValueExample(c: ValueConst) extends CounterExample { override def toString = c.toString }
     case class TypeExample(c: Const)  extends CounterExample { override def toString = "(_ : "+ c +")" }
     case class NegativeExample(nonTrivialNonEqualTo: List[Const]) extends CounterExample {
+      // require(nonTrivialNonEqualTo.nonEmpty, nonTrivialNonEqualTo)
       override def toString = {
         val negation =
-          if (nonTrivialNonEqualTo.tail.isEmpty) nonTrivialNonEqualTo.head.toValueString
-          else nonTrivialNonEqualTo.map(_.toValueString).sorted.mkString("in (", ", ", ")")
+          if (nonTrivialNonEqualTo.tail.isEmpty) nonTrivialNonEqualTo.head.toString
+          else nonTrivialNonEqualTo.map(_.toString).sorted.mkString("in (", ", ", ")")
         "<not "+ negation +">"
       }
     }
@@ -2115,6 +2551,21 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL
     case object WildcardExample extends CounterExample { override def toString = "_" }
     case object NoExample extends CounterExample { override def toString = "??" }
 
+    @inline def modelToVarAssignment(model: Model): Map[Var, (Seq[Const], Seq[Const])] =
+      model.toSeq.groupBy{f => f match {case (sym, value) => sym.variable} }.mapValues{ xs =>
+        val (trues, falses) = xs.partition(_._2)
+        (trues map (_._1.const), falses map (_._1.const))
+        // should never be more than one value in trues...
+      }
+
+    def varAssignmentString(varAssignment: Map[Var, (Seq[Const], Seq[Const])]) =
+      varAssignment.toSeq.sortBy(_._1.toString).map { case (v, (trues, falses)) =>
+         val assignment = "== "+ (trues mkString("(", ", ", ")")) +"  != ("+ (falses mkString(", ")) +")"
+         v +"(="+ v.path +": "+ v.domainTp +") "+ assignment
+       }.mkString("\n")
+
+    def modelString(model: Model) = varAssignmentString(modelToVarAssignment(model))
+
     // return constructor call when the model is a true counter example
     // (the variables don't take into account type information derived from other variables,
     //  so, naively, you might try to construct a counter example like _ :: Nil(_ :: _, _ :: _),
@@ -2125,24 +2576,16 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL
       // x1.tl = ...
       // x1.hd.hd = ...
       // ...
-      val varAssignment = model.toSeq.groupBy{f => f match {case (sym, value) => sym.variable} }.mapValues{ xs =>
-        val (trues, falses) = xs.partition(_._2)
-        (trues map (_._1.const), falses map (_._1.const))
-        // should never be more than one value in trues...
-      }
-
-      // println("var assignment:\n"+
-      //   varAssignment.toSeq.sortBy(_._1.toString).map { case (v, (trues, falses)) =>
-      //     val assignment = "== "+ (trues mkString("(", ", ", ")")) +"  != ("+ (falses mkString(", ")) +")"
-      //     v +"(="+ v.path +": "+ v.domainTp +") "+ assignment
-      //   }.mkString("\n"))
+      val varAssignment = modelToVarAssignment(model)
 
+      // patmatDebug("var assignment for model "+ model +":\n"+ varAssignmentString(varAssignment))
 
       // chop a path into a list of symbols
       def chop(path: Tree): List[Symbol] = path match {
         case Ident(_) => List(path.symbol)
         case Select(pre, name) => chop(pre) :+ path.symbol
-        case _ => println("don't know how to chop "+ path); Nil
+        case _ => // patmatDebug("don't know how to chop "+ path)
+          Nil
       }
 
       // turn the variable assignments into a tree
@@ -2181,7 +2624,9 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL
 
       // node in the tree that describes how to construct a counter-example
       case class VariableAssignment(variable: Var, equalTo: List[Const], notEqualTo: List[Const], fields: collection.mutable.Map[Symbol, VariableAssignment]) {
-        private lazy val ctor       = (equalTo match { case List(Const(tp)) => tp case _ => variable.domainTp }).typeSymbol.primaryConstructor
+        // need to prune since the model now incorporates all super types of a constant (needed for reachability)
+        private lazy val prunedEqualTo = equalTo filterNot (subsumed => equalTo.exists(better => (better ne subsumed) && (better implies subsumed)))
+        private lazy val ctor       = (prunedEqualTo match { case List(TypeConst(tp)) => tp case _ => variable.domainTp }).typeSymbol.primaryConstructor
         private lazy val ctorParams = if (ctor == NoSymbol || ctor.paramss.isEmpty) Nil else ctor.paramss.head
         private lazy val cls        = if (ctor == NoSymbol) NoSymbol else ctor.owner
         private lazy val caseFieldAccs = if (cls == NoSymbol) Nil else cls.caseFieldAccessors
@@ -2190,7 +2635,7 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL
         def allFieldAssignmentsLegal: Boolean =
           (fields.keySet subsetOf caseFieldAccs.toSet) && fields.values.forall(_.allFieldAssignmentsLegal)
 
-        private lazy val nonTrivialNonEqualTo = notEqualTo.filterNot{c => val sym = c.tp.typeSymbol; sym == AnyClass } // sym == NullClass ||
+        private lazy val nonTrivialNonEqualTo = notEqualTo.filterNot{c => c.isAny }
 
         // NoExample if the constructor call is ill-typed
         // (thus statically impossible -- can we incorporate this into the formula?)
@@ -2198,17 +2643,17 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL
         def toCounterExample(beBrief: Boolean = false): CounterExample =
           if (!allFieldAssignmentsLegal) NoExample
           else {
-//            println("describing "+ (variable, equalTo, notEqualTo, fields, cls, allFieldAssignmentsLegal))
-            val res = equalTo match {
+            // patmatDebug("describing "+ (variable, equalTo, notEqualTo, fields, cls, allFieldAssignmentsLegal))
+            val res = prunedEqualTo match {
               // a definite assignment to a value
-              case List(eq@Const(_: ConstantType)) if fields.isEmpty => ValueExample(eq)
+              case List(eq: ValueConst) if fields.isEmpty => ValueExample(eq)
 
               // constructor call
               // or we did not gather any information about equality but we have information about the fields
               //  --> typical example is when the scrutinee is a tuple and all the cases first unwrap that tuple and only then test something interesting
               case _ if cls != NoSymbol &&
-                        (  equalTo.nonEmpty
-                        || (fields.nonEmpty && !isPrimitiveValueClass(cls) && equalTo.isEmpty && notEqualTo.isEmpty)) =>
+                        (  prunedEqualTo.nonEmpty
+                        || (fields.nonEmpty && !isPrimitiveValueClass(cls) && prunedEqualTo.isEmpty && notEqualTo.isEmpty)) =>
 
                 @inline def args(brevity: Boolean = beBrief) = {
                   // figure out the constructor arguments from the field assignment
@@ -2235,7 +2680,7 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL
               // TODO: improve reasoning -- in the mean time, a false negative is better than an annoying false positive
               case _ => NoExample
             }
-//            println("described as: "+ res)
+            // patmatDebug("described as: "+ res)
             res
           }
 
@@ -2255,11 +2700,9 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL
     /** a flow-sensitive, generalised, common sub-expression elimination
      * reuse knowledge from performed tests
      * the only sub-expressions we consider are the conditions and results of the three tests (type, type&equality, equality)
-     * when a sub-expression is share, it is stored in a mutable variable
+     * when a sub-expression is shared, it is stored in a mutable variable
      * the variable is floated up so that its scope includes all of the program that shares it
      * we generalize sharing to implication, where b reuses a if a => b and priors(a) => priors(b) (the priors of a sub expression form the path through the decision tree)
-     *
-     * intended to be generalised to exhaustivity/reachability checking
      */
     def doCSE(prevBinder: Symbol, cases: List[List[TreeMaker]], pt: Type): List[List[TreeMaker]] = {
       val testss = approximateMatch(prevBinder, cases)
@@ -2308,7 +2751,7 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL
         tested.clear()
         tests dropWhile storeDependencies
       }
-      // println("dependencies: "+ dependencies)
+      // patmatDebug("dependencies: "+ dependencies)
 
       // find longest prefix of tests that reuse a prior test, and whose dependent conditions monotonically increase
       // then, collapse these contiguous sequences of reusing tests
@@ -2342,7 +2785,7 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL
               case _ =>
             }
 
-            // println("sharedPrefix: "+ sharedPrefix)
+            // patmatDebug("sharedPrefix: "+ sharedPrefix)
             // if the shared prefix contains interesting conditions (!= Top)
             // and the last of such interesting shared conditions reuses another treemaker's test
             // replace the whole sharedPrefix by a ReusingCondTreeMaker
@@ -2358,7 +2801,7 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL
       // replace original treemakers that are reused (as determined when computing collapsed),
       // by ReusedCondTreeMakers
       val reusedMakers = collapsed mapConserve (_ mapConserve reusedOrOrig)
-//      println("after CSE:")
+// patmatDebug("after CSE:")
 //      showTreeMakers(reusedMakers)
       reusedMakers
     }
@@ -2366,7 +2809,7 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL
     object ReusedCondTreeMaker {
       def apply(orig: CondTreeMaker) = new ReusedCondTreeMaker(orig.prevBinder, orig.nextBinder, orig.cond, orig.res, orig.pos)
     }
-    class ReusedCondTreeMaker(prevBinder: Symbol, val nextBinder: Symbol, cond: Tree, res: Tree, pos: Position) extends TreeMaker { import CODE._
+    class ReusedCondTreeMaker(prevBinder: Symbol, val nextBinder: Symbol, cond: Tree, res: Tree, val pos: Position) extends TreeMaker { import CODE._
       lazy val localSubstitution        = Substitution(List(prevBinder), List(CODE.REF(nextBinder)))
       lazy val storedCond               = freshSym(pos, BooleanClass.tpe, "rc") setFlag MUTABLE
       lazy val treesToHoist: List[Tree] = {
@@ -2382,6 +2825,8 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL
     }
 
     case class ReusingCondTreeMaker(sharedPrefix: List[Test], toReused: TreeMaker => TreeMaker) extends TreeMaker { import CODE._
+      val pos = sharedPrefix.last.treeMaker.pos
+
       lazy val localSubstitution = {
         // replace binder of each dropped treemaker by corresponding binder bound by the most recent reused treemaker
         var mostRecentReusedMaker: ReusedCondTreeMaker = null
@@ -2471,7 +2916,7 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL
                 val substedBody  = btm.substitution(body)
                 CaseDef(Alternative(patterns), EmptyTree, substedBody)
               }
-            case _ => //println("can't emit switch for "+ makers)
+            case _ => // patmatDebug("can't emit switch for "+ makers)
               None //failure (can't translate pattern to a switch)
           }
         }
@@ -2696,8 +3141,14 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL
                               with DeadCodeElimination
                               with SwitchEmission
                               with OptimizedCodegen
-                              with SymbolicMatchAnalysis { self: TreeMakers =>
+                              with SymbolicMatchAnalysis
+                              with DPLLSolver { self: TreeMakers =>
     override def optimizeCases(prevBinder: Symbol, cases: List[List[TreeMaker]], pt: Type, unchecked: Boolean): (List[List[TreeMaker]], List[Tree]) = {
+      if (!unchecked) {
+        unreachableCase(prevBinder, cases, pt) foreach { caseIndex =>
+          typer.context.unit.warning(cases(caseIndex).last.pos, "unreachable code")
+        }
+      }
       val counterExamples = if (unchecked) Nil else exhaustive(prevBinder, cases, pt)
       if (counterExamples.nonEmpty) {
         val ceString =
diff --git a/src/compiler/scala/tools/nsc/util/Statistics.scala b/src/compiler/scala/tools/nsc/util/Statistics.scala
index 61c7695911..53ab6654ee 100644
--- a/src/compiler/scala/tools/nsc/util/Statistics.scala
+++ b/src/compiler/scala/tools/nsc/util/Statistics.scala
@@ -60,6 +60,14 @@ class Statistics extends scala.reflect.internal.util.Statistics {
 
   val macroExpandCount = new Counter
   val macroExpandNanos = new Timer
+
+  val patmatNanos      = new Timer
+  val patmatAnaDPLL    = new Timer
+  val patmatAnaVarEq   = new Timer
+  val patmatCNF        = new Timer
+  val patmatAnaExhaust = new Timer
+  val patmatAnaReach   = new Timer
+  val patmatCNFSizes   = new collection.mutable.HashMap[Int, Int] withDefaultValue 0
 }
 
 object Statistics extends Statistics
@@ -71,7 +79,7 @@ abstract class StatisticsInfo {
   val global: Global
   import global._
 
-  var phasesShown = List("parser", "typer", "erasure", "cleanup")
+  var phasesShown = List("parser", "typer", "patmat", "erasure", "cleanup")
 
   def countNodes(tree: Tree, counts: ClassCounts) {
     for (t <- tree) counts(t.getClass) += 1
@@ -83,10 +91,15 @@ abstract class StatisticsInfo {
   def showRelTyper(timer: Timer) =
     timer+showPercent(timer.nanos, typerNanos.nanos)
 
-  def showCounts(counts: ClassCounts) =
+  def showRelPatmat(timer: Timer) =
+    timer+showPercent(timer.nanos, patmatNanos.nanos)
+
+  def showCounts[T](counts: scala.collection.mutable.Map[T, Int]) =
     counts.toSeq.sortWith(_._2 > _._2).map {
-      case (cls, cnt) =>
+      case (cls: Class[_], cnt) =>
         cls.toString.substring(cls.toString.lastIndexOf("$") + 1)+": "+cnt
+      case (o, cnt) =>
+        o.toString +": "+cnt
     }
 
   def print(phase: Phase) = if (phasesShown contains phase.name) {
@@ -169,6 +182,16 @@ abstract class StatisticsInfo {
       if (timer1   != null) inform("#timer1                  : " + timer1)
       if (timer2   != null) inform("#timer2                  : " + timer2)
       //for (t <- uniques.iterator) println("unique: "+t)
+
+      if (phase.name == "patmat") {
+        inform("time spent in patmat       : " + patmatNanos                   )
+        inform("             of which DPLL : " + showRelPatmat(patmatAnaDPLL   ))
+        inform("of which in CNF conversion : " + showRelPatmat(patmatCNF       ))
+        inform("           CNF size counts : " + showCounts(patmatCNFSizes     ))
+        inform("of which variable equality : " + showRelPatmat(patmatAnaVarEq  ))
+        inform("  of which in exhaustivity : " + showRelPatmat(patmatAnaExhaust))
+        inform("of which in unreachability : " + showRelPatmat(patmatAnaReach  ))
+      }
     }
   }
 }
diff --git a/test/files/neg/patmatexhaust.check b/test/files/neg/patmatexhaust.check
index 1168f36e11..4556e6622f 100644
--- a/test/files/neg/patmatexhaust.check
+++ b/test/files/neg/patmatexhaust.check
@@ -14,6 +14,9 @@ patmatexhaust.scala:49: error: match may not be exhaustive.
 It would fail on the following inputs: Gp(), Gu
     def ma4(x:Deep) = x match { // missing cases: Gu, Gp
                       ^
+patmatexhaust.scala:55: error: unreachable code
+      case _ if 1 == 0 => 
+                       ^
 patmatexhaust.scala:53: error: match may not be exhaustive.
 It would fail on the following input: Gp()
     def ma5(x:Deep) = x match {
@@ -34,4 +37,4 @@ patmatexhaust.scala:126: error: match may not be exhaustive.
 It would fail on the following input: C1()
     def ma10(x: C) = x match { // not exhaustive: C1 is not abstract.
                      ^
-9 errors found
+10 errors found
diff --git a/test/files/neg/virtpatmat_reach_null.check b/test/files/neg/virtpatmat_reach_null.check
new file mode 100644
index 0000000000..595c8ec889
--- /dev/null
+++ b/test/files/neg/virtpatmat_reach_null.check
@@ -0,0 +1,4 @@
+virtpatmat_reach_null.scala:13: error: unreachable code
+      case _                              =>  // unreachable
+                                          ^
+one error found
diff --git a/test/files/neg/virtpatmat_reach_null.flags b/test/files/neg/virtpatmat_reach_null.flags
new file mode 100644
index 0000000000..e8fb65d50c
--- /dev/null
+++ b/test/files/neg/virtpatmat_reach_null.flags
@@ -0,0 +1 @@
+-Xfatal-warnings
\ No newline at end of file
diff --git a/test/files/neg/virtpatmat_reach_null.scala b/test/files/neg/virtpatmat_reach_null.scala
new file mode 100644
index 0000000000..6314a5b1d8
--- /dev/null
+++ b/test/files/neg/virtpatmat_reach_null.scala
@@ -0,0 +1,19 @@
+sealed abstract class Const {
+  final def excludes(other: Const) =
+    (this, other) match {
+      case (_, NullConst)                 =>
+      case (NullConst, _)                 =>
+      case (_: ValueConst, _: ValueConst) =>
+      case (_: ValueConst, _: TypeConst)  =>
+      case (_: TypeConst,  _: ValueConst) =>
+      case (_: TypeConst,  _: TypeConst)  =>
+      case (null, _)                      =>
+      case (_, null)                      =>
+      case null                           =>
+      case _                              =>  // unreachable
+    }
+}
+
+sealed class TypeConst extends Const
+sealed class ValueConst extends Const
+case object NullConst extends Const
diff --git a/test/files/neg/virtpatmat_reach_sealed_unsealed.check b/test/files/neg/virtpatmat_reach_sealed_unsealed.check
new file mode 100644
index 0000000000..10638eff52
--- /dev/null
+++ b/test/files/neg/virtpatmat_reach_sealed_unsealed.check
@@ -0,0 +1,14 @@
+virtpatmat_reach_sealed_unsealed.scala:16: error: match may not be exhaustive.
+It would fail on the following input: false
+  (true: Boolean) match { case true => } // not exhaustive, but reachable
+       ^
+virtpatmat_reach_sealed_unsealed.scala:18: error: unreachable code
+  (true: Boolean) match { case true => case false =>  case _ => } // exhaustive, last case is unreachable
+                                                             ^
+virtpatmat_reach_sealed_unsealed.scala:19: error: unreachable code
+  (true: Boolean) match { case true => case false =>  case _: Boolean => } // exhaustive, last case is unreachable
+                                                                      ^
+virtpatmat_reach_sealed_unsealed.scala:20: error: unreachable code
+  (true: Boolean) match { case true => case false =>  case _: Any => } // exhaustive, last case is unreachable
+                                                                  ^
+four errors found
diff --git a/test/files/neg/virtpatmat_reach_sealed_unsealed.flags b/test/files/neg/virtpatmat_reach_sealed_unsealed.flags
new file mode 100644
index 0000000000..e8fb65d50c
--- /dev/null
+++ b/test/files/neg/virtpatmat_reach_sealed_unsealed.flags
@@ -0,0 +1 @@
+-Xfatal-warnings
\ No newline at end of file
diff --git a/test/files/neg/virtpatmat_reach_sealed_unsealed.scala b/test/files/neg/virtpatmat_reach_sealed_unsealed.scala
new file mode 100644
index 0000000000..13911dbd78
--- /dev/null
+++ b/test/files/neg/virtpatmat_reach_sealed_unsealed.scala
@@ -0,0 +1,21 @@
+sealed abstract class X
+sealed case class A(x: Int) extends X
+
+// test reachability on mixed sealed / non-sealed matches
+object Test extends App {
+  val B: X = A(0)
+  val C: X = A(1)
+
+  // all cases are reachable and the match is exhaustive
+  (C: X) match {
+    case B =>
+    case C =>
+    case A(_) =>
+  }
+
+  (true: Boolean) match { case true => } // not exhaustive, but reachable
+  (true: Boolean) match { case true => case false => } // exhaustive, reachable
+  (true: Boolean) match { case true => case false =>  case _ => } // exhaustive, last case is unreachable
+  (true: Boolean) match { case true => case false =>  case _: Boolean => } // exhaustive, last case is unreachable
+  (true: Boolean) match { case true => case false =>  case _: Any => } // exhaustive, last case is unreachable
+}
\ No newline at end of file
diff --git a/test/files/pos/virtpatmat_reach_const.scala b/test/files/pos/virtpatmat_reach_const.scala
new file mode 100644
index 0000000000..b55b7cb229
--- /dev/null
+++ b/test/files/pos/virtpatmat_reach_const.scala
@@ -0,0 +1,11 @@
+// check the interaction between constants and type tests in creating the equality axioms
+object Test {
+  type Formula = List[String]
+  val TrueF: Formula = List()
+  def distribute(a: Formula, b: Formula) = (a, b) match {
+    case (TrueF, _) =>
+    case (_, TrueF) =>  // bug: considered unreachable
+    case (a :: Nil, b :: Nil) =>
+    case _ =>
+  }
+}
\ No newline at end of file