From d16b42430e2a7170c55531b7d293fc2b9bb1338f Mon Sep 17 00:00:00 2001
From: Zyad Hassan <zyadh@amazon.com>
Date: Thu, 12 Jan 2023 14:30:58 -0800
Subject: [PATCH] Add double negation in assert macro definition

---
 library/std/src/lib.rs        |  5 +++--
 tests/kani/Assert/bool_ref.rs | 12 ++++++++++++
 2 files changed, 15 insertions(+), 2 deletions(-)
 create mode 100644 tests/kani/Assert/bool_ref.rs

diff --git a/library/std/src/lib.rs b/library/std/src/lib.rs
index c0cdf2ae9664..907d98d280a2 100644
--- a/library/std/src/lib.rs
+++ b/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
diff --git a/tests/kani/Assert/bool_ref.rs b/tests/kani/Assert/bool_ref.rs
new file mode 100644
index 000000000000..5a9c005f7681
--- /dev/null
+++ b/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);
+}