SI-7746 Fix non-determinism in the DPLL algorithm and disallow infeasible counter examples directly in the formula.

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 are passed to the solver are now restricted in order to avoid generating invalid counter examples.
Previously the incorrectly set up formula resulted in invalid counter examples that were then removed in
the following filtering step.
That led to the weird situation where the fixed DPLL algorithm returned less counter examples than the buggy version.
Cleanup `LinkedHashSet` fixes and replace them with `Set` (i.e., back to initial implementation).

Since the non-determinism in the DPLL procedure has been fixed that workaround is not needed anymore.