Add primitive verdict-based YAML violation witness rejection
Closes #1301.
Most of this is just adding YAML witness violation_sequence parsing support and adapting the parsing of locations in YAML witnesses to allow for fields which the updated 2.0 format allows to omit.
The actual rejection part is laughably trivial: do nothing!
- If program is correct and we can prove it, we output
true, which counts as refutation of violation witness. - If program is correct and we cannot prove it, we output
unknown. - If program is incorrect, we output
unknown.
Actually using any of the information in the violation sequence is a separate issue. We should be able to kill some paths or refine some values based on that, a la (linear) observer automaton.
TODO
- [x] Add some tests.
I tried running this on SV-COMP 2024 YAML violation witnesses (it's extremely difficult to even get them). If I did everything correctly, there are at most 160 (probably even much fewer) tasks with expected true verdict. Among them, only two of CPAchecker's we terminate with unknown. So we cannot reject anything.
Also doing some refinement with violation sequences might allow us to reject witnesses even for tasks with expected verdict false, if the error path cannot lead to the violation. But I'm not very hopeful about that.