File tree Expand file tree Collapse file tree 1 file changed +2
-1
lines changed Expand file tree Collapse file tree 1 file changed +2
-1
lines changed Original file line number Diff line number Diff line change @@ -341,7 +341,8 @@ impl Layout {
341
341
/// On arithmetic overflow, returns `LayoutError`.
342
342
#[ unstable( feature = "alloc_layout_extra" , issue = "55724" ) ]
343
343
#[ inline]
344
- #[ ensures( |result| result. is_err( ) || n == 0 || result. as_ref( ) . unwrap( ) . 0 . size( ) % n == 0 ) ]
344
+ // the below modulo operation might be too costly to prove
345
+ // #[ensures(|result| result.is_err() || n == 0 || result.as_ref().unwrap().0.size() % n == 0)]
345
346
#[ ensures( |result| result. is_err( ) || n == 0 || result. as_ref( ) . unwrap( ) . 0 . size( ) >= self . size( ) ) ]
346
347
// the below multiplication might be too costly to prove at this time
347
348
// #[ensures(|result| result.is_err() || result.as_ref().unwrap().0.size() == n * result.as_ref().unwrap().1)]
You can’t perform that action at this time.
0 commit comments