Expensive "runtime checks" of SMG analysis

There are several problems related to the "runtime check" feature of the SMG CPA (which checks SMGs for inconsistency during the analysis):

• The standard configuration file config/smg.properties enables the full set of expensive checks.
• These checks are not interruptible with the ShutdownManager.
• They use log level SEVERE for reporting errors (e.g., in SMGConsistencyVerifier), which violates our logging guidelines and is bad for unit tests because log messages are typically lost there.
• They use boolean return values to determine whether the check was successful instead of throwing exceptions, which is error-prone and can easily lead to an error being hidden (we just noticed this with sv-benchmark's check.py).
• Besides the option cpa.smg.runtimeCheck, there exist static mutable fields in the class CLangSMG that control whether the check is done, meaning it is hard to understand whether and when checks are done (some methods run the checks if the option is set, some methods run the code if the field is set).
• They are not integrated with our existing system of disabling sanity checks (-disable-java-assertions and -benchmark), meaning they will run even if somebody told CPAchecker explicitly to run as fast as possible and disable these kinds of checks.

I would suggest to:

• Change the checks to throw exceptions on failure.
• Put all relevant info into the exception message or additional fields on the exception and remove the error logging.
• Remove all the static state.
• Enable the checks if and only if assertions are enabled. This is the same that we do with CFACheck.check. To make sure that the checks are executed in tests the tests could fail if assertions are disabled.

If there is really the need for having different levels of checks, it should at least be integrated with the standard options, e.g., no checks if assertions are disabled, standard checks in production if assertions are enabled, and full set of checks in tests.

If a full refactoring cannot be done soon, we should at least fix the problem that too many checks are run by default.

Btw: Why do the config files for SMG override so many defaults from the options of the SMG CPA? Is it not possible and better to put these values as default into the code?