Simmo Saan

Indeed, since those are our only usages of `must_be_parent` and `may_create`, they might not and I didn't consider that so far. Although there we require `current` to be must parent,...

I managed to simplify and optimize it to something reasonable by using a simple (but efficient) `GobList.remove_common_prefix` function. The old way of checking of `p` is a prefix of `p'`...

I went through all the unit tests for the improved cases and tried to construct a real program for each one. Five of them have a corresponding regression test now...

A before vs after benchmark run on SV-COMP ConcurrencySafety with 60s timeout gives zero verdict differences and performance differences are also just within measurement noise. As to the over-approximated $$C$$...

I offered a thesis topic on formally verifying this but there's no student working on it (and I'm not sure if there ever will be), so we shouldn't wait for...

I added some more explanations to the three comments. I wouldn't want to outright remove them because then it's unclear why something might appear missing.

cava has a lot of missing library functions though, so how exactly are you intending to analyze it without losing all precision from invalidations? I'm not sure how correctly those...

The `_with` suffixed versions are standard in Apron and those three are far from the only ones: https://github.com/goblint/analyzer/blob/2fa4f55e682da3ad937e394fe20449eeef4c9634/src/cdomains/apron/apronDomain.apron.ml#L133-L151 It looks like `ApronDomain` was oddly split into `RelationDomain` and `SharedFunctions`.

> @sim642: Do you recall why this was necessary? It seem that unnecessarily ties us to only having imperative implementations whereas the old setting allowed us to have both pure...

> If we replace them with their `pt_with` equivalent, we could get rid of > > ```ocaml > type t = { > mutable d : RelDomain.t option; > mutable...