Sarah Tilscher

So I reconstructed what you described above. The reluctant destabilization works fine on a minimized example without the precision annotation. In the run on 03-precision-annotation/01-change_precision, the problem arises because the...

>This feels like a quick hack than a proper fix, because really the problem is with the incremental comparison and updating, if it gets confused by a `GVarDecl` Actually I...

It is still an issue that needs to be fixed.

Yes, the `compare_runs` worked for the zstd benchmarks. Only the configuration was different there and it was used together with the new node comparison, that compares abstract values of unknowns...

You could still achieve this by setting the configuration option `force-reanalyze`. I would find that more transparent because I think that there should not be any hidden assumption regarding the...

I created a small example to test the open questions that @jerhard posted above. It seems that the merger is not behaving correctly. If `merge_inline` is disabled a function definition...

Yes, another round of feedback would be great. I think I also still need to make sure that the new incremental cram tests are also automatically executed in the CI....

I thought it would be good to wait for an approval in the reviews before merging.

> I cannot find anywhere were global variable initializers are even compared for incremental. There is CompareAST.eq_init but it is dead code (it was even removed in https://github.com/goblint/analyzer/commit/711d37bb0584e69bbf1c5881013af0006b1c5fba, but somehow...

Since the number of commits is very large, but only few lines of code have been changed, I would suggest to squash merge this PR after the review is finished.