The satsolver is reatined and only updated with new clauses for every
state that is generated out of a core. Once the core becomes Open (as
opposed to expandable), the solver is no longer needed.

This patch makes the solver a `Solver option` and gets it deallocated
once no longer needed and resets the hashtable (makes it empty and zero
size) to save memory. This saves about 60% memory usage on some extreme
cases (e.g. exp_unsat from the CTL Benchmark set)

This makes the identifying information be of type bset*bset instead of
bset and adds tracking of deferrals for propositional reasoning and --
in case of K -- for modal reasoning

As there should never be free variables in formulas within the
FL-Closure maybe we should rather signal an error here?

Make following state of a fixpoint it's unfold

should now properly calculate the FL-Closure

Patch by Florian Widmann In order to fix the behaviour for the K*K
formulas

    [pi1]<R>c0 | [pi1]<S>c1 | [pi2]<T>c3
    [pi1]<R>c0 | [pi1]<S>c1 | [pi2]<T>c3 | [pi1][U]c4