From 2db3d3b037ad7cb1e15510b34a775323d5328580 Mon Sep 17 00:00:00 2001
From: Carolyn Zech <cmzech@amazon.com>
Date: Tue, 3 Sep 2024 10:20:00 -0400
Subject: [PATCH] add tests for issues 2239 and 2732

---
 tests/expected/issue-2239/issue_2239.expected |  5 +++++
 tests/expected/issue-2239/issue_2239.rs       | 12 ++++++++++++
 tests/expected/issue-2732/issue_2732.expected |  5 +++++
 tests/expected/issue-2732/issue_2732.rs       | 11 +++++++++++
 4 files changed, 33 insertions(+)
 create mode 100644 tests/expected/issue-2239/issue_2239.expected
 create mode 100644 tests/expected/issue-2239/issue_2239.rs
 create mode 100644 tests/expected/issue-2732/issue_2732.expected
 create mode 100644 tests/expected/issue-2732/issue_2732.rs

diff --git a/tests/expected/issue-2239/issue_2239.expected b/tests/expected/issue-2239/issue_2239.expected
new file mode 100644
index 000000000000..8bdab0df1862
--- /dev/null
+++ b/tests/expected/issue-2239/issue_2239.expected
@@ -0,0 +1,5 @@
+test_trivial_bounds.unreachable.1\
+- Status: FAILURE\
+- Description: "unreachable code"
+
+VERIFICATION:- FAILED
\ No newline at end of file
diff --git a/tests/expected/issue-2239/issue_2239.rs b/tests/expected/issue-2239/issue_2239.rs
new file mode 100644
index 000000000000..e663b0178c09
--- /dev/null
+++ b/tests/expected/issue-2239/issue_2239.rs
@@ -0,0 +1,12 @@
+#![feature(trivial_bounds)]
+#![allow(unused, trivial_bounds)]
+
+#[kani::proof]
+fn test_trivial_bounds()
+where
+    i32: Iterator,
+{
+    for _ in 2i32 {}
+}
+
+fn main() {}
diff --git a/tests/expected/issue-2732/issue_2732.expected b/tests/expected/issue-2732/issue_2732.expected
new file mode 100644
index 000000000000..ad4c07cd69ff
--- /dev/null
+++ b/tests/expected/issue-2732/issue_2732.expected
@@ -0,0 +1,5 @@
+test.assertion\
+- Status: FAILURE\
+- Description: "index out of bounds: the length is less than or equal to the given index"
+
+VERIFICATION:- FAILED
\ No newline at end of file
diff --git a/tests/expected/issue-2732/issue_2732.rs b/tests/expected/issue-2732/issue_2732.rs
new file mode 100644
index 000000000000..b2ea4c25795e
--- /dev/null
+++ b/tests/expected/issue-2732/issue_2732.rs
@@ -0,0 +1,11 @@
+const C: [u32; 5] = [0; 5];
+
+#[allow(unconditional_panic)]
+fn test() -> u32 {
+    C[10]
+}
+
+#[kani::proof]
+fn main() {
+    test();
+}