Removed kani assumes removed from proof_for_contract

model-checking · Oct 8, 2024 · 21ae29e · 21ae29e
1 parent daf1576
commit 21ae29e
Showing 1 changed file with 0 additions and 3 deletions.
diff --git a/library/core/src/num/nonzero.rs b/library/core/src/num/nonzero.rs
@@ -2213,9 +2213,6 @@ nonzero_integer! {
 fn nonzero_check_new_unchecked() {
     let x: i32 = kani::any();  // Generates a symbolic value of type i32
 
-    // Only proceed if x is not zero, because passing zero would violate the precondition
-    kani::assume(x != 0);
-
     unsafe {
         let _ = NonZeroI32::new_unchecked(x);  // Calls NonZero::new_unchecked
         }