Proof Refactoring

[maul-esel]

This PR refactors how ULTIMATE works with proof artifacts (for now, primarily Floyd-Hoare annotations). The point is:

1. to make it easier to work with proofs, by making them first-class concepts (e.g. IFloydHoareAnnotation) rather than annotations in an Icfg. This allows e.g. considering the proofs of multiple CEGAR loops separately (a more elegant solution than the workaround used in #670).
2. to make the handling of proofs more flexible, in preparation for supporting other kinds of proofs; most importantly, thread-modular proofs at many levels and Owicki-Gries proofs. These other kinds of proofs are e.g. needed for concurrency correctness witnesses.

I consider the PR more or less ready for review, if the currently running nightly tests don't show any more issues. The only change I still have planned from my side is to go through the .epf files and adapt them to the following change in the settings for TraceAbstraction:

The setting Compute Hoare Annotation of negated interpolant automaton, abstraction and CFG has been removed. The existing setting Positions where we compute the Hoare Annotation has a possible value NONE (the default value) to disable Hoare computation completely.

However, I wanted to first ask if anyone objects to this or would propose a different settings structure, before I start going through all the settings files.

[maul-esel]

Thanks for the reviews. I'll wait for the nightly test run; if no further issues occur I will merge this tomorrow.

[maul-esel]

Fixing the tests required some changes:

• The precondition for our Floyd-Hoare annotations is not necessarily true; instead, it is a conjunction of (= g |old(g)|) for all modifiable global variables g of the initial location's procedure. This requires supporting different preconditions per initial location, in the case of multiple initial locations.
• A bug in BlockEncodingV2 caused contract computation to fail, as some procedures did not have an exit location. I've fixed this, and added some checks to prevent similar bugs in the future.

While doing this, I also added a feature required e.g. in the context of requirements analysis: Each proof now also has an explicit description of the specification that it proves. This information is also added to InvariantResult and ProcedureContractResult (in the form of Check objects).