Allow assert with custom message to be used in const contexts (#1858)

Author: zhassan-aws

library/std/src/lib.rs

@@ -54,7 +54,7 @@ macro_rules! assert {
         // strategy, which is tracked in
         // https://github.com/model-checking/kani/issues/692
         if false {
-            let _ = format_args!($($arg)+);
+            ::std::panic!($($arg)+);
         }
     }};
 }

tests/kani/Assert/in_const_fn_args.rs

@@ -0,0 +1,16 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! This test checks that `assert!` with a custom message can be used in a const
+//! fn
+
+const fn const_add(x: i32, y: i32) {
+    assert!(x + y == x, "some message");
+}
+
+#[kani::proof]
+fn check() {
+    let x = kani::any();
+    let y = 0;
+    const_add(x, y);
+}