chore: selectively change solvers to use with Kani (#2283)

CaDiCaL version 1.9.2 and later have a substantially worse performance
on some instances produced by CBMC (via Kani). Use MiniSat or Kissat
instead to avoid this performance penalty when running proofs with
(future versions of) Kani.

quic/s2n-quic-core/src/slice.rs

@@ -233,7 +233,7 @@ mod tests {
     const LEN: usize = if cfg!(kani) { 2 } else { 32 };
 
     #[test]
-    #[cfg_attr(kani, kani::proof, kani::unwind(5), kani::solver(cadical))]
+    #[cfg_attr(kani, kani::proof, kani::unwind(5), kani::solver(kissat))]
     #[cfg_attr(miri, ignore)] // This test is too expensive for miri to complete in a reasonable amount of time
     fn vectored_copy_fuzz_test() {
         check!()

quic/s2n-quic-platform/src/message/cmsg/tests.rs

@@ -23,7 +23,7 @@ fn aligned_iter(bytes: &[u8], f: impl FnOnce(decode::Iter)) {
 
 /// Ensures the cmsg iterator doesn't crash or segfault
 #[test]
-#[cfg_attr(kani, kani::proof, kani::solver(cadical), kani::unwind(17))]
+#[cfg_attr(kani, kani::proof, kani::solver(minisat), kani::unwind(17))]
 fn iter_test() {
     check!().for_each(|bytes| {
         aligned_iter(bytes, |iter| {
@@ -37,7 +37,7 @@ fn iter_test() {
 
 /// Ensures the `decode::Iter::collect` doesn't crash or segfault
 #[test]
-#[cfg_attr(kani, kani::proof, kani::solver(cadical), kani::unwind(17))]
+#[cfg_attr(kani, kani::proof, kani::solver(minisat), kani::unwind(17))]
 fn collect_test() {
     check!().for_each(|bytes| {
         aligned_iter(bytes, |iter| {
@@ -117,7 +117,7 @@ type Ops = Vec<Op>;
 type Ops = s2n_quic_core::testing::InlineVec<Op, 8>;
 
 #[test]
-#[cfg_attr(kani, kani::proof, kani::solver(cadical), kani::unwind(9))]
+#[cfg_attr(kani, kani::proof, kani::solver(kissat), kani::unwind(9))]
 fn round_trip_test() {
     check!().with_type::<Ops>().for_each(|ops| round_trip(ops));
 }

quic/s2n-quic-platform/src/message/msg/tests.rs

@@ -65,7 +65,7 @@ fn address_inverse_pair_test() {
 #[cfg_attr(
     kani,
     kani::proof,
-    kani::solver(cadical),
+    kani::solver(minisat),
     kani::unwind(65),
     // it's safe to stub out cmsg::decode since the cmsg result isn't actually checked in this particular test
     kani::stub(cmsg::decode::collect, stubs::collect)