From dbe03e4f6daf219aeb0eb9118c466e8d47a2e537 Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Mon, 28 Oct 2024 10:49:00 -0700 Subject: [PATCH] Reduce the number of object bits for refcell test --- .../interior-mutability/whole-struct/refcell.rs | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/tests/expected/function-contract/interior-mutability/whole-struct/refcell.rs b/tests/expected/function-contract/interior-mutability/whole-struct/refcell.rs index 1cce5e2364c3..518c8140ea37 100644 --- a/tests/expected/function-contract/interior-mutability/whole-struct/refcell.rs +++ b/tests/expected/function-contract/interior-mutability/whole-struct/refcell.rs @@ -1,6 +1,8 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: -Zfunction-contracts +// Temporarily reduce the number of object bits till +// https://github.com/model-checking/kani/issues/3611 is fixed +// kani-flags: -Zfunction-contracts --enable-unstable --cbmc-args --object-bits 12 /// The objective of this test is to check the modification of a RefCell used as interior mutability in an immutable struct use std::cell::RefCell;