Simmo Saan

Apparently the `Pretty.text` primitive directly uses that but does something involved under the hood to break the text up further (based on `\n`). It's just the massive strings of Apron...

I pinned the fixed goblint-cil on master, so Goblint actually uses the optimization as well.

More broadly, it might be worth experimenting with alternatives to various data structures like `Map`s (although the baby library doesn't yet have them) or `Hashtbl`s. This includes both libraries that...

This might not yet be publicly announced, but the deadline for new task submission to SV-COMP 2025 should be October 15, 2024. This can be done before #1485 is merged....

I thought it'd be a good way to review the tests at the same time, but already with the first test I realized this would be so much work. It...

On entire sv-benchmarks runs with 60s, this doesn't really make any difference to our score (after the second fixes). Some tasks (loop-lit/hh2012-ex1b) go from

Something related to this shows up in our own witness validation in SV-COMP. This is illustrated with the following test, where the assertion is unknown: ```c #include int main() {...

> However, it seems unclear what that is supposed to do: Currently, the effect is that while paths are kept separate, they are then **all** propagated to callees. This seems...

I was about to suggest the `tred` algorithm: https://gitlab.com/graphviz/graphviz/-/blob/fb242ae33b809d87f46fe3a20bb95a6fc70f51d5/lib/cgraph/tred.c. It's obviously more optimized with a special-purpose DFS, but the important difference might be that it doesn't run all DFS-s at...

How large are the dump files themselves? It could either be that the input files are already overly massive or that the comparison somehow allocates too much something.