Requested feature: Coverage checks are instrumented when using --coverage but these often end up being too frequent or redundant (due to, e.g., compiler optimizations or other procedures). They can definitely convert hard problems into infeasible ones due to the high number checks, we need to investigate how and come up with ways to reduce the number to the minimum if we continue to report along regular verification results. We could also exclude them from dependencies to improve performance.
Use case: Coverage results
Link to relevant documentation (Rust reference, Nomicon, RFC): #2612