SI-6479 Don't lift try exprs in label arguments.

The new pattern matcher uses label jumps to GOTO
the next case. Uncurry treated these like regular
method arguments, and performed the liftedTree()
transformation, which ensures that try expressions
are only used in a statement position. Even try
in statement position of a block used as such an argument
are subject to the same transform.

This transform stems from the JVM limitation,
that try/catch does not leave a value on the stack.
See b194446.

This commit changes Uncurry to avoid this transform
for arguments to label jumps. This avoids needlessly
indirect code, and enables tail call elimination in
more cases.

As an example, Scala 2.10.0 transforms the last
method of the enclosed test case to:

      try {
        case <synthetic> val x1: Int = 1;
        case5(){
          if (2.==(x1))
            {
              val x2: Int = x1;
              matchEnd4({
                {
                  def liftedTree2(): Unit = try {
                    throw new scala.runtime.NonLocalReturnControl[Unit](nonLocalReturnKey1, ())
                  } catch {
                    case (e @ (_: ClassNotFoundException)) => ()
                  };
                  liftedTree2()
                };
                TailrecAfterTryCatch.this.bad()
              })
            }
          else
            case6()
        };
        case6(){
          matchEnd4(throw new MatchError(x1))
        };
        matchEnd4(x: Unit){
          x
        }
      } catch {
        case (ex @ (_: scala.runtime.NonLocalReturnControl[Unit @unchecked])) => if (ex.key().eq(nonLocalReturnKey1))
          ex.value()
        else
          throw ex
      }

After this patch:

    @scala.annotation.tailrec final def bad(): Unit = {
      case <synthetic> val x1: Int = 1;
      case5(){
        if (2.==(x1))
          {
            <synthetic> val x2: Int = x1;
            matchEnd4({
              try {
                return ()
              } catch {
                case (e @ (_: ClassNotFoundException)) => ()
              };
              TailrecAfterTryCatch.this.bad()
            })
          }
        else
          case6()
      };
      case6(){
        matchEnd4(throw new MatchError(x1))
      };
      matchEnd4(x: Unit){
        x
      }
    }
SI-6942 more efficient unreachability analysis

Avoid blowing the stack/the analysis budget by more eagerly translating
the propositions that model matches to CNF.
First building a large proposition that represents the match,
and then converting to CNF tends to blow the stack.
Luckily, it's easy to convert to CNF as we go.

The optimization relies on `CNF(P1 /\ ... /\ PN) == CNF(P1) ++ CNF(...) ++ CNF(PN)`:

Normalizing a conjunction of propositions
    yields the same formula as
concatenating the normalized conjuncts.

CNF conversion is expensive for large propositions,
so we push it down into the conjunction and
then concatenate the resulting arrays of clauses (which is cheap).

(CNF converts a free-form proposition into an `Array[Set[Lit]]`, where:
 - the Array's elements are /\'ed together;
 - and the Set's elements are \/'ed;
 - a Lit is a possibly negated variable.)

NOTE: removeVarEq may throw an AnalysisBudget.Exception

use arraybuffer to build formula

interface work
use ArrayBuffer instead of Array to build Formulae