Simmo Saan

I think the reason we kept it so far is because there's a distinct check there ```ocaml HM.mem called y || destabilize_vs y || b || was_stable && List.mem_cmp S.Var.compare...

Adding the hook call isn't controversial I think. I don't understand what's the issue with `||` though, they both recurse if not in `called`.

> It's a clean code thing, I find the more explicit > > ```ocaml > if not (HM.mem called y) then destabilize_vs y else true > ``` > > to...

As to the code duplication, `destabilize_with_side` is an even worse offender with very similar loops (only over different sets): https://github.com/goblint/analyzer/blob/06bc1e1e47f760df217ed45387743e82b9488d69/src/solver/td3.ml#L568-L605 Getting rid of the duplication is a bit of a...

It's not an unsoundness bug but an usability feature regarding unsoundness.

Now that the thesis is done, will this still be worked on or not? I don't recall where I originally noticed this, but this may be quite crucial now because...

After some more digging into silver searcher it appears that `strdup` might not be the main biggest hurdle. Rather it seems proper value analysis of thread-local variables (#876) is more...

I guess this might be what the `ReachableUkTypes` query is trying to do. Although it's a completely separate reachability computation which isn't good for performance nor consistency.

This doesn't seem intentional to me: https://github.com/goblint/analyzer/blob/bffc5e3cbb1f43bd5c9483a6545802cfba5d3d76/src/autoTune.ml#L139-L142 The autotuner is only enabling this annotation option which again has very surprising implications that are not documented anywhere: > Enable manual annotation...

With PR #1623 merged, this also causes that domain to spuriously be activated in svcomp configuration, although we have no intended autotuning for it.