Update the .out files

AeneasVerif · Jan 17, 2025 · 4094caa · 4094caa
1 parent ba2cc36
commit 4094caa
Showing 1 changed file with 17 additions and 20 deletions.
diff --git a/charon/tests/ui/issue-297-cfg.out b/charon/tests/ui/issue-297-cfg.out
@@ -1,6 +1,6 @@
 # Final LLBC before serialization:
 
-fn test_crate::f<'_0>(@1: &'_0 (Slice<u8>)) -> usize
+fn test_crate::f1<'_0>(@1: &'_0 (Slice<u8>)) -> usize
 {
     let @0: usize; // return
     let a@1: &'_ (Slice<u8>); // arg #1
@@ -125,9 +125,8 @@ trait core::num::nonzero::ZeroablePrimitive<Self>
     parent_clause0 : [@TraitClause0]: core::marker::Sized<Self>
     parent_clause1 : [@TraitClause1]: core::marker::Copy<Self>
     parent_clause2 : [@TraitClause2]: core::num::nonzero::private::Sealed<Self>
-    parent_clause3 : [@TraitClause3]: core::marker::Copy<Self::NonZeroInner>
-    parent_clause4 : [@TraitClause4]: core::clone::Clone<Self::NonZeroInner>
-    parent_clause5 : [@TraitClause5]: core::marker::Sized<Self::NonZeroInner>
+    parent_clause3 : [@TraitClause3]: core::marker::Sized<Self::NonZeroInner>
+    parent_clause4 : [@TraitClause4]: core::marker::Copy<Self::NonZeroInner>
     type NonZeroInner
 }
 
@@ -171,9 +170,8 @@ impl core::num::nonzero::{impl core::num::nonzero::ZeroablePrimitive for usize}#
     parent_clause0 = core::marker::Sized<usize>
     parent_clause1 = core::marker::{impl core::marker::Copy for usize}#37
     parent_clause2 = core::num::nonzero::{impl core::num::nonzero::private::Sealed for usize}#25
-    parent_clause3 = core::num::nonzero::private::{impl core::marker::Copy for core::num::nonzero::private::NonZeroUsizeInner}#27
-    parent_clause4 = core::num::nonzero::private::{impl core::clone::Clone for core::num::nonzero::private::NonZeroUsizeInner}#26
-    parent_clause5 = core::marker::Sized<core::num::nonzero::private::NonZeroUsizeInner>
+    parent_clause3 = core::marker::Sized<core::num::nonzero::private::NonZeroUsizeInner>
+    parent_clause4 = core::num::nonzero::private::{impl core::marker::Copy for core::num::nonzero::private::NonZeroUsizeInner}#27
     type NonZeroInner = core::num::nonzero::private::NonZeroUsizeInner
 }
 
@@ -295,13 +293,12 @@ trait core::ops::try_trait::Try<Self>
 
 trait core::ops::try_trait::Residual<Self, O>
 where
-    Self::parent_clause1::Residual = Self,
-    Self::parent_clause1::Output = O,
+    Self::parent_clause2::Output = O,
+    Self::parent_clause2::Residual = Self,
 {
     parent_clause0 : [@TraitClause0]: core::marker::Sized<O>
-    parent_clause1 : [@TraitClause1]: core::ops::try_trait::Try<Self::TryType>
-    parent_clause2 : [@TraitClause2]: core::ops::try_trait::FromResidual<Self::TryType, Self>
-    parent_clause3 : [@TraitClause3]: core::marker::Sized<Self::TryType>
+    parent_clause1 : [@TraitClause1]: core::marker::Sized<Self::TryType>
+    parent_clause2 : [@TraitClause2]: core::ops::try_trait::Try<Self::TryType>
     type TryType
 }
 
@@ -450,11 +447,11 @@ trait core::iter::traits::iterator::Iterator<Self>
 
 trait core::iter::traits::collect::IntoIterator<Self>
 where
-    Self::parent_clause1::Item = Self::Item,
+    Self::parent_clause2::Item = Self::Item,
 {
     parent_clause0 : [@TraitClause0]: core::marker::Sized<Self::Item>
-    parent_clause1 : [@TraitClause1]: core::iter::traits::iterator::Iterator<Self::IntoIter>
-    parent_clause2 : [@TraitClause2]: core::marker::Sized<Self::IntoIter>
+    parent_clause1 : [@TraitClause1]: core::marker::Sized<Self::IntoIter>
+    parent_clause2 : [@TraitClause2]: core::iter::traits::iterator::Iterator<Self::IntoIter>
     type Item
     type IntoIter
     fn into_iter = core::iter::traits::collect::IntoIterator::into_iter<Self>
@@ -599,7 +596,7 @@ where
     fn __iterator_get_unchecked<'_0> = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Chunks<'a, T>[@TraitClause0]}#71::__iterator_get_unchecked<'a, '_0_0, T>[@TraitClause0]
 }
 
-fn test_crate::rej_sample<'_0, '_1>(@1: &'_0 (Slice<u8>), @2: &'_1 mut (Slice<i16>)) -> usize
+fn test_crate::f2<'_0, '_1>(@1: &'_0 (Slice<u8>), @2: &'_1 mut (Slice<i16>)) -> usize
 {
     let @0: usize; // return
     let a@1: &'_ (Slice<u8>); // arg #1
@@ -835,8 +832,8 @@ where
     [@TraitClause1]: core::iter::traits::iterator::Iterator<I>,
 {
     parent_clause0 = @TraitClause1::parent_clause0
-    parent_clause1 = @TraitClause1
-    parent_clause2 = @TraitClause0
+    parent_clause1 = @TraitClause0
+    parent_clause2 = @TraitClause1
     type Item = @TraitClause1::Item
     type IntoIter = I
     fn into_iter = core::iter::traits::collect::{impl core::iter::traits::collect::IntoIterator for I}#1::into_iter<I>[@TraitClause0, @TraitClause1]
@@ -866,14 +863,14 @@ fn core::iter::traits::iterator::Iterator::step_by<Self>(@1: Self, @2: usize) ->
 where
     [@TraitClause0]: core::marker::Sized<Self>,
 
-fn core::iter::traits::iterator::Iterator::chain<Self, U>(@1: Self, @2: U) -> core::iter::adapters::chain::Chain<Self, @TraitClause2::IntoIter>[@TraitClause1, @TraitClause2::parent_clause2]
+fn core::iter::traits::iterator::Iterator::chain<Self, U>(@1: Self, @2: U) -> core::iter::adapters::chain::Chain<Self, @TraitClause2::IntoIter>[@TraitClause1, @TraitClause2::parent_clause1]
 where
     [@TraitClause0]: core::marker::Sized<U>,
     [@TraitClause1]: core::marker::Sized<Self>,
     [@TraitClause2]: core::iter::traits::collect::IntoIterator<U>,
     @TraitClause2::Item = Self::Item,
 
-fn core::iter::traits::iterator::Iterator::zip<Self, U>(@1: Self, @2: U) -> core::iter::adapters::zip::Zip<Self, @TraitClause2::IntoIter>[@TraitClause1, @TraitClause2::parent_clause2]
+fn core::iter::traits::iterator::Iterator::zip<Self, U>(@1: Self, @2: U) -> core::iter::adapters::zip::Zip<Self, @TraitClause2::IntoIter>[@TraitClause1, @TraitClause2::parent_clause1]
 where
     [@TraitClause0]: core::marker::Sized<U>,
     [@TraitClause1]: core::marker::Sized<Self>,