Currently our SV-COMP validator returns ERROR (Failure) whenever the witness file is missing. This is quite ugly because it's very non-informative and could include other failwith cases which are indistinguishable.
This PR changes the verdict to ERROR (witness missing) in such cases.
It also refactors the passing of YAML witness validation to the SV-COMP result printing to be explicit rather than go through global variables.
TODO
[x] Also do it for unassume analysis somehow.
[x] Check witness existence before doing the whole analysis?
Currently our SV-COMP validator returns
ERROR (Failure)whenever the witness file is missing. This is quite ugly because it's very non-informative and could include otherfailwithcases which are indistinguishable.This PR changes the verdict to
ERROR (witness missing)in such cases. It also refactors the passing of YAML witness validation to the SV-COMP result printing to be explicit rather than go through global variables.TODO