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.

removeVarEq may throw an AnalysisBudget.Exception
use arraybuffer to build formula