Add option witness.yaml.sv-comp-true-only

[sim642]

We used to have the option witness.graphml.unknown for whether to output GraphML correctness witnesses for "unknown" SV-COMP results. This was removed in #1738 along with GraphML witnesses entirely.

At some point I thought that we still had the option and it applied to YAML witnesses. Turns out that's not the case: YAML correctness witnesses are currently just invariant sets (not necessarily tied to correctness). And our implementation of YAML witnesses is also completely independent from SV-COMP support. This has allowed us to use YAML witnesses in various CRAM tests without needing to configure ana.specification to a single SV-COMP property file.

This PR adds the analogous option for YAML witnesses, giving us the possibility to not create too many large YAML witnesses in SV-COMP when they'd be useless anyway.

TODO

• Decide value for svcomp conf going forward.

[jerhard]

Looks good to me!

Decide value for svcomp conf going forward.

The following two questions come to mind:

1. Do the additional witnesses help us with debugging, in case there is something to fix before the final submission of Goblint to SV-Comp? I would assume that it is relatively easy to generate those witnesses ourselves in case we need them and only a few tasks are affected.

2. Do we plan to to do further experiments with witnesses generated by Goblint in SV-COMP 26 and forward for tasks where Goblint does not produce a true verdict?
   @karoliineh may have an opinion on that with her plans on exploiting such witnesses.

If we answer both questions with "no", then we can set the flag to true. It is sensible to not generate files that will not be useful.

[karoliineh]

Do we plan to to do further experiments with witnesses generated by Goblint in SV-COMP 26 and forward for tasks where Goblint does not produce a true verdict?

Currently, I am only looking into well-defined correctness witnesses, i.e., the ones that are defined by SV-COMP rules:

• Correctness witnesses are supported for only two properties in some base categories
• Correctness witness is defined only for programs with a true verdict

It will take well over 2 years until maybe we get some gain from the non-defined witnesses. Further, my opinions are, that at SV-COMP:

1. We should not generate witnesses when our verdict is Unknown.

2. We should definitely disable generating witnesses for properties that do not support correctness witnesses, namely:

• termination (this alone would benefit everyone by shrinking the Zenodo witness packages and make handling them much easier). Ties well to:

Giving us the possibility to not create too many large YAML witnesses in SV-COMP when they'd be useless anyway.

• no-data-race
• valid-memcleanup
• valid-memsafety

3. I'm not sure how easy it would be to disable generating witnesses for the base-category-dependent properties, i.e., tasks of property unreach-call that belong to subcategories: *-Arrays, *-Floats, -Heap, and ConcurrencySafety-, and for no-overflow, base category ConcurrencySafety-*, for which correctness witnesses are also not (yet) supported by the rules. So that might not be a priority right now.

[sim642]

3. I'm not sure how easy it would be to disable generating witnesses for the base-category-dependent properties, i.e., tasks of property unreach-call that belong to subcategories: *-Arrays, -Floats, _-Heap, and ConcurrencySafety-__, and for no-overflow, base category _ConcurrencySafety-, for which correctness witnesses are also not (yet) supported by the rules. So that might not be a priority right now.

It is actually against SV-COMP rules to even do that:

There is one global set of parameters that can be used to tune the verifier to the benchmark programs. Verifiers are forbidden from using the program name, its hash, or the current category to tune their parameters.

The exclusion only means that having the witnesses validated is not required to score points, but it doesn't mean that tools shouldn't produce witnesses in those excluded subcategories. Without fingerprinting tasks, it's actually not even possible to not produce witnesses in those subcategories.