Simmo Saan

> It seems to me, that it would be more suited to ensure that the `current_node` is set correctly on a `join` than to pass the `precision` around in so...

> The `eval_int` that is called by the `smart_join` within the partitioned array domain then evaluates whether `i - 1 == 0`. `i` has an integer value that come from...

I think I will cherry-pick some (working) changes from this PR to a new PR that could be safely merged. Then we could already benefit from some optimizations while the...

I've been debugging the reluctant destabilization problem and decided to do some tracing on `master` to see how it works with the one big CFG hashtable there, but I have...

> I created a test case where this leads to the function foo being dead after the incremental run (which is not the case in 03-precision-annotation/01-change_precision because the added precision...

> The `varinfo` receives a new id because the declaration was newly added. I'm not so sure whether the distinguishing between changes in `GFun` and `GVarDecl` in the comparison algorithm...

Just to make it very clear, this is blocked by #627.

As found by @michael-schwarz, there seems to be a closely related issue: https://github.com/goblint/bench/issues/16#issuecomment-1023440349. But that one is crashing on the iteration of `slocals`, not `sallstmts`. I suppose there's also the...

@stilscher Actually the problem described here wasn't about comparing function declarations, although I guess with the uniqueness check it might already fail during comparison. The issue was with updating the...

> To recap from Gobcon yesterday: The bottoms that are inserted are meaningful in that the hashtable for a partial (post-)solution should be closed, i.e. not depend on any implicit...