Rename core::assert to avoid possible conflicts in user crate

library/std/src/lib.rs

@@ -12,6 +12,12 @@
 // 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
+#[allow(unused_imports)]
+use core::assert as __kani__workaround_core_assert;
+
 // Override process calls with stubs.
 pub mod process;
 
@@ -54,7 +60,7 @@ macro_rules! assert {
         // strategy, which is tracked in
         // https://github.com/model-checking/kani/issues/692
         if false {
-            ::core::assert!(true, $($arg)+);
+            __kani__workaround_core_assert!(true, $($arg)+);
         }
     }};
 }
@@ -158,7 +164,7 @@ macro_rules! unreachable {
     // handle.
     ($fmt:expr, $($arg:tt)*) => {{
         if false {
-            ::core::assert!(true, $fmt, $($arg)+);
+            __kani__workaround_core_assert!(true, $fmt, $($arg)+);
         }
         kani::panic(concat!("internal error: entered unreachable code: ",
         stringify!($fmt, $($arg)*)))}};
@@ -190,7 +196,7 @@ macro_rules! panic {
     // `panic!("Error: {}", code);`
     ($($arg:tt)+) => {{
         if false {
-            ::core::assert!(true, $($arg)+);
+            __kani__workaround_core_assert!(true, $($arg)+);
         }
         kani::panic(stringify!($($arg)+));
     }};

tests/kani/Panic/extern_core.rs

@@ -0,0 +1,16 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! This test checks that the panic macro does not cause a "recursion limit
+//! reached" compiler error if the user crate contains an `extern crate std as
+//! core` line (see https://github.com/model-checking/kani/issues/1949)
+
+extern crate std as core;
+
+#[kani::proof]
+fn main() {
+    let x = if kani::any() { 11 } else { 33 };
+    if x < 10 {
+        panic!("x is {}", x);
+    }
+}