These changes allow computing Floyd/Hoare annotations for
product automata of concurrent programs.

BasicCegarLoop should not refer to Floyd/Hoare proofs, let NwaCegarLoop
handle this. Also, CEGAR loops refer directly to Hoare annotation states,
not IcfgLocations.

Do not check the setting again, the caller should supply the appropriate states.

Also define their semantics in the class itself,
rather than in some utility class.

…kerUtils

…cers

…on & document

…ntSynthesis

# Conflicts:
#	trunk/source/InvariantSynthesis/src/de/uni_freiburg/informatik/ultimate/plugins/generator/invariantsynthesis/InvariantSynthesisStarter.java
#	trunk/source/Library-ModelCheckerUtils/src/de/uni_freiburg/informatik/ultimate/lib/modelcheckerutils/smt/predicates/PredicateUtils.java
#	trunk/source/Library-Proofs/src/de/uni_freiburg/informatik/ultimate/lib/proofs/floydhoare/HoareAnnotationComposer.java
#	trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/TraceAbstractionStarter.java
#	trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/TraceAbstractionUtils.java
#	trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/predicates/HoareAnnotationChecker.java

CEGAR loops decide which kinds of proofs they provide and how.
Disentangle possible postprocessing of proofs from CEGAR loops
and proof production.

# Conflicts:
#	trunk/source/InvariantSynthesis/src/de/uni_freiburg/informatik/ultimate/plugins/generator/invariantsynthesis/InvariantSynthesisStarter.java
#	trunk/source/Library-ModelCheckerUtils/src/de/uni_freiburg/informatik/ultimate/lib/modelcheckerutils/smt/predicates/PredicateUtils.java
#	trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/TraceAbstractionStarter.java

- introduce marker interface IProof to avoid using Object
- decouple AbstractCegarLoop, CegarLoopResult from proof production
- remove useless interfaces
- decouple proofs and proof translation from IInitialAbstractionProvider interface

…necessarily "true"

…to prove asserts inside the procedure

Removes the workaround introduced in 720a012, as proofs of different
CEGAR loops are now stored separately in the ICFG.

# Conflicts:
#	trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/NwaCegarLoop.java

This is particularly useful if we create multiple proof objects
for the same program and different (partial) specifications, to
distinguish which proof objects relate to which specification.

…ation

Every procedure that exists in the IIcfg should have an exit location,
even if that location is unreachable.

This was not the case for the IIcfgs produced by the BlockEncodingV2 plugin.
This commit fixes this bug, and introduces an assert statement after block
encoding has finished to check if the produced IIcfg satisfies this invariant.

Moreover, we add two sanity checks regarding the computation of procedure contracts,
where the problem was discovered (the location of the ProcedureContractResult was null),
such that similar issues are caught earlier in the future.

# Conflicts:
#	trunk/source/InvariantSynthesis/src/de/uni_freiburg/informatik/ultimate/plugins/generator/invariantsynthesis/InvariantSynthesisStarter.java
#	trunk/source/Library-ModelCheckerUtils/src/de/uni_freiburg/informatik/ultimate/lib/modelcheckerutils/smt/predicates/HoareAnnotation.java
#	trunk/source/Library-ModelCheckerUtils/src/de/uni_freiburg/informatik/ultimate/lib/modelcheckerutils/smt/predicates/PredicateFactory.java
#	trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/HoareAnnotationWriter.java

# Conflicts:
#	releaseScripts/website-config/frontend/config.js
#	trunk/source/WebsiteStatic/config/config.dist.js