Incremental verify and warnings

[sim642]

Problem

Currently when running incremental analysis save and load without any changes to the program on https://github.com/goblint/bench/blob/master/pthread/aget_comb.c, the incremental loading has the following timings:

TOTAL                           1.061 s
  parse                           0.006 s
  convert to CIL                  0.007 s
  compareCilFiles                 0.007 s
  analysis                        1.042 s
    global_inits                    0.002 s
    solving                         0.500 s
    verify                          0.529 s

In solving TD3 performs reachability, which will iterate over the whole thing, regardless of incrementality.
In verify verification iterates (problematically, see #367) over the whole thing to generate warnings about the whole program, regardless of incrementality.

Even these single iterations over an unchanged solution take significant time and CIL is far from the bottleneck here!
And being unchanged, this is the best-case scenario, which will only be worse as the programs get bigger than aget (which takes 4.4s to analyze from scratch).

Right now, we cannot just disable verify either for incremental analysis, because then we'd get no warnings for the reanalyzed program since program warnings are generated during verify.

Solution

Hence we need warnings (actually all Messages) and thus their generation in verify to also be handled incrementally: all warnings from non-obsolete code can be reused from the previous run and the warnings from changed code should be generated during verification of only the changed solution.

This probably requires additional improvements to the message system, to keep track of the nodes (not just locations) and constraint variables whose right-hand sides emitted these, to be able to selectively remove them at incremental load.
Together with the newly emitted warnings from reanalyzed code, the warnings from the incremental run should make up the same set as from-scratch analysis.

And for that we need incremental partial verify, which can just check the relevant parts of the new solution. Since the destabilization and resolving is all in top-down manner, it's likely that incremental verify would also have to be.
This is in line with the proposal in #367 to also verify top-down.

For the incremental case, it'd probably make sense to have an option, whether verify is partial (trusting the old solution) or full (doing the slow thing, which we don't want for interactivity). It might still in some case be good to be able to do full verify in incremental in case there's some bug with the partial verify.

[sim642]

This was done by #372 into #391.