YAML witnesses containing entries with different versions in SV-COMP 2026

[sim642]

In SV-COMP 2026 (first) final result, we have a witness invalid (true) verdict for five tasks:

• goblint-coreutils/instrumented_cksum_comb
• goblint-coreutils/instrumented_cut_comb
• goblint-coreutils/instrumented_interval_cksum_comb
• goblint-coreutils/instrumented_interval_nohup_comb
• goblint-coreutils/instrumented_nohup_comb

The error from witnesslint is:

CRITICAL: The given YAML witness contains entries with different format versions.
Running witnesslint version 2.1.2

I think what happens in these programs is that they do something which causes Goblint to go into multi-threaded mode without actually creating threads (e.g. registering signal handlers). In that case, we end up generating YAML witnesses with ghost_instrumentation (version 2.1), but an invariant_set (version 2.0).

Ideally, we would just have a less crude analysis of those constructs, but the witnesses should be consistent and pass witnesslint regardless.