diff --git a/library/core/src/alloc/layout.rs b/library/core/src/alloc/layout.rs index 53426be7e6010..9104ab3356713 100644 --- a/library/core/src/alloc/layout.rs +++ b/library/core/src/alloc/layout.rs @@ -341,7 +341,8 @@ impl Layout { /// On arithmetic overflow, returns `LayoutError`. #[unstable(feature = "alloc_layout_extra", issue = "55724")] #[inline] - #[ensures(|result| result.is_err() || n == 0 || result.as_ref().unwrap().0.size() % n == 0)] + // the below modulo operation might be too costly to prove + // #[ensures(|result| result.is_err() || n == 0 || result.as_ref().unwrap().0.size() % n == 0)] #[ensures(|result| result.is_err() || n == 0 || result.as_ref().unwrap().0.size() >= self.size())] // the below multiplication might be too costly to prove at this time // #[ensures(|result| result.is_err() || result.as_ref().unwrap().0.size() == n * result.as_ref().unwrap().1)]