Since kani relies on pinned toolchain for analyzing Rust code through rustc, is it a good practice to run cargo +1.76 kani when you're using incompatible toolchain?
Why not just run cargo +nightly-xxxx-xx-xx kani where nightly-xxxx-xx-xx is required by kani?

This was motivated by running Kani in an existing repo with an old rust-toolchain.toml and getting a very obscure error that took several hours to track down - +1.76 is just for ease of testing.
I also experimented with trying to translate old-format IDs to new-format, but given that the format is unspecified I'm not confident in being able to write a reliable solution there

I think cargo +nightly-xxxx-xx-xx kani is more reliable, because

• +nightly-xxxx-xx-xx is precedent to rust-toolchain.toml by rustup
• you'll need nightly-xxxx-xx-xx toolchain anyways to make kani really work to do analysis

Unless I'm mistaken, Kani always uses its linked nightly-xxxx toolchain (unless built in a dev environment) for everything else - this fixes the inconsistency here by also using it for cargo metadata, which was a bit of a beginner papercut when trying to use the tool initially

Thanks for the PR! This cargo +1.76 kani invocation pattern is not something we'd like to support--for a given version of Kani, we only support it working with its rust-toolchain.toml version. I worry that this PR will lead users into thinking that Kani is accepting their 1.76 override, which IMO is more confusing than just failing loudly when they try to override the toolchain. One thing we could do is try to detect if someone is overriding the toolchain version and error with a message about that, since I agree that the current cargo metadata related error message is quite obscure.

I'm curious about this comment:

This was motivated by running Kani in an existing repo with an old rust-toolchain.toml and getting a very obscure error that took several hours to track down - +1.76 is just for ease of testing.

Can you post a follow up in #3967 elaborating more on what happened here? You should be able to invoke Kani in a repo that has a different rust-toolchain.toml file. If there are papercuts with using the tool, we would very much like to know about them (and fix them).

I'm going to close this PR, but please do follow up in #3967 if you have the bandwidth--if something took hours of debugging, we would like to improve on that.