Skip to content

Commit

Permalink
chore: change further solvers in harnesses used with Kani (#2284)
Browse files Browse the repository at this point in the history
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`).
  • Loading branch information
tautschnig committed Jul 25, 2024
1 parent 75afd77 commit cc4e6d0
Show file tree
Hide file tree
Showing 2 changed files with 2 additions and 2 deletions.
2 changes: 1 addition & 1 deletion quic/s2n-quic-core/src/packet/number/tests.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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(
Expand Down
2 changes: 1 addition & 1 deletion quic/s2n-quic-platform/src/message.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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();
Expand Down

0 comments on commit cc4e6d0

Please sign in to comment.