Unless CBMC is invoked with --no-self-loops-to-assumptions, self-loops
are replaced by assumptions. This commit now introduces a status output
that such replacement is happening, and also a warning when
--unwinding-assertions is set: as the loop is replaced by an assumption,
no unwinding assertions can possible be generated. This behaviour may be
unexpected by the user, and we should therefore let them know what is
going on.

Fixes: #6433

• Each commit message has a non-empty body, explaining why the change was made.
• n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
• n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
• Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
• n/a My commit message includes data points confirming performance improvements (if claimed).
• My PR is restricted to a single feature or bugfix.
• n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.