Add test for model-checking#1226

tests/perf/vec/vec/Cargo.toml

@@ -0,0 +1,11 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+[package]
+name = "vec"
+version = "0.1.0"
+edition = "2021"
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[dependencies]

tests/perf/vec/vec/expected

@@ -0,0 +1,4 @@
+Status: SUCCESS\
+Description: "assertion failed: v2 == vec![1]"
+
+VERIFICATION:- SUCCESSFUL

tests/perf/vec/vec/src/main.rs

@@ -0,0 +1,16 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! This test checks the performance of 2d-vectors
+//! The test is from https://github.com/model-checking/kani/issues/1226.
+//! Pre CBMC 5.72.0, it ran out of memory.
+//! With CBMC 5.72.0, it takes ~2 seconds and consumes a few hundred MB of memory.
+
+#[kani::proof]
+#[kani::unwind(5)]
+fn main() {
+    let v1: Vec<Vec<i32>> = vec![vec![1], vec![]];
+
+    let v2: Vec<i32> = v1.into_iter().flatten().collect();
+    assert_eq!(v2, vec![1]);
+}