An RMC run includes multiple stages (codegen, symtab2gb, cbmc, etc.) each of which produces its own output and warning/error messages. It's often daunting to find the relevant pieces of information in the output, for example the results of specific assertions (#477), or whether there were warnings in codegen that may impact soundness (#316), etc. The proposal is to reorganize the output from RMC as follows:

1. The output printed in the terminal (stdout) should be minimal; it should only include an indicator of the progress, e.g. which stage the run is in, the number of codegen'd crates out of the total, how many CBMC checks are solved so far, etc., and a summary at the end that includes the number of warnings/errors from the different stages, and how many checks passed or failed. This would be similar in spirit to the output from cargo test where by default no output is emitted for passing tests. The user should be able to increase the output verbosity via a switch.

2. (Optional) A log file that includes all the detailed output from all stages.

3. A report file (e.g. rmc-report.txt) that includes the verification results organized by category, where categories include user-specified assertions, arithmetic overflow checks, bound checks, etc. Each section should list the specific checks that were done, and the result of each.