Finalize options, so that they cannot be mutated after the solver started

[michael-schwarz]

Pulled out from #28 since most of the TODOs there are now done.

This would gives us an additional safety guarantee that no options are modified after the solver has started, which may lead to inconsistent results, crashing (e.g. if the list of activated analyses is modified), and other undesirable things.

[sim642]

We'll also need to unfinalize them such that server mode can modify options.