Storing CPA in ReachedSet

As discussed in 21fb4896 (comment 652539366) our "main" CPA instance (the one used by the CPAchecker class) is not always the CPA instance that corresponds to the abstract states in the resulting reached set from a CPAchecker run, for example not in cases of composite analyses and uses of ForwardingReachedSet. This could lead to problems if code analyzes the reached set and applies the wrong CPA to it.

The best way to fix this is to add a reference to the respective CPA (i.e., the one that created the contained abstract states) to the reached set, and this MR implements this. This will also allow to proceed with #909 (closed).

Steps:

• Add factory methods to reached-set factories that accept a CPA
• Change all callers such that they provide a CPA instance
• Store reference in DefaultReachedSet and expose it in ReachedSet interface
• Use it where it makes sense

The current state is that all easy callers of reached-set factories have been converted. Some can easily be converted together with step 3.

TerminationAlgorithm.addInvariantsToAggregatedReachedSet is a tricky case, but a dummy CPA will suffice for now because the reached set created there is only used shortly and then passed somewhere else, where it is used only as UnmodifiableReachedSet, which won't get the method for retrieving the CPA.

And there are two more difficult cases that will be discussed below. These are the ones that currently produce a compiler warning.