From cc4e6d023f8edf92fea294dcaea2fd5a1132cb47 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Thu, 25 Jul 2024 12:11:48 +0200
Subject: [PATCH] chore: change further solvers in harnesses used with Kani
 (#2284)

CaDiCaL version 1.9.2 and later have a substantially worse performance on some
instances produced by CBMC (via Kani). Use MiniSat to change overall
verification time from over 800 seconds down to 20 (`rx_message_test`) and from
over 80 seconds down to 15 (`round_trip`).
---
 quic/s2n-quic-core/src/packet/number/tests.rs | 2 +-
 quic/s2n-quic-platform/src/message.rs         | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/quic/s2n-quic-core/src/packet/number/tests.rs b/quic/s2n-quic-core/src/packet/number/tests.rs
index ab13d222f9..041aa7e123 100644
--- a/quic/s2n-quic-core/src/packet/number/tests.rs
+++ b/quic/s2n-quic-core/src/packet/number/tests.rs
@@ -10,7 +10,7 @@ use bolero::{check, generator::*};
 use s2n_codec::{testing::encode, DecoderBuffer};
 
 #[test]
-#[cfg_attr(kani, kani::proof, kani::unwind(5), kani::solver(cadical))]
+#[cfg_attr(kani, kani::proof, kani::unwind(5), kani::solver(minisat))]
 fn round_trip() {
     check!()
         .with_generator(
diff --git a/quic/s2n-quic-platform/src/message.rs b/quic/s2n-quic-platform/src/message.rs
index 8de208a793..1e7e58ad53 100644
--- a/quic/s2n-quic-platform/src/message.rs
+++ b/quic/s2n-quic-platform/src/message.rs
@@ -160,7 +160,7 @@ mod tests {
     use bolero::check;
 
     #[test]
-    #[cfg_attr(kani, kani::proof, kani::unwind(17), kani::solver(cadical))]
+    #[cfg_attr(kani, kani::proof, kani::unwind(17), kani::solver(minisat))]
     fn rx_message_test() {
         let path = bolero::gen::<path::RemoteAddress>();
         let ecn = bolero::gen();