From b504445a71210b22cecd7f1be42fd7461317958d Mon Sep 17 00:00:00 2001
From: Zyad Hassan <zyadh@amazon.com>
Date: Thu, 8 Dec 2022 11:34:28 -0800
Subject: [PATCH] Add test for #1823

---
 tests/perf/misc/array_fold/Cargo.toml  | 11 +++++++++
 tests/perf/misc/array_fold/expected    |  1 +
 tests/perf/misc/array_fold/src/main.rs | 34 ++++++++++++++++++++++++++
 3 files changed, 46 insertions(+)
 create mode 100644 tests/perf/misc/array_fold/Cargo.toml
 create mode 100644 tests/perf/misc/array_fold/expected
 create mode 100644 tests/perf/misc/array_fold/src/main.rs

diff --git a/tests/perf/misc/array_fold/Cargo.toml b/tests/perf/misc/array_fold/Cargo.toml
new file mode 100644
index 000000000000..673b7681e0c7
--- /dev/null
+++ b/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]
diff --git a/tests/perf/misc/array_fold/expected b/tests/perf/misc/array_fold/expected
new file mode 100644
index 000000000000..643fbd2317ec
--- /dev/null
+++ b/tests/perf/misc/array_fold/expected
@@ -0,0 +1 @@
+Complete - 0 successfully verified harnesses, 2 failures, 2 total.
diff --git a/tests/perf/misc/array_fold/src/main.rs b/tests/perf/misc/array_fold/src/main.rs
new file mode 100644
index 000000000000..62eeba9864db
--- /dev/null
+++ b/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() {}