Fix out of memory error in exhaustivity check in pattern matcher.

The OOM could occur when all models are forcibly expanded in the DPLL solver.

The simplest solution would be to limit the number of returned models but then
we are back in non-determinism land (since the subset we get back depends on
which models were found first).

A better alternative is to create only the models that have corresponding
counter examples.

If this does not ring a bell, here's a longer explanation:

The models we get from the DPLL solver need to be mapped back to counter examples.
However there's no precalculated mapping model -> counter example. Even worse,
not every valid model corresponds to a valid counter example.
The reason is that restricting the valid models further would for example require
a quadratic number of additional clauses. So to keep the optimistic case fast
(i.e., all cases are covered in a pattern match), the infeasible counter examples
are filtered later.
The DPLL procedure keeps the literals that do not contribute to the solution
unassigned, e.g., for  `(a \/ b)`
only {a = true} or {b = true} is required and the other variable can have any value.
This function does a smart expansion of the model and avoids models that
have conflicting mappings.
For example for in case of the given set of symbols (taken from `t7020.scala`),
only one can be set to true,
since `V2` can at most be equal to one of {2,6,5,4,7}:
 "V2=2#16"
 "V2=6#19"
 "V2=5#18"
 "V2=4#17"
 "V2=7#20"