Hi,

This is to probe a discussion on the handling of unsound flags and arguments to cbmc
and assorted tools going forward.

To that effect I have drafted a PR (#6479) which is issuing a warning in cbmc and goto-instrument
if the user has enabled any of the known unsound flags either directly or indirectly.

This may or may not be fine as a temporary solution (hence why it's a draft PR) but long
term there needs to be different handling of it. At the moment I'm unsure if the unsound options
are resolved if say some associated bugs (like in #6394) are resolved - actually, I'm unsure
about the extend of unsoundness that these options entail in general.

I'm open to modifying/closing that draft PR if further investigation (I'm planning to deal with #6394 as
a next step) shows that these issues are transient and really are just a manifestation of one bug, and
then fixing that restores soundness (as an example).

But there's a lot of uncertainty surrounding that from my end, hence why I'd like to solicit
some advise from the community. There has been some discussion already about this in #6397, but
this RFC is about converging on an acceptable solution for the long term handling of issues like these.

I'd appreciate your input 👍🏻