add tests for issues 2239 and 2732

tests/expected/issue-2239/issue_2239.expected

@@ -0,0 +1,5 @@
+test_trivial_bounds.unreachable.1\
+- Status: FAILURE\
+- Description: "unreachable code"
+
+VERIFICATION:- FAILED

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() {}

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

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();
+}