Skip to content

rule change: exclude NoDataRace from violation witness validation

Dominik Klumpp requested to merge ultimate-pa/bench-defs:no-datarace-violation-witnesses into main

There is currently no agreed-upon format for violation witnesses wrt. the no-data-race property (see issue 1216 at sv-benchmarks), and there do not exist any validators.

Thus it was agreed in the community meeting on Nov 7th 2023 (see minutes) that the NoDataRace category is excluded from violation witness validation. The intention is that this change is only for SV-COMP 2024. By SV-COMP 2025, there should be validator support for this property.

Merge request reports