Can the "no decreases clause" and "no assigns clause" warnings be at a higher verbosity? #8654
Description
goto-instrument -dfcc commonly produces two warnings when checking loop contracts
No decreases clause provided for loop...
and
No assigns clause provided for loop XXX in file YYY. Set { XXX }...
The first is uninteresting, since the developer is assumed to have omitted the decreases clause on purpose. The second can produce a large volume of largely unintelligable output.
Both tend to clutter on-screen and CI logs that make debugging runs difficult.
Could these messages be promoted to a higher verbosity level so that they do not appear at the default verbosity, but can be re-instated if required?