Simmo Saan

Besides the couple of unresolved comments, the test group 58-array_annotations needs to be renumbered to 60-array_annotations to avoid conflict on master.

> * Raising `Deadcode` during `special` for `pthread_cond_wait` does not work, probably related to the `split` and `event` business in `mutexAnalysis.ml`. Any ideas there @sim642? You would just conditionally have...

Just to have this here, my earlier take on this as a constraint system functor and actually using exceptions for aborting right-hand sides is here: https://github.com/goblint/analyzer/commit/531b8a60fce17a99a3fc1a6eee49ca757539e295 (also in `caching-constrsys` branch).

> @jerhard and I managed to solve the performance degradation: It seems like this `dep_vals` was populated to eagerly! Looks like after pulling that `dep_vals` populating code from `eval` to...

This probably only matters if this PR provides meaningful speedup and we want to have it, but currently this is on top of #391, where all aborting was now reverted...

> my next ambition would be to somehow integrate this with superstable such that warnings etc can be re-used for things that were destabilized, but their RHS never needed to...

> The performance story is still a bit mucky: sometimes we have big savings, sometimes it doesn't matter, and sometimes it is worse. It would be a good idea to...

Given the renowned activity on this, I guess you're intending to polish this into a working state. If so, then we should really think about this point I had in...

> I think the reason we are opposed to having it as a functor around the constraint system on the Munich side is that any such data structures that are...

> What I meant here was removing the pre-processing of all the solver data structures for the incremental mode from the solver itself and putting it somewhere else. #545 does...