Merge rust-bitcoin/rust-bitcoin#2454: Remove broken kani test

47569302fc Fix broken kani test (Tobin C. Harding)

Pull request description:

  Recently we added a kani test that doesn't work because of `debug_assert` calls in ops traits.

  Instead of opening the can of worms that is correct panic behaviour in ops lets just remove the test.

ACKs for top commit:
  Kixunil:
    ACK 47569302fc
  apoelstra:
    ACK 47569302fc

Tree-SHA512: f4a862d99173c1502e70fe4c2b9085a1f23dd4501f2ae25dc8a92e3edda7804b42b0580ef32fef2a3d5ea0d98e16b6f0fdba456cf4f0926c5b051ec8a6e54c78
This commit is contained in:
Andrew Poelstra 2024-02-07 15:09:48 +00:00
commit 48dd9842ef
No known key found for this signature in database
GPG Key ID: C588D63CE41B97C1
1 changed files with 2 additions and 1 deletions

View File

@ -1742,11 +1742,12 @@ mod verification {
let _ = x.mul_u64(y); let _ = x.mul_u64(y);
} }
#[kani::unwind(5)] // I can't remember exactly why we need this. #[kani::unwind(5)] // Same as above.
#[kani::proof] #[kani::proof]
fn check_div_rem() { fn check_div_rem() {
let x: U256 = kani::any(); let x: U256 = kani::any();
let y: U256 = kani::any(); let y: U256 = kani::any();
kani::assume(x < U256::from(u128::MAX) && y < U256::from(u128::MAX) && y != U256::ZERO);
assert_eq!(x * y / y, x); assert_eq!(x * y / y, x);
} }