Simmo Saan

I suppose we could have two options to control this behavior: 1. `sem.malloc.zero.null` - boolean whether `malloc(0)` may return `NULL`. 2. `sem.malloc.zero.blob` - boolean whether `malloc(0)` may return a (pointer...

Just `ask` isn't enough for these kinds of things though, they also need `global`. For example, the deadlock analysis needs to traverse the entire cycle starting from a global.

Hmm, yes, real-world programs might actually use these. The sensible thing would be to actually check if the program uses them other than the declaration.

I haven't checked if this is possible, but maybe we could even add `ctx` to the arguments of `context`. That gives access to the caller node (and thus its `fundec`)....

Syntactic unrolling avoids this by introducing separate nodes and thus constraint unknowns for each iteration. Via that the solver can establish sensible fine-grained dependency structure and avoid recomputations of all...

I'm closing this because we now have ideas for an alternative approach that should avoid the inefficiencies.

> I don't know if we'd want to have this back, but it could also make for interesting benchmarking. And indeed it did, on SV-COMP ConcurrencySafety at least (if I...

> I think congruences are enabled by the autotuner. Sorry, yes. I meant that just about interval sets.

There's now an option to disable these simplifications. This includes the possibility to even disable the definite integer simplification. These simplifications are the default, to give nicest output out of...

Surprisingly, letting `join` not refine, but making `widen` refine passes all our tests, including this one. https://link.springer.com/chapter/10.1007/978-3-540-77505-8_23 mention an obscure concept of _pre-widening_ as a version of `join` which doesn't...