Requested feature: Generate code on a per-harness basis instead of aggregating the reachable code for all harnesses.
Use case: Improve the verification performance since goto-instrument may not be able to slice some stuff that is actually unreachable. See #1659 for an example on how adding a second harness can interfere with the time of the first.
Link to relevant documentation (Rust reference, Nomicon, RFC):