Concrete playback instructions don't work if user sets --cfg=kani

[celinval]

I tried the following:

$ cargo init dummy
$ cd dummy

I added the following line to Cargo.toml

[dev-dependencies]
kani = { git = "https://github.com/model-checking/kani", features = ["concrete_playback"] }

I opened src/main.rs

#[cfg(kani)]
mod harnesses {
  #[kani::proof]
  fn force_failure() {
    assert!(kani::any());
  }
}

using the following command line invocation:

cargo kani --enable-unstable --concrete-playback
RUSTFLAGS="--cfg=kani" cargo +nightly test

with Kani version: 0.9.0

I expected to see this happen: Cargo runs the new test and fail.

Instead, this happened: Cargo failed to build the harness with the following error:

error[E0433]: failed to resolve: use of undeclared crate or module `kanitool`
  --> src/main.rs:36:5
   |
36 |     #[kani::proof]
   |     ^^^^^^^^^^^^^^ use of undeclared crate or module `kanitool`
   |
   = note: this error originates in the attribute macro `kani::proof` (in Nightly builds, run with -Z macro-backtrace for more info)

[celinval]

Closed the wrong issue. Sorry!

[celinval]

As @jaisnan and I discussed offline, one solution here would be to add a concrete_playback feature to kani_macros crate the same way we have added to the kani crate.

[celinval]

I think we could even enable it by default and disable it when building our sysroot