Wrong clause was caught

Author: tautschnig

library/core/src/alloc/layout.rs

@@ -434,7 +434,10 @@ impl Layout {
     /// On arithmetic overflow, returns `LayoutError`.
     #[unstable(feature = "alloc_layout_extra", issue = "55724")]
     #[inline]
-    #[ensures(|result| result.is_err() || result.as_ref().unwrap().size() == n * self.size())]
+    // the below multiplication might be too costly to prove at this time
+    // #[ensures(|result| result.is_err() || result.as_ref().unwrap().size() == n * self.size())]
+    // use the weaker statement below for now
+    #[ensures(|result| result.is_err() || n == 0 || result.as_ref().unwrap().size() >= self.size())]
     #[ensures(|result| result.is_err() || result.as_ref().unwrap().align() == self.align())]
     pub fn repeat_packed(&self, n: usize) -> Result<Self, LayoutError> {
         let size = self.size().checked_mul(n).ok_or(LayoutError)?;
@@ -450,9 +453,6 @@ impl Layout {
     /// On arithmetic overflow, returns `LayoutError`.
     #[unstable(feature = "alloc_layout_extra", issue = "55724")]
     #[inline]
-    // the below is wrong but was written in a previous commit; keeping it for now to confirm that
-    // this is caught
-    #[ensures(|result| result.is_err() || result.as_ref().unwrap().size() <= next.size())]
     #[ensures(|result| result.is_err() || result.as_ref().unwrap().size() == self.size() + next.size())]
     #[ensures(|result| result.is_err() || result.as_ref().unwrap().align() == self.align())]
     pub fn extend_packed(&self, next: Self) -> Result<Self, LayoutError> {