Allow &bool in asserts

library/std/src/lib.rs

@@ -44,10 +44,11 @@ pub mod process;
 #[macro_export]
 macro_rules! assert {
     ($cond:expr $(,)?) => {
-        kani::assert($cond, concat!("assertion failed: ", stringify!($cond)));
+        // The double negation is to resolve https://github.com/model-checking/kani/issues/2108
+        kani::assert(!!$cond, concat!("assertion failed: ", stringify!($cond)));
     };
     ($cond:expr, $($arg:tt)+) => {{
-        kani::assert($cond, concat!(stringify!($($arg)+)));
+        kani::assert(!!$cond, concat!(stringify!($($arg)+)));
         // Process the arguments of the assert inside an unreachable block. This
         // is to make sure errors in the arguments (e.g. an unknown variable or
         // an argument that does not implement the Display or Debug traits) are

tests/kani/Assert/bool_ref.rs

@@ -0,0 +1,12 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! This test makes sure Kani handles the valid `assert!(&b)` syntax where `b` is a `bool`
+//! See https://github.com/model-checking/kani/issues/2108 for details.
+
+#[kani::proof]
+fn check_assert_with_reg() {
+    let b1: bool = kani::any();
+    let b2 = b1 || !b1; // true
+    assert!(&b2);
+}