Unassume witness invariants during solving

[sim642]

This PR adds an unassume analysis, which loads a YAML witness before solving and emits Unassume events during the analysis at nodes which have invariants. Both base, apron and var_eq analysis handle these events to make their local states less precise to immediately account for all states matching the invariant. Since the parsed invariants should be from a completed analysis, they correspond to the fixpoint. Thus unassuming the invariants allows the analysis to directly jump to that fixpoint. The benefits of this are two-fold:

1. It avoids widening-narrowing iterations to reach the same fixpoint, speeding up the analysis (hopefully).
2. It avoids widening jumping over fixpoints (especially with apron that cannot narrow), making the analysis more precise.

Changes

Besides the unassuming, many surrounding bigger and smaller changes are included:

1. Extract base analysis branch invariant out to a separate BaseInvariant module. This is a fairly large part of base analysis code, but sufficiently self-contained that it can be decoupled. The real reason for doing this was to use a slightly modified version of invariant for unassuming without a complete copy of invariant.
2. Add widening tokens, a dynamic way to delay widenings: http://www2.in.tum.de/bib/files/mihaila13widening.pdf. This turned out to be necessary, otherwise unassume itself causes a widening and becomes even less precise than intended.
3. Add witness.invariant.exact, which allows disabling the generation of exact equality invariants that are useless for unassuming.
4. Add witness.invariant.exclude-vars, which is a list of regexes for variable names that invariants should not be generated for. This can be tuned for sv-benchmarks which have already been CIL-led and contain awful amounts of temporaries.
5. Improve base branch refinement for address sets, interval bound non-equality and disjunctions of address/int equalities.

TODO

• Emit Unassume events after all transfer functions, not just assign.
• Support unassuming preconditioned invariants.
• Support unassuming multithreaded invariants about globals (at locations)? This kind of requires us to first generate such invariants properly. (Privatized location invariants in YAML witnesses #833)
• More precise unassuming than doing an assume on a top state and joining that in? In base, this probably would be an invariant-like recursive computation; in apron, not sure if anything better can be done.
• Clean up and document widening tokens.
• Adapt tests to Refactor stub libraries structure #845.

[michael-schwarz]

I think once the comments are addressed and the adaptations necessary because of the new affeq analysis are made, this is ready to be merged.