From 8f4c07dfcf1420f0a5552092878aa88ee72a7fb3 Mon Sep 17 00:00:00 2001
From: Carolyn Zech <cmzech@amazon.com>
Date: Tue, 3 Sep 2024 09:59:59 -0400
Subject: [PATCH] add test for issue 3022

---
 tests/expected/issue-3022/issue_3022.expected |  5 ++++
 tests/expected/issue-3022/issue_3022.rs       | 24 +++++++++++++++++++
 2 files changed, 29 insertions(+)
 create mode 100644 tests/expected/issue-3022/issue_3022.expected
 create mode 100644 tests/expected/issue-3022/issue_3022.rs

diff --git a/tests/expected/issue-3022/issue_3022.expected b/tests/expected/issue-3022/issue_3022.expected
new file mode 100644
index 000000000000..9600182a5209
--- /dev/null
+++ b/tests/expected/issue-3022/issue_3022.expected
@@ -0,0 +1,5 @@
+main.assertion\
+- Status: SUCCESS\
+- Description: "assertion failed: inner == func2.inner"
+
+VERIFICATION:- SUCCESSFUL
\ No newline at end of file
diff --git a/tests/expected/issue-3022/issue_3022.rs b/tests/expected/issue-3022/issue_3022.rs
new file mode 100644
index 000000000000..6ef6f944395f
--- /dev/null
+++ b/tests/expected/issue-3022/issue_3022.rs
@@ -0,0 +1,24 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+type BuiltIn = for<'a> fn(&str);
+
+struct Function {
+    inner: BuiltIn,
+}
+
+impl Function {
+    fn new(subr: BuiltIn) -> Self {
+        Self { inner: subr }
+    }
+}
+
+fn dummy(_: &str) {}
+
+#[kani::proof]
+fn main() {
+    let func1 = Function::new(dummy);
+    let func2 = Function::new(dummy);
+    let inner: fn(&'static _) -> _ = func1.inner;
+    assert!(inner == func2.inner);
+}