diff --git a/bitcoin/src/pow.rs b/bitcoin/src/pow.rs
index ad38dd86..7af2bb61 100644
--- a/bitcoin/src/pow.rs
+++ b/bitcoin/src/pow.rs
@@ -1742,11 +1742,12 @@ mod verification {
         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]
     fn check_div_rem() {
         let x: 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);
     }