From 29fd73615ae0c44aada8a60ea54b7e0920a71431 Mon Sep 17 00:00:00 2001
From: Zyad Hassan <zyadh@amazon.com>
Date: Thu, 15 Feb 2024 13:07:11 -0800
Subject: [PATCH] test(s2n-quic-core): use a smaller length in the Kani test

---
 quic/s2n-quic-core/src/inet/checksum.rs | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

diff --git a/quic/s2n-quic-core/src/inet/checksum.rs b/quic/s2n-quic-core/src/inet/checksum.rs
index ba326d4a23..551c88b97b 100644
--- a/quic/s2n-quic-core/src/inet/checksum.rs
+++ b/quic/s2n-quic-core/src/inet/checksum.rs
@@ -401,13 +401,18 @@ mod tests {
         }
     }
 
+    // Reduce the length to 4 for Kani until
+    // https://github.com/model-checking/kani/issues/3030 is fixed
+    #[cfg(any(kani, miri))]
+    const LEN: usize = if cfg!(kani) { 4 } else { 32 };
+
     /// * Compares the implementation to a port of the C code defined in the RFC
     /// * Ensures partial writes are correctly handled, even if they're not at a 16 bit boundary
     #[test]
-    #[cfg_attr(kani, kani::proof, kani::unwind(17), kani::solver(kissat))]
+    #[cfg_attr(kani, kani::proof, kani::unwind(9), kani::solver(cadical))]
     fn differential() {
         #[cfg(any(kani, miri))]
-        type Bytes = crate::testing::InlineVec<u8, 16>;
+        type Bytes = crate::testing::InlineVec<u8, LEN>;
         #[cfg(not(any(kani, miri)))]
         type Bytes = Vec<u8>;