Skip to content

Commit 5da586f

Browse files
authored
Improve u16::carrying_mul harness performance (#230)
This harness takes between 22-25 minutes in CI. Change the harnesses's macro to use kissat solver instead, which brings verification time down to ~7 seconds. As an aside, I noticed this problem because the partition 1 runner in #229 is taking ~55 minutes, where the other partitions are taking ~30 minutes. This harness accounts for almost the entire difference. One nice consequence of partitioning verification is that it will make performance issues like this more noticeable. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
1 parent 67e2f1c commit 5da586f

File tree

1 file changed

+1
-0
lines changed

1 file changed

+1
-0
lines changed

Diff for: library/core/src/num/mod.rs

+1
Original file line numberDiff line numberDiff line change
@@ -1759,6 +1759,7 @@ mod verify {
17591759
($type:ty, $wide_type:ty, $($harness_name:ident, $min:expr, $max:expr),+) => {
17601760
$(
17611761
#[kani::proof]
1762+
#[kani::solver(kissat)]
17621763
pub fn $harness_name() {
17631764
let lhs: $type = kani::any::<$type>();
17641765
let rhs: $type = kani::any::<$type>();

0 commit comments

Comments
 (0)