From 817310a3b32085577cfe43a7407334a47680dc0e Mon Sep 17 00:00:00 2001
From: Zyad Hassan <zyadh@amazon.com>
Date: Thu, 25 Aug 2022 23:57:18 -0700
Subject: [PATCH 1/2] Make panic a const function

---
 library/kani/src/lib.rs   |  2 +-
 tests/kani/Panic/const.rs | 16 ++++++++++++++++
 2 files changed, 17 insertions(+), 1 deletion(-)
 create mode 100644 tests/kani/Panic/const.rs

diff --git a/library/kani/src/lib.rs b/library/kani/src/lib.rs
index 151a4f220e27..94266f9f46cd 100644
--- a/library/kani/src/lib.rs
+++ b/library/kani/src/lib.rs
@@ -134,7 +134,7 @@ pub fn expect_fail(_cond: bool, _message: &'static str) {
 #[inline(never)]
 #[rustc_diagnostic_item = "KaniPanic"]
 #[doc(hidden)]
-pub fn panic(message: &'static str) -> ! {
+pub const fn panic(message: &'static str) -> ! {
     panic!("{}", message)
 }
 
diff --git a/tests/kani/Panic/const.rs b/tests/kani/Panic/const.rs
new file mode 100644
index 000000000000..ddffa53d5517
--- /dev/null
+++ b/tests/kani/Panic/const.rs
@@ -0,0 +1,16 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! This test checks that `panic!` can be used in a const fn
+
+const fn my_const_fn() {
+    panic!()
+}
+
+#[kani::proof]
+pub fn check_something() {
+    let x: u8 = if kani::any() { 3 } else { 95 };
+    if x > 100 {
+        my_const_fn();
+    }
+}

From 1591fa4d20829fb03d538ffa1998ce1ff39c3d31 Mon Sep 17 00:00:00 2001
From: Zyad Hassan <zyadh@amazon.com>
Date: Fri, 26 Aug 2022 10:15:35 -0700
Subject: [PATCH 2/2] Make assert const as well

---
 library/kani/src/lib.rs          |  2 +-
 tests/kani/Assert/in_const_fn.rs | 15 +++++++++++++++
 2 files changed, 16 insertions(+), 1 deletion(-)
 create mode 100644 tests/kani/Assert/in_const_fn.rs

diff --git a/library/kani/src/lib.rs b/library/kani/src/lib.rs
index 94266f9f46cd..e4b456431cc0 100644
--- a/library/kani/src/lib.rs
+++ b/library/kani/src/lib.rs
@@ -58,7 +58,7 @@ pub fn assume(_cond: bool) {
 /// ```
 #[inline(never)]
 #[rustc_diagnostic_item = "KaniAssert"]
-pub fn assert(_cond: bool, _msg: &'static str) {
+pub const fn assert(_cond: bool, _msg: &'static str) {
     if cfg!(feature = "concrete_playback") {
         assert!(_cond, "{}", _msg);
     }
diff --git a/tests/kani/Assert/in_const_fn.rs b/tests/kani/Assert/in_const_fn.rs
new file mode 100644
index 000000000000..064a3f869b37
--- /dev/null
+++ b/tests/kani/Assert/in_const_fn.rs
@@ -0,0 +1,15 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! This test checks that `assert!` can be used in a const fn
+
+const fn const_add(x: i32, y: i32) {
+    assert!(x + y == x);
+}
+
+#[kani::proof]
+fn check() {
+    let x = kani::any();
+    let y = 0;
+    const_add(x, y);
+}