diff --git a/docs/src/usage.md b/docs/src/usage.md
index fced7a047804..6f011a599a9b 100644
--- a/docs/src/usage.md
+++ b/docs/src/usage.md
@@ -84,6 +84,7 @@ When Kani builds your code, it does two important things:
 
 1. It sets `cfg(kani)`.
 2. It injects the `kani` crate.
+3. For host crates (crates that your target crate depends on), Kani sets `cfg(kani_host)`.
 
 A proof harness (which you can [learn more about in the tutorial](./kani-tutorial.md)), is a function annotated with `#[kani::proof]` much like a test is annotated with `#[test]`.
 But you may experience a similar problem using Kani as you would with `dev-dependencies`: if you try writing `#[kani::proof]` directly in your code, `cargo build` will fail because it doesn't know what the `kani` crate is.
diff --git a/kani-driver/src/call_cargo.rs b/kani-driver/src/call_cargo.rs
index a1d976d73150..7b57ff4853fc 100644
--- a/kani-driver/src/call_cargo.rs
+++ b/kani-driver/src/call_cargo.rs
@@ -326,10 +326,10 @@ pub fn cargo_config_args() -> Vec<OsString> {
     [
         "--target",
         env!("TARGET"),
-        // Propagate `--cfg=kani` to build scripts.
+        // Propagate `--cfg=kani_host` to build scripts.
         "-Zhost-config",
         "-Ztarget-applies-to-host",
-        "--config=host.rustflags=[\"--cfg=kani\"]",
+        "--config=host.rustflags=[\"--cfg=kani_host\"]",
     ]
     .map(OsString::from)
     .to_vec()
diff --git a/tests/cargo-kani/build-rs-plus-host-with-kani-proofs/README.md b/tests/cargo-kani/build-rs-plus-host-with-kani-proofs/README.md
new file mode 100644
index 000000000000..8b5d0799e11f
--- /dev/null
+++ b/tests/cargo-kani/build-rs-plus-host-with-kani-proofs/README.md
@@ -0,0 +1,10 @@
+This repo contains contains a minimal example that breaks compilation when using [kani](https://github.com/model-checking/kani), where I would expect compilation to work.
+
+Deleting the `binary/build.rs` script makes the compilation work suddenly, despite it being skipped anyways:
+
+```
+binary$ cargo kani -v
+Kani Rust Verifier 0.48.0 (cargo plugin)
+Skipped the following unsupported targets: 'build-script-build'.
+...
+```
diff --git a/tests/cargo-kani/build-rs-plus-host-with-kani-proofs/binary/Cargo.toml b/tests/cargo-kani/build-rs-plus-host-with-kani-proofs/binary/Cargo.toml
new file mode 100644
index 000000000000..fffa04fc9a76
--- /dev/null
+++ b/tests/cargo-kani/build-rs-plus-host-with-kani-proofs/binary/Cargo.toml
@@ -0,0 +1,12 @@
+[package]
+name = "binary"
+version = "0.1.0"
+edition = "2021"
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[dependencies]
+constants = { path = "../constants" }
+
+[build-dependencies]
+constants = { path = "../constants" }
diff --git a/tests/cargo-kani/build-rs-plus-host-with-kani-proofs/binary/build.rs b/tests/cargo-kani/build-rs-plus-host-with-kani-proofs/binary/build.rs
new file mode 100644
index 000000000000..948425cbf0ee
--- /dev/null
+++ b/tests/cargo-kani/build-rs-plus-host-with-kani-proofs/binary/build.rs
@@ -0,0 +1,19 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// From https://github.com/model-checking/kani/issues/3101
+
+use constants::SOME_CONSTANT;
+
+// Having a build script that depends on the constants package
+// breaks kani compilation of that package, when compiling the build script.
+// I assume it's because the build compile does not set cfg(kani) on the constants package dependency.
+
+fn main() {
+    // build.rs changes should trigger rebuild
+    println!("cargo:rerun-if-changed=build.rs");
+
+    // Here we have an assertion that gives us additional compile-time checks.
+    // In reality, here I read a linker script and assert certain properties in relation to constants defined in the constants package.
+    assert_eq!(SOME_CONSTANT, 42);
+}
diff --git a/tests/cargo-kani/build-rs-plus-host-with-kani-proofs/binary/src/main.rs b/tests/cargo-kani/build-rs-plus-host-with-kani-proofs/binary/src/main.rs
new file mode 100644
index 000000000000..975059a5083c
--- /dev/null
+++ b/tests/cargo-kani/build-rs-plus-host-with-kani-proofs/binary/src/main.rs
@@ -0,0 +1,31 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// From https://github.com/model-checking/kani/issues/3101
+
+use constants::SomeStruct;
+
+fn function_that_does_something(b: bool) -> SomeStruct {
+    SomeStruct { some_field: if b { 42 } else { 24 } }
+}
+
+fn main() {
+    println!("The constant is {}", constants::SOME_CONSTANT);
+
+    let some_struct = function_that_does_something(true);
+
+    println!("some_field is {:?}", some_struct.some_field);
+}
+
+#[cfg(kani)]
+mod verification {
+    use super::*;
+
+    #[kani::proof]
+    fn function_never_returns_zero_struct() {
+        let input: bool = kani::any();
+        let output = function_that_does_something(input);
+
+        assert!(output.some_field != 0);
+    }
+}
diff --git a/tests/cargo-kani/build-rs-plus-host-with-kani-proofs/constants/Cargo.toml b/tests/cargo-kani/build-rs-plus-host-with-kani-proofs/constants/Cargo.toml
new file mode 100644
index 000000000000..06d81738ccfc
--- /dev/null
+++ b/tests/cargo-kani/build-rs-plus-host-with-kani-proofs/constants/Cargo.toml
@@ -0,0 +1,8 @@
+[package]
+name = "constants"
+version = "0.1.0"
+edition = "2021"
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[dependencies]
diff --git a/tests/cargo-kani/build-rs-plus-host-with-kani-proofs/constants/src/lib.rs b/tests/cargo-kani/build-rs-plus-host-with-kani-proofs/constants/src/lib.rs
new file mode 100644
index 000000000000..a230ab5d3d65
--- /dev/null
+++ b/tests/cargo-kani/build-rs-plus-host-with-kani-proofs/constants/src/lib.rs
@@ -0,0 +1,27 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// From https://github.com/model-checking/kani/issues/3101
+
+pub const SOME_CONSTANT: u32 = 42;
+
+pub struct SomeStruct {
+    pub some_field: u32,
+}
+
+#[cfg(kani)]
+impl kani::Arbitrary for SomeStruct {
+    fn any() -> Self {
+        SomeStruct { some_field: kani::any() }
+    }
+}
+
+#[cfg(kani)]
+mod verification {
+    use super::*;
+
+    #[kani::proof]
+    fn zero() {
+        assert_ne!(SOME_CONSTANT, 0);
+    }
+}