Arrays with more than 64 elements no longer cause spurious failures (model-checking#4470)

With model-checking#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: model-checking#2416
Resolves: model-checking#4408

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

Author: tautschnig

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);
+}