SMG consistency checks

This is an 'overview' of points we may want to change regarding any checks on SMGs. See also upstream #712.

General things

  • Use assertions / google's Verify exception instead of SMGInconsistentException so it is treated as a CPAchecker bug and not swallowed.
  • Add message directly to the exception. Fail immediately when an inconsistency is found, instead of waiting for all checks to pass. I can't see the use of it.
  • Use assert in top-level calls so the checks are disabled by -benchmark option.
  • Maybe reconsider where it is enabled by default (currently a HALF setting is default). Separate option for more frequent/thorough checks as FULL is too expensive?

SMG-specific things

  • Check against FIT-TR-2012-04 p.8?
    • add nesting consistency
  • join.SMGJoinSubSMGs#performChecks is set to false and never changes. Are these checks needed? They are ignored even in tests, e.g. SMGRegionsWithRegionsTest#testAbstractionOfLinkedRegionsWithSubregions() fails if I turn them on.
  • Check for PTE with wrong target specifiers. Note, algorithm 11, line 7 explicitly overrides target specifiers that are wrongly written in Algorithm 7, line 3 for two regions abstracted into a list 2+.
  • Should such checks be moved into constructors / add/remove methods? That is, assert that a new edge is consistent with all present edges when we are constructing and adding it, instead of checking this after at some checkpoint.
Edited by Васильев Антон Александрович