The sv-benchmarks results (with 60s timeout) indicate some changes to verdicts:

• 32 tasks go from unknown to true thanks to the more precise bounds we use for ILP32.
• 56 tasks go from true to unknown which are all cases of previous unsoundness: we assumed larger type bounds for some no-overflow tasks than they actually have and were simply lucky to still have sound verdicts.
• 55 tasks go from true to EXCEPTION (IntDomain.IncompatibleIKinds) which for some reason all are valid-memsafety tasks.

I think we should investigate the 55 new EXCEPTION (IntDomain.IncompatibleIKinds exceptions before merging, while we still have an idea of what could be the case.

Also, when this is addressed, I think it makes sense to do a full ressource run the state before this and after it on server01 here before merging. I can start it if you ping me.

I just made a fix ea2f616 which fixes one of those. I'm doing another quick run to see if that covers all of them.
EDIT: It fixes all those cases, so you can try a full resources run @michael-schwarz.

The runs for the context gas values are now finished, I just started the comparison run on the current master (approx 24h), and will then start the run with this after.

In the meantime, there seems to be some problems with OS X left here.

The comparison run I started yesterday has finished this morning, I Just started https://github.com/goblint/analyzer/tree/staging_machdep-arch now.

For now I disabled the test on MacOS. But I also added error messages about the missing machine definition. At least it's still possible to do SV-COMP runs on MacOS for ILP32 tasks but there will be a clear message about the possible unsoundness. The alternative would be to just crash when the machdep is missing, but that might be too harsh and inconvenient (because -m64 probably also doesn't work).

In the future we might want to provide pre-generated machdeps in CIL (at least for type sizes if not all machdep components). That should be enough for SV-COMP where preprocessing isn't needed.