Add test for model-checking#1823

tests/perf/misc/array_fold/Cargo.toml

@@ -0,0 +1,11 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+[package]
+name = "array_fold"
+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/misc/array_fold/expected

@@ -0,0 +1 @@
+Complete - 0 successfully verified harnesses, 2 failures, 2 total.

tests/perf/misc/array_fold/src/main.rs

@@ -0,0 +1,34 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! This test checks the performance of fold, which uses iterators under the
+//! hood.
+//! The test is from https://github.com/model-checking/kani/issues/1823.
+//! Pre CBMC 5.72.0, it took ~36 seconds and consumed ~3.6 GB of memory.
+//! With CBMC 5.72.0, it takes ~11 seconds and consumes ~255 MB of memory.
+
+pub fn array_sum_fold(x : [usize; 100]) -> usize {
+    x.iter().fold(0, |accumulator, current| accumulator + current)
+}
+
+pub fn array_sum_for(x : [usize; 100]) -> usize {
+    let mut accumulator : usize = 0;
+    for i in 0..100 {
+      accumulator = x[i] + accumulator
+    }
+    accumulator
+}
+
+#[kani::proof]
+fn array_sum_fold_proof() {
+    let x: [usize; 100] = kani::any();
+    array_sum_fold(x);
+}
+
+#[kani::proof]
+fn array_sum_for_proof() {
+    let x: [usize; 100] = kani::any();
+    array_sum_for(x);
+}
+
+fn main() {}