Fix non-determinism in DPLL algorithm. The function to compute all solutions was flawed and thus only returned a subset of the solutions. The algorithm would stop too soon and thus depending on the ordering of the symbols return more or less solutions.
I also added printing a warning when the search was stopped because the max recursion depth was reached. This is very useful as an explanation of suddenly failing regression tests, since less counter examples are reported.
The formulas that were passed to the solver resulted in invalid counter examples that were then removed in a following filtering step. That led to the weird situation where the fixed DPLL algorithm returned less counter examples than the buggy version.

I tried to keep the warnings compatible to the warnings before. For example in case of `patmatexhaust.scala` the old behavior was to report to report `Gu` and `Gp` as missing, even though matching only on `Gu` would also catch `Gp`. In order to return the same counter examples, we must explicitely specify in `mutuallyExclusiveDomainSyms` what symbols can be reported together.