Proposed change:
It might make sense to add a simple heuristic to determine the order in which we codegen harnesses.

Motivation:
When working on #4236, I noticed that the main compiler thread would sometimes get unlucky and try to codegen a very large harness last, meaning it would be done with all its work but have to wait on a worker thread to export a large goto file. Although the effect isn't all that large, it could be avoided if we did codegen for large harnesses first, so that the thread pool has a longer amount of time to write them to disk off the critical path of compilation.

The plot below (of kani-compiler threads' CPU usage over time) shows an example of this situation.