Skip to content

Commit 29fd736

Browse files
committed
test(s2n-quic-core): use a smaller length in the Kani test
1 parent cf0b40e commit 29fd736

File tree

1 file changed

+7
-2
lines changed

1 file changed

+7
-2
lines changed

quic/s2n-quic-core/src/inet/checksum.rs

+7-2
Original file line numberDiff line numberDiff line change
@@ -401,13 +401,18 @@ mod tests {
401401
}
402402
}
403403

404+
// Reduce the length to 4 for Kani until
405+
// https://github.com/model-checking/kani/issues/3030 is fixed
406+
#[cfg(any(kani, miri))]
407+
const LEN: usize = if cfg!(kani) { 4 } else { 32 };
408+
404409
/// * Compares the implementation to a port of the C code defined in the RFC
405410
/// * Ensures partial writes are correctly handled, even if they're not at a 16 bit boundary
406411
#[test]
407-
#[cfg_attr(kani, kani::proof, kani::unwind(17), kani::solver(kissat))]
412+
#[cfg_attr(kani, kani::proof, kani::unwind(9), kani::solver(cadical))]
408413
fn differential() {
409414
#[cfg(any(kani, miri))]
410-
type Bytes = crate::testing::InlineVec<u8, 16>;
415+
type Bytes = crate::testing::InlineVec<u8, LEN>;
411416
#[cfg(not(any(kani, miri)))]
412417
type Bytes = Vec<u8>;
413418

0 commit comments

Comments
 (0)