Simmo Saan

The sv-benchmarks MR for excluding this program has been merged.

I now brought this up to date and the previously failing incremental test at least passes now. But somehow this is breaking incremental tests with CFG comparison. **EDIT:** I managed...

@michael-schwarz Was it the plan for some students to benchmark this? If so, then this should be in a suitable state for doing so. It's still suboptimal due to extra...

It does work non-incrementally, so it would still be possible to benchmark this. If there's no benefit, then there's no reason to try to fix it for CFG comparison either....

I merged `master` into this and two CFG comparison tests still fail: one crashes in some `List.iter2` and the other is unsound.

> Could this issue be related to the issue you uncovered with `List.mem` @sim642? I don't believe so. I directly fixed remaining instances directly on master: bcb4de29e22885570ba82f7ec9cee2e661854b7a. None of those...

@michael-schwarz I think I've now done all the tinkering on this that I intended, so you can also have a final look. Just a reminder here at the end again:...

I merged `master` into this to see what's the state of this. The test case no longer runs because there's no `wpoint` solver, but: 1. `wpoint` solver was renamed to...

> The three changes to region domain lattice operations is something I'm still looking into to see if they make sense or matter at all (I suspect they might even...

iowarrior is not new, but it hasn't just been mentioned in any issue. The program itself is problematic, so there's already an sv-benchmarks MR for it: https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/merge_requests/1374 (**EDIT:** merged).