From 5f6de6ee3b42ffdc91e9414beb4c119edb81acf1 Mon Sep 17 00:00:00 2001
From: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>
Date: Mon, 9 Sep 2024 13:01:24 -0700
Subject: [PATCH] Reduce object-bits for test to avoid OOM (#3511)

Kani often runs out of memory on
`tests/expected/function-contract/history/stub.rs` when running the
regressions. In particular, `quadruple_harness` consumes over 9 GB of
memory. This PR reduces the object bits for this test to 8 to avoid OOM
issues. This brings down memory usage to ~125 MB.

Before:
```bash
$ /usr/bin/time -v kani -Zfunction-contracts stub.rs --harness quadruple_harness
        Maximum resident set size (kbytes): 9136036
```

After:
```bash
$ /usr/bin/time -v kani -Zfunction-contracts stub.rs --harness quadruple_harness --enable-unstable --cbmc-args --object-bits 8
...
        Maximum resident set size (kbytes): 125172
```

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
---
 tests/expected/function-contract/history/stub.rs | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/tests/expected/function-contract/history/stub.rs b/tests/expected/function-contract/history/stub.rs
index 77c590134f41..ce795bea6990 100644
--- a/tests/expected/function-contract/history/stub.rs
+++ b/tests/expected/function-contract/history/stub.rs
@@ -1,6 +1,8 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: -Zfunction-contracts
+// This test consumes > 9 GB of memory with 16 object bits. Reducing the number
+// of object bits to 8 to avoid running out of memory.
+// kani-flags: -Zfunction-contracts --enable-unstable --cbmc-args --object-bits 8
 
 #[kani::ensures(|result| old(*ptr + *ptr) == *ptr)]
 #[kani::requires(*ptr < 100)]