Component-based CEGAR and invariant witnesses

This MR contains configurations for component-based CEGAR. It includes a configuration for a single CEGAR step (for refinement for the precision of the predicate abstraction), and a relaxation of the correctness witness, called invariant witness: An invariant witness contains all found path invariants at all program locations as disjunctions, but does not simplify all invariants to 'true' if any path invariant at a certain program location is 'true' (the correctness witness does this simplification).