Simmo Saan

> It means that every miniscule change to the analyzer, it's solvers or how it outputs things amounts to re-checking all the generated diffs for the benchmarks Anything that is...

Yet another thing Cram tests would be really useful for is witness generation, both YAML and GraphML, which are currently completely untested. It would just need an option for slightly...

> 1. and 2. are actually things that are all tackled within #186 by our Master's Practical student who will hopefully make a PR any day now. I guess the...

We'll also need to unfinalize them such that server mode can modify options.

By the way c44f9cabbb434406870fa13350ec045484878363 from #770 accidentally works around the unsoundness issue by making the bot-valued variable expression have a top value instead. That is how I stumbled upon the...

Since #809 makes this problem even more urgent, we probably need a quicker fix than completely refactoring lvalue representations to carry a canonical form or whatnot. A simpler implementation for...

A remark from Zulip on optimizing the pairwise may alias checking. Checking all pairs is overly wasteful because addresses may only alias if their `varinfo`s (without `offset`s) are equal, so...

When I did SV-COMP performance comparisons for #770, I actually saw 5 unsound tasks, including the ones you listed above: https://goblint.cs.ut.ee/results/72-all-fast-evalint-opt-after/table-generator.table.html#/table?filter=0(0*status*(category(in(wrong)))). Have you not seen the others in your recent...

Right now these two are the only two unsoundness cases that haven't been dealt with AFAIK. Are you still planning to look into these?

I did an sv-benchmarks run with this for good measure. That single benchmark went from `ASSERTION` to `TIMEOUT`, but at least there's no regression to results or performance.