Simmo Saan

> I think I also still need to make sure that the new incremental cram tests are also automatically executed in the CI. That probably needs a step like this...

As determined during GobCon, the problem is this check: https://github.com/goblint/analyzer/blob/33775dbcc680622acb836129e2b157372c57ebc7/src/analyses/mallocWrapperAnalysis.ml#L131-L133 When the second (non-unique) thread locks the mutex, it checks whether it is unique and only considers the case when...

The failures were in unit tests, not regression tests. `dune runtest` should run them all.

This is also a fairly big PR and has changes that often conflict with other changes on master, so it would be great to also get this merged soon.

["Generation of Violation Witnesses by Under-Approximating Abstract Interpretation"](https://link.springer.com/chapter/10.1007/978-3-031-50524-9_3) also contains some improved powerset widening.

I did the refactoring currently in a separate branch: https://github.com/goblint/analyzer/tree/eager_destab_cheap_abort-refactor. Since it depends on #909, I didn't yet merge it here in order to not clutter the diff with changes...

I now ran this on sv-benchmarks and there it doesn't help, but has ~3% slowdown:  ([Full table](https://goblint.cs.ut.ee/results/108-all-fast-abort-after/results/results.2022-12-05_13-30-27.table.html#/scatter?toolY=1&columnY=1&filter=0(0*status*(category(notIn(error)))),1(0*status*(category(notIn(error))))&results=All&regression=Linear&scaling=Linear&line=1.2&toolX=0&columnX=1))

Sure, I just disabled it by default for now.

Actually the TODO sounds like it's just about casts between different array sizes (e.g. `int[2]` and `int[4]`), but the incompatibility here is even worse: the array contents aren't being cast...

Other pointers to the array are irrelevant at this point: nothing is being changed here, this logic already is part of reading in `eval_offset`. This is when you are _reading_...