From cad14b775e9844c321c98c1923d0d9649b9d7207 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 12 Nov 2025 11:30:24 +0000 Subject: [PATCH] Arrays with more than 64 elements no longer cause spurious failures With #4448 merged (upgrade to CBMC 6.8.0) we have the necessary fix in place to avoid spurious failures with arrays that have more than 64 elements. Resolves: #2416 Resolves: #4408 --- tests/kani/Array/array_64.rs | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) create mode 100644 tests/kani/Array/array_64.rs diff --git a/tests/kani/Array/array_64.rs b/tests/kani/Array/array_64.rs new file mode 100644 index 000000000000..f38d5cfe627d --- /dev/null +++ b/tests/kani/Array/array_64.rs @@ -0,0 +1,16 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +//! Check that CBMC (as invoked via Kani) does not spuriously fail with arrays of more 64 elements. + +#[derive(PartialEq, Eq)] +enum Foo { + A, + B([u8; 65]), +} + +#[kani::proof] +fn main() { + let x: Foo = Foo::B([42; 65]); + let y: Foo = Foo::B([42; 65]); + assert!(x == y); +}