UAutomizer rejects witnesses based on their file-endings

[marian-lingsch]

Basic Info

• Version: SV-COMP25

Description

When validating a witness using UAutomizer, it requires that the file ends in .yml in order to be validated. In case this is not the case it outputs Unsupported witness type file-ending

It would be nice if UAutomizer could decide if the witness is supported or not based on the file contents of the file not based on the file ending. Alternatively it would be sufficient if the error message describing what is expected could be improved. Since when there is no file-ending the error message is somewhat confusing, Unsupported witness type $FILE, making it somewhat unclear how to fix the witness in order for it to be valid.

[schuessf]

You are right, the message was not really meaningful, so I tried to improve it.

It would be nice if UAutomizer could decide if the witness is supported or not based on the file contents of the file not based on the file ending.

Even though, we could implement this in our Python wrapper script, we also rely on the file ending internally to decide which parser to use. I don't think it is feasible to change this behaviour.