Kani builds don't enable features the same as ordinary cargo builds

[tedinski]

Many projects use workspaces, with dependencies between crates in the workspace.

A common pattern is to have a feature named something like "test_utilities" that, when enabled, exports more symbols that are generally just for testing and other crates request this feature for their own tests.

When building a workspace, if a crate has any dependents with a feature enabled, then the crate is built in that workspace with the feature enabled, which is what's used for all dependents. This means it's common for one crate to properly ask for "test_utilities" and other crates to forget, because they're accidentally getting it for free.

Kani, however, builds one crate at a time with -p at present, and so we no longer benefit(?) from this behavior, and that means customers trying Kani immediate run into build failures if they have this common misconfiguration problem. It's normally hidden from them.

We shouldn't get in customer's way, if cargo test works, then cargo kani should too. We should fix this.