diff --git a/.github/workflows/cargo-update.yml b/.github/workflows/cargo-update.yml
index ef2d8847d527..d8bd170d1821 100644
--- a/.github/workflows/cargo-update.yml
+++ b/.github/workflows/cargo-update.yml
@@ -37,7 +37,7 @@ jobs:
             git diff
           fi
       - name: Create Pull Request
-        uses: peter-evans/create-pull-request@v5
+        uses: peter-evans/create-pull-request@v6
         with:
           commit-message: Upgrade cargo dependencies to ${{ env.today }}
           branch: cargo-update-${{ env.today }}
diff --git a/.github/workflows/cbmc-update.yml b/.github/workflows/cbmc-update.yml
index e5f33e935e09..74d9caeb0fcf 100644
--- a/.github/workflows/cbmc-update.yml
+++ b/.github/workflows/cbmc-update.yml
@@ -63,7 +63,7 @@ jobs:
 
       - name: Create Pull Request
         if: ${{ env.next_step == 'create_pr' }}
-        uses: peter-evans/create-pull-request@v5
+        uses: peter-evans/create-pull-request@v6
         with:
           commit-message: Upgrade CBMC from ${{ env.CBMC_VERSION }} to ${{ env.CBMC_LATEST }}
           branch: cbmc-${{ env.CBMC_LATEST }}
diff --git a/.github/workflows/toolchain-upgrade.yml b/.github/workflows/toolchain-upgrade.yml
index 32266375cb5f..8252bfb826e6 100644
--- a/.github/workflows/toolchain-upgrade.yml
+++ b/.github/workflows/toolchain-upgrade.yml
@@ -68,7 +68,7 @@ jobs:
           fi
       - name: Create Pull Request
         if: ${{ env.next_step == 'create_pr' }}
-        uses: peter-evans/create-pull-request@v5
+        uses: peter-evans/create-pull-request@v6
         with:
           commit-message: Upgrade Rust toolchain to nightly-${{ env.next_toolchain_date }}
           branch: toolchain-${{ env.next_toolchain_date }}
diff --git a/library/kani/src/lib.rs b/library/kani/src/lib.rs
index 865344df4d4b..e3456f69fbb3 100644
--- a/library/kani/src/lib.rs
+++ b/library/kani/src/lib.rs
@@ -288,6 +288,13 @@ macro_rules! cover {
     };
 }
 
+// Used to bind `core::assert` to a different name to avoid possible name conflicts if a
+// crate uses `extern crate std as core`. See
+// https://github.com/model-checking/kani/issues/1949 and https://github.com/model-checking/kani/issues/2187
+#[doc(hidden)]
+#[cfg(not(feature = "concrete_playback"))]
+pub use core::assert as __kani__workaround_core_assert;
+
 // Kani proc macros must be in a separate crate
 pub use kani_macros::*;
 
diff --git a/library/std/src/lib.rs b/library/std/src/lib.rs
index 92ff9216da95..37e0e5a21518 100644
--- a/library/std/src/lib.rs
+++ b/library/std/src/lib.rs
@@ -12,13 +12,6 @@
 // re-export all std symbols
 pub use std::*;
 
-// Bind `core::assert` to a different name to avoid possible name conflicts if a
-// crate uses `extern crate std as core`. See
-// https://github.com/model-checking/kani/issues/1949
-#[cfg(not(feature = "concrete_playback"))]
-#[allow(unused_imports)]
-use core::assert as __kani__workaround_core_assert;
-
 #[cfg(not(feature = "concrete_playback"))]
 // Override process calls with stubs.
 pub mod process;
@@ -64,7 +57,7 @@ macro_rules! assert {
         // strategy, which is tracked in
         // https://github.com/model-checking/kani/issues/692
         if false {
-            __kani__workaround_core_assert!(true, $($arg)+);
+            kani::__kani__workaround_core_assert!(true, $($arg)+);
         }
     }};
 }
@@ -178,7 +171,7 @@ macro_rules! unreachable {
     // handle.
     ($fmt:expr, $($arg:tt)*) => {{
         if false {
-            __kani__workaround_core_assert!(true, $fmt, $($arg)+);
+            kani::__kani__workaround_core_assert!(true, $fmt, $($arg)+);
         }
         kani::panic(concat!("internal error: entered unreachable code: ",
         stringify!($fmt, $($arg)*)))}};
@@ -195,7 +188,7 @@ macro_rules! panic {
     // `panic!("Error message")`
     ($msg:literal $(,)?) => ({
         if false {
-            __kani__workaround_core_assert!(true, $msg);
+            kani::__kani__workaround_core_assert!(true, $msg);
         }
         kani::panic(concat!($msg))
     });
@@ -214,7 +207,7 @@ macro_rules! panic {
     // `panic!("Error: {}", code);`
     ($($arg:tt)+) => {{
         if false {
-            __kani__workaround_core_assert!(true, $($arg)+);
+            kani::__kani__workaround_core_assert!(true, $($arg)+);
         }
         kani::panic(stringify!($($arg)+));
     }};
diff --git a/tests/cargo-kani/no_std/Cargo.toml b/tests/cargo-kani/no_std/Cargo.toml
deleted file mode 100644
index 10c0b0b681b7..000000000000
--- a/tests/cargo-kani/no_std/Cargo.toml
+++ /dev/null
@@ -1,16 +0,0 @@
-# Copyright Kani Contributors
-# SPDX-License-Identifier: Apache-2.0 OR MIT
-[package]
-name = "no_std"
-version = "0.1.0"
-edition = "2021"
-
-# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
-
-[dependencies]
-
-[features]
-std = []
-
-[package.metadata.kani.flags]
-features = ["std"]
diff --git a/tests/cargo-kani/no_std/foo.expected b/tests/cargo-kani/no_std/foo.expected
deleted file mode 100644
index 7f5175082667..000000000000
--- a/tests/cargo-kani/no_std/foo.expected
+++ /dev/null
@@ -1 +0,0 @@
-error: cannot find macro `__kani__workaround_core_assert` in this scope
diff --git a/tests/cargo-kani/no_std/src/main.rs b/tests/cargo-kani/no_std/src/main.rs
deleted file mode 100644
index 0a2bff90fbd8..000000000000
--- a/tests/cargo-kani/no_std/src/main.rs
+++ /dev/null
@@ -1,20 +0,0 @@
-// Copyright Kani Contributors
-// SPDX-License-Identifier: Apache-2.0 OR MIT
-
-//! This test checks that Kani handles assert in no_std environment which
-//! currently doesn't work:
-//! https://github.com/model-checking/kani/issues/2187)
-
-#![no_std]
-
-#[cfg(feature = "std")]
-extern crate std;
-
-#[kani::proof]
-fn foo() {
-    let x: i32 = kani::any();
-    let y = 0;
-    std::debug_assert!(x + y == x, "Message");
-}
-
-fn main() {}
diff --git a/tests/ui/extern_std/macro_override.expected b/tests/ui/extern_std/macro_override.expected
new file mode 100644
index 000000000000..feacbd7b5be6
--- /dev/null
+++ b/tests/ui/extern_std/macro_override.expected
@@ -0,0 +1,15 @@
+Checking harness foo...
+
+Status: SUCCESS\
+Description: ""debug_assert""\
+macro_override.rs:
+
+Status: SUCCESS\
+Description: "panic"\
+macro_override.rs:
+
+Status: SUCCESS\
+Description: "internal error: entered unreachable code: unreachable"\
+macro_override.rs:
+
+Complete - 1 successfully verified harnesses, 0 failures, 1 total.
diff --git a/tests/ui/extern_std/macro_override.rs b/tests/ui/extern_std/macro_override.rs
new file mode 100644
index 000000000000..b53bff757f26
--- /dev/null
+++ b/tests/ui/extern_std/macro_override.rs
@@ -0,0 +1,22 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Test if Kani can correctly identify assertions in a no_std crate that re-exports `std` library.
+//! Issue previously reported here: <https://github.com/model-checking/kani/issues/2187>
+//
+// compile-flags: --cfg=feature="std"
+#![no_std]
+
+#[cfg(feature = "std")]
+extern crate std;
+
+#[kani::proof]
+fn foo() {
+    std::debug_assert!(true, "debug_assert");
+    if kani::any_where(|b| !b) {
+        std::unreachable!("unreachable")
+    }
+    if kani::any_where(|val: &u8| *val > 10) < 10 {
+        std::panic!("panic")
+    }
+}