Julian Erhard

>I didn't check, but this sounds a lot like something I fixed in https://github.com/goblint/analyzer/pull/796: https://github.com/goblint/analyzer/commit/73df4cac9812c65a3446c7ea53770fa6d45d59d6. If that's the right thing, then you can just cherry pick it. I needed to...

I tested this with `bench/cp_comb.c`: when one sets the `surroundByAtomic` in `EvalAssert` to `false`, and adds an `#include` to the resulting `transformed.c`, the C-file can be compiled. However, the executable...

>I think the issue is due to flow-insensitivity of the global alloc variable, which initially has all bot fields, but then gets default_tuning in there. But we don't distinguish at...

Looking at this with @michael-schwarz and Helmut, we found that performing a context-insensitive analysis and not generating asserts for blobs gets rid of the asserts that fail during some simple...

There are still three issues in the generated code that required manual fixing: - [e.g. here](https://gitlab.com/erhardj/sv-benchmarks/-/commit/77d88a8cdfe237d1266fefce939f24e51fe803f2), asserts are generated for `table` -- which is a type, not a variable. -...

>Is that also preserved by Mergecil? Because even if Cabs2cil on each file does produce at most one declaration (in addition to a definition), then maybe Mergecil leaves all the...

The question thus is whether - when `merge_inlines` is `false`, there can be multiple inline function definitions with the same name? - when `merge_inlines` is `true`, there can be multiple...

>If merge_inline is disabled a function definition and an inline function definition with the same name but in a different translation unit do not get merged but are not renamed...

This indeed fixes the crash on at least cksum_comb.c and cp_comb.c (did not try the others yet). The question is, whether a fallback to `bot` is the right thing to...

>Might be worth just temporarily printing out the constraint variable names that it happens with to see if it could be a problem. This produces a long, but mostly repeating...