diff --git a/library/core/src/num/mod.rs b/library/core/src/num/mod.rs index 3e47debf38f8f..a5ce315a94506 100644 --- a/library/core/src/num/mod.rs +++ b/library/core/src/num/mod.rs @@ -2191,4 +2191,36 @@ mod verify { usize, checked_f128_to_int_unchecked_usize ); + + // `unchecked_disjoint_bitor` proofs + generate_unchecked_math_harness!( + u8, + unchecked_disjoint_bitor, + checked_unchecked_disjoint_bitor_u8 + ); + generate_unchecked_math_harness!( + u16, + unchecked_disjoint_bitor, + checked_unchecked_disjoint_bitor_u16 + ); + generate_unchecked_math_harness!( + u32, + unchecked_disjoint_bitor, + checked_unchecked_disjoint_bitor_u32 + ); + generate_unchecked_math_harness!( + u64, + unchecked_disjoint_bitor, + checked_unchecked_disjoint_bitor_u64 + ); + generate_unchecked_math_harness!( + u128, + unchecked_disjoint_bitor, + checked_unchecked_disjoint_bitor_u128 + ); + generate_unchecked_math_harness!( + usize, + unchecked_disjoint_bitor, + checked_unchecked_disjoint_bitor_usize + ); }