I tried the code inside tests/cargo-kani/dependencies using the following command line invocation:

cargo kani --function check_dummy
cargo kani --function check_dummy

with Kani version:

I expected to see this happen: explanation

Compilation should only execute once. In the second case, only CBMC should execute.

Instead, this happened: Cargo compiles the project and its dependencies every time we execute cargo kani.