From 984847cd30df6a1a8f89d72bd52ac10c3e7da196 Mon Sep 17 00:00:00 2001 From: arnaudgolfouse Date: Wed, 4 Dec 2024 14:19:00 +0100 Subject: [PATCH] Update tests --- .../creusot-contracts/creusot-contracts.coma | 252 ++++++++++++------ .../creusot-contracts/why3session.xml | 15 ++ .../creusot-contracts/why3shapes.gz | Bin 25522 -> 25609 bytes creusot/tests/should_fail/bug/878.coma | 4 +- creusot/tests/should_fail/bug/specialize.coma | 4 +- .../should_succeed/bug/final_borrows.coma | 4 +- creusot/tests/should_succeed/hashmap.coma | 8 +- .../should_succeed/heapsort_generic.coma | 4 +- creusot/tests/should_succeed/hillel.coma | 8 +- .../should_succeed/iterators/02_iter_mut.coma | 16 +- .../iterators/03_std_iterators.coma | 8 +- .../should_succeed/iterators/04_skip.coma | 12 +- .../should_succeed/iterators/05_map.coma | 18 +- .../iterators/06_map_precond.coma | 22 +- .../should_succeed/iterators/07_fuse.coma | 4 +- .../iterators/08_collect_extend.coma | 4 +- .../should_succeed/iterators/12_zip.coma | 12 +- .../should_succeed/iterators/13_cloned.coma | 12 +- .../should_succeed/iterators/14_copied.coma | 12 +- .../iterators/15_enumerate.coma | 14 +- creusot/tests/should_succeed/knapsack.coma | 2 +- .../tests/should_succeed/knapsack_full.coma | 2 +- creusot/tests/should_succeed/linked_list.coma | 6 +- .../selection_sort_generic.coma | 2 +- creusot/tests/should_succeed/slices/01.coma | 2 +- .../tests/should_succeed/sparse_array.coma | 8 +- .../tests/should_succeed/take_first_mut.coma | 2 +- .../traits/16_impl_cloning.coma | 2 +- .../type_invariants/vec_inv.coma | 2 +- .../tests/should_succeed/vector/02_gnome.coma | 2 +- .../vector/03_knuth_shuffle.coma | 2 +- .../vector/05_binary_search_generic.coma | 2 +- .../should_succeed/vector/07_read_write.coma | 2 +- .../should_succeed/vector/09_capacity.coma | 4 +- 34 files changed, 285 insertions(+), 188 deletions(-) diff --git a/creusot/tests/creusot-contracts/creusot-contracts.coma b/creusot/tests/creusot-contracts/creusot-contracts.coma index 6b872e7e4..4f8c710c6 100644 --- a/creusot/tests/creusot-contracts/creusot-contracts.coma +++ b/creusot/tests/creusot-contracts/creusot-contracts.coma @@ -1099,7 +1099,7 @@ module M_creusot_contracts__stdqy35z1__iter__cloned__qyi10472681371035856984__pr let%span siter10 = "../../../creusot-contracts/src/std/iter.rs" 46 15 46 32 let%span siter11 = "../../../creusot-contracts/src/std/iter.rs" 47 15 47 32 let%span siter12 = "../../../creusot-contracts/src/std/iter.rs" 48 14 48 42 - let%span sseq13 = "../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95 + let%span sseq13 = "../../../creusot-contracts/src/logic/seq.rs" 620 20 620 95 let%span sboxed14 = "../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18 let%span sinvariant15 = "../../../creusot-contracts/src/invariant.rs" 24 8 24 18 @@ -1149,7 +1149,7 @@ module M_creusot_contracts__stdqy35z1__iter__cloned__qyi10472681371035856984__pr axiom inv_axiom'2 [@rewrite] : forall x : t_T'0 [inv'3 x] . inv'3 x = invariant'1 x - predicate invariant'0 [#"../../../creusot-contracts/src/logic/seq.rs" 610 4 610 30] (self : Seq.seq t_T'0) = + predicate invariant'0 [#"../../../creusot-contracts/src/logic/seq.rs" 619 4 619 30] (self : Seq.seq t_T'0) = [%#sseq13] forall i : int . 0 <= i /\ i < Seq.length self -> inv'3 (Seq.get self i) predicate inv'1 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : Seq.seq t_T'0) @@ -1220,7 +1220,7 @@ module M_creusot_contracts__stdqy35z1__iter__cloned__qyi10472681371035856984__pr let%span siter14 = "../../../creusot-contracts/src/std/iter.rs" 46 15 46 32 let%span siter15 = "../../../creusot-contracts/src/std/iter.rs" 47 15 47 32 let%span siter16 = "../../../creusot-contracts/src/std/iter.rs" 48 14 48 42 - let%span sseq17 = "../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95 + let%span sseq17 = "../../../creusot-contracts/src/logic/seq.rs" 620 20 620 95 let%span sboxed18 = "../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18 let%span sinvariant19 = "../../../creusot-contracts/src/invariant.rs" 24 8 24 18 @@ -1268,7 +1268,7 @@ module M_creusot_contracts__stdqy35z1__iter__cloned__qyi10472681371035856984__pr axiom inv_axiom'2 [@rewrite] : forall x : t_T'0 [inv'3 x] . inv'3 x = invariant'1 x - predicate invariant'0 [#"../../../creusot-contracts/src/logic/seq.rs" 610 4 610 30] (self : Seq.seq t_T'0) = + predicate invariant'0 [#"../../../creusot-contracts/src/logic/seq.rs" 619 4 619 30] (self : Seq.seq t_T'0) = [%#sseq17] forall i : int . 0 <= i /\ i < Seq.length self -> inv'3 (Seq.get self i) predicate inv'1 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : Seq.seq t_T'0) @@ -1348,7 +1348,7 @@ module M_creusot_contracts__stdqy35z1__iter__copied__qyi18224474876607687026__pr let%span siter10 = "../../../creusot-contracts/src/std/iter.rs" 46 15 46 32 let%span siter11 = "../../../creusot-contracts/src/std/iter.rs" 47 15 47 32 let%span siter12 = "../../../creusot-contracts/src/std/iter.rs" 48 14 48 42 - let%span sseq13 = "../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95 + let%span sseq13 = "../../../creusot-contracts/src/logic/seq.rs" 620 20 620 95 let%span sboxed14 = "../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18 let%span sinvariant15 = "../../../creusot-contracts/src/invariant.rs" 24 8 24 18 @@ -1398,7 +1398,7 @@ module M_creusot_contracts__stdqy35z1__iter__copied__qyi18224474876607687026__pr axiom inv_axiom'2 [@rewrite] : forall x : t_T'0 [inv'3 x] . inv'3 x = invariant'1 x - predicate invariant'0 [#"../../../creusot-contracts/src/logic/seq.rs" 610 4 610 30] (self : Seq.seq t_T'0) = + predicate invariant'0 [#"../../../creusot-contracts/src/logic/seq.rs" 619 4 619 30] (self : Seq.seq t_T'0) = [%#sseq13] forall i : int . 0 <= i /\ i < Seq.length self -> inv'3 (Seq.get self i) predicate inv'1 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : Seq.seq t_T'0) @@ -1469,7 +1469,7 @@ module M_creusot_contracts__stdqy35z1__iter__copied__qyi18224474876607687026__pr let%span siter14 = "../../../creusot-contracts/src/std/iter.rs" 46 15 46 32 let%span siter15 = "../../../creusot-contracts/src/std/iter.rs" 47 15 47 32 let%span siter16 = "../../../creusot-contracts/src/std/iter.rs" 48 14 48 42 - let%span sseq17 = "../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95 + let%span sseq17 = "../../../creusot-contracts/src/logic/seq.rs" 620 20 620 95 let%span sboxed18 = "../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18 let%span sinvariant19 = "../../../creusot-contracts/src/invariant.rs" 24 8 24 18 @@ -1517,7 +1517,7 @@ module M_creusot_contracts__stdqy35z1__iter__copied__qyi18224474876607687026__pr axiom inv_axiom'2 [@rewrite] : forall x : t_T'0 [inv'3 x] . inv'3 x = invariant'1 x - predicate invariant'0 [#"../../../creusot-contracts/src/logic/seq.rs" 610 4 610 30] (self : Seq.seq t_T'0) = + predicate invariant'0 [#"../../../creusot-contracts/src/logic/seq.rs" 619 4 619 30] (self : Seq.seq t_T'0) = [%#sseq17] forall i : int . 0 <= i /\ i < Seq.length self -> inv'3 (Seq.get self i) predicate inv'1 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : Seq.seq t_T'0) @@ -1676,7 +1676,7 @@ module M_creusot_contracts__stdqy35z1__iter__enumerate__qyi2718914205750388896__ let%span siter11 = "../../../creusot-contracts/src/std/iter.rs" 46 15 46 32 let%span siter12 = "../../../creusot-contracts/src/std/iter.rs" 47 15 47 32 let%span siter13 = "../../../creusot-contracts/src/std/iter.rs" 48 14 48 42 - let%span sseq14 = "../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95 + let%span sseq14 = "../../../creusot-contracts/src/logic/seq.rs" 620 20 620 95 let%span sboxed15 = "../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18 type t_I'0 @@ -1705,7 +1705,7 @@ module M_creusot_contracts__stdqy35z1__iter__enumerate__qyi2718914205750388896__ axiom inv_axiom'2 [@rewrite] : forall x : t_Item'0 [inv'3 x] . inv'3 x = invariant'2 x - predicate invariant'1 [#"../../../creusot-contracts/src/logic/seq.rs" 610 4 610 30] (self : Seq.seq t_Item'0) = + predicate invariant'1 [#"../../../creusot-contracts/src/logic/seq.rs" 619 4 619 30] (self : Seq.seq t_Item'0) = [%#sseq14] forall i : int . 0 <= i /\ i < Seq.length self -> inv'3 (Seq.get self i) predicate inv'1 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : Seq.seq t_Item'0) @@ -1810,7 +1810,7 @@ module M_creusot_contracts__stdqy35z1__iter__enumerate__qyi2718914205750388896__ let%span siter15 = "../../../creusot-contracts/src/std/iter.rs" 46 15 46 32 let%span siter16 = "../../../creusot-contracts/src/std/iter.rs" 47 15 47 32 let%span siter17 = "../../../creusot-contracts/src/std/iter.rs" 48 14 48 42 - let%span sseq18 = "../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95 + let%span sseq18 = "../../../creusot-contracts/src/logic/seq.rs" 620 20 620 95 let%span sboxed19 = "../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18 type t_I'0 @@ -1839,7 +1839,7 @@ module M_creusot_contracts__stdqy35z1__iter__enumerate__qyi2718914205750388896__ axiom inv_axiom'2 [@rewrite] : forall x : t_Item'0 [inv'3 x] . inv'3 x = invariant'2 x - predicate invariant'1 [#"../../../creusot-contracts/src/logic/seq.rs" 610 4 610 30] (self : Seq.seq t_Item'0) = + predicate invariant'1 [#"../../../creusot-contracts/src/logic/seq.rs" 619 4 619 30] (self : Seq.seq t_Item'0) = [%#sseq18] forall i : int . 0 <= i /\ i < Seq.length self -> inv'3 (Seq.get self i) predicate inv'1 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : Seq.seq t_Item'0) @@ -2463,7 +2463,7 @@ module M_creusot_contracts__stdqy35z1__iter__fuse__qyi7691061398646472980__is_fu let%span sfuse20 = "../../../creusot-contracts/src/std/iter/fuse.rs" 8 14 8 39 let%span sfuse21 = "../../../creusot-contracts/src/std/iter/fuse.rs" 9 14 9 71 let%span sinvariant22 = "../../../creusot-contracts/src/invariant.rs" 34 20 34 44 - let%span sseq23 = "../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95 + let%span sseq23 = "../../../creusot-contracts/src/logic/seq.rs" 620 20 620 95 let%span siter24 = "../../../creusot-contracts/src/std/iter.rs" 38 15 38 24 let%span siter25 = "../../../creusot-contracts/src/std/iter.rs" 39 14 39 45 let%span siter26 = "../../../creusot-contracts/src/std/iter.rs" 43 15 43 21 @@ -2528,7 +2528,7 @@ module M_creusot_contracts__stdqy35z1__iter__fuse__qyi7691061398646472980__is_fu axiom inv_axiom'5 [@rewrite] : forall x : t_Item'0 [inv'5 x] . inv'5 x = invariant'3 x - predicate invariant'1 [#"../../../creusot-contracts/src/logic/seq.rs" 610 4 610 30] (self : Seq.seq t_Item'0) = + predicate invariant'1 [#"../../../creusot-contracts/src/logic/seq.rs" 619 4 619 30] (self : Seq.seq t_Item'0) = [%#sseq23] forall i : int . 0 <= i /\ i < Seq.length self -> inv'5 (Seq.get self i) predicate inv'2 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : Seq.seq t_Item'0) @@ -2643,7 +2643,7 @@ module M_creusot_contracts__stdqy35z1__iter__map__qyi6597778842032428791__produc let%span siter18 = "../../../creusot-contracts/src/std/iter.rs" 46 15 46 32 let%span siter19 = "../../../creusot-contracts/src/std/iter.rs" 47 15 47 32 let%span siter20 = "../../../creusot-contracts/src/std/iter.rs" 48 14 48 42 - let%span sseq21 = "../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95 + let%span sseq21 = "../../../creusot-contracts/src/logic/seq.rs" 620 20 620 95 let%span sboxed22 = "../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18 let%span sinvariant23 = "../../../creusot-contracts/src/invariant.rs" 34 20 34 44 @@ -2733,7 +2733,7 @@ module M_creusot_contracts__stdqy35z1__iter__map__qyi6597778842032428791__produc axiom inv_axiom'3 [@rewrite] : forall x : borrowed t_F'0 [inv'5 x] . inv'5 x = invariant'2 x - predicate invariant'0 [#"../../../creusot-contracts/src/logic/seq.rs" 610 4 610 30] (self : Seq.seq (borrowed t_F'0)) + predicate invariant'0 [#"../../../creusot-contracts/src/logic/seq.rs" 619 4 619 30] (self : Seq.seq (borrowed t_F'0)) = [%#sseq21] forall i : int . 0 <= i /\ i < Seq.length self -> inv'5 (Seq.get self i) @@ -2758,7 +2758,7 @@ module M_creusot_contracts__stdqy35z1__iter__map__qyi6597778842032428791__produc axiom inv_axiom'4 [@rewrite] : forall x : t_Item'0 [inv'6 x] . inv'6 x = invariant'3 x - predicate invariant'1 [#"../../../creusot-contracts/src/logic/seq.rs" 610 4 610 30] (self : Seq.seq t_Item'0) = + predicate invariant'1 [#"../../../creusot-contracts/src/logic/seq.rs" 619 4 619 30] (self : Seq.seq t_Item'0) = [%#sseq21] forall i : int . 0 <= i /\ i < Seq.length self -> inv'6 (Seq.get self i) predicate inv'2 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : Seq.seq t_Item'0) @@ -2850,7 +2850,7 @@ module M_creusot_contracts__stdqy35z1__iter__map__qyi6597778842032428791__produc let%span siter22 = "../../../creusot-contracts/src/std/iter.rs" 46 15 46 32 let%span siter23 = "../../../creusot-contracts/src/std/iter.rs" 47 15 47 32 let%span siter24 = "../../../creusot-contracts/src/std/iter.rs" 48 14 48 42 - let%span sseq25 = "../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95 + let%span sseq25 = "../../../creusot-contracts/src/logic/seq.rs" 620 20 620 95 let%span sboxed26 = "../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18 let%span sinvariant27 = "../../../creusot-contracts/src/invariant.rs" 34 20 34 44 @@ -2938,7 +2938,7 @@ module M_creusot_contracts__stdqy35z1__iter__map__qyi6597778842032428791__produc axiom inv_axiom'3 [@rewrite] : forall x : borrowed t_F'0 [inv'5 x] . inv'5 x = invariant'2 x - predicate invariant'0 [#"../../../creusot-contracts/src/logic/seq.rs" 610 4 610 30] (self : Seq.seq (borrowed t_F'0)) + predicate invariant'0 [#"../../../creusot-contracts/src/logic/seq.rs" 619 4 619 30] (self : Seq.seq (borrowed t_F'0)) = [%#sseq25] forall i : int . 0 <= i /\ i < Seq.length self -> inv'5 (Seq.get self i) @@ -2963,7 +2963,7 @@ module M_creusot_contracts__stdqy35z1__iter__map__qyi6597778842032428791__produc axiom inv_axiom'4 [@rewrite] : forall x : t_Item'0 [inv'6 x] . inv'6 x = invariant'3 x - predicate invariant'1 [#"../../../creusot-contracts/src/logic/seq.rs" 610 4 610 30] (self : Seq.seq t_Item'0) = + predicate invariant'1 [#"../../../creusot-contracts/src/logic/seq.rs" 619 4 619 30] (self : Seq.seq t_Item'0) = [%#sseq25] forall i : int . 0 <= i /\ i < Seq.length self -> inv'6 (Seq.get self i) predicate inv'2 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : Seq.seq t_Item'0) @@ -3068,7 +3068,7 @@ module M_creusot_contracts__stdqy35z1__iter__map_inv__qyi9026772487048432788__pr let%span smap_inv21 = "../../../creusot-contracts/src/std/iter/map_inv.rs" 130 14 130 81 let%span smap_inv22 = "../../../creusot-contracts/src/std/iter/map_inv.rs" 133 12 138 88 let%span smap_inv23 = "../../../creusot-contracts/src/std/iter/map_inv.rs" 123 12 125 63 - let%span sseq24 = "../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95 + let%span sseq24 = "../../../creusot-contracts/src/logic/seq.rs" 620 20 620 95 let%span smap_inv25 = "../../../creusot-contracts/src/std/iter/map_inv.rs" 146 12 151 71 let%span sinvariant26 = "../../../creusot-contracts/src/invariant.rs" 34 20 34 44 let%span sboxed27 = "../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18 @@ -3152,7 +3152,7 @@ module M_creusot_contracts__stdqy35z1__iter__map_inv__qyi9026772487048432788__pr axiom inv_axiom'6 [@rewrite] : forall x : t_Item'0 [inv'10 x] . inv'10 x = invariant'6 x - predicate invariant'2 [#"../../../creusot-contracts/src/logic/seq.rs" 610 4 610 30] (self : Seq.seq t_Item'0) = + predicate invariant'2 [#"../../../creusot-contracts/src/logic/seq.rs" 619 4 619 30] (self : Seq.seq t_Item'0) = [%#sseq24] forall i : int . 0 <= i /\ i < Seq.length self -> inv'10 (Seq.get self i) predicate inv'2 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : Seq.seq t_Item'0) @@ -3262,7 +3262,7 @@ module M_creusot_contracts__stdqy35z1__iter__map_inv__qyi9026772487048432788__pr axiom inv_axiom'5 [@rewrite] : forall x : borrowed t_F'0 [inv'9 x] . inv'9 x = invariant'5 x - predicate invariant'1 [#"../../../creusot-contracts/src/logic/seq.rs" 610 4 610 30] (self : Seq.seq (borrowed t_F'0)) + predicate invariant'1 [#"../../../creusot-contracts/src/logic/seq.rs" 619 4 619 30] (self : Seq.seq (borrowed t_F'0)) = [%#sseq24] forall i : int . 0 <= i /\ i < Seq.length self -> inv'9 (Seq.get self i) @@ -3340,7 +3340,7 @@ module M_creusot_contracts__stdqy35z1__iter__map_inv__qyi9026772487048432788__pr let%span smap_inv25 = "../../../creusot-contracts/src/std/iter/map_inv.rs" 130 14 130 81 let%span smap_inv26 = "../../../creusot-contracts/src/std/iter/map_inv.rs" 133 12 138 88 let%span smap_inv27 = "../../../creusot-contracts/src/std/iter/map_inv.rs" 123 12 125 63 - let%span sseq28 = "../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95 + let%span sseq28 = "../../../creusot-contracts/src/logic/seq.rs" 620 20 620 95 let%span smap_inv29 = "../../../creusot-contracts/src/std/iter/map_inv.rs" 146 12 151 71 let%span sinvariant30 = "../../../creusot-contracts/src/invariant.rs" 34 20 34 44 let%span sboxed31 = "../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18 @@ -3424,7 +3424,7 @@ module M_creusot_contracts__stdqy35z1__iter__map_inv__qyi9026772487048432788__pr axiom inv_axiom'6 [@rewrite] : forall x : t_Item'0 [inv'10 x] . inv'10 x = invariant'6 x - predicate invariant'2 [#"../../../creusot-contracts/src/logic/seq.rs" 610 4 610 30] (self : Seq.seq t_Item'0) = + predicate invariant'2 [#"../../../creusot-contracts/src/logic/seq.rs" 619 4 619 30] (self : Seq.seq t_Item'0) = [%#sseq28] forall i : int . 0 <= i /\ i < Seq.length self -> inv'10 (Seq.get self i) predicate inv'2 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : Seq.seq t_Item'0) @@ -3532,7 +3532,7 @@ module M_creusot_contracts__stdqy35z1__iter__map_inv__qyi9026772487048432788__pr axiom inv_axiom'5 [@rewrite] : forall x : borrowed t_F'0 [inv'9 x] . inv'9 x = invariant'5 x - predicate invariant'1 [#"../../../creusot-contracts/src/logic/seq.rs" 610 4 610 30] (self : Seq.seq (borrowed t_F'0)) + predicate invariant'1 [#"../../../creusot-contracts/src/logic/seq.rs" 619 4 619 30] (self : Seq.seq (borrowed t_F'0)) = [%#sseq28] forall i : int . 0 <= i /\ i < Seq.length self -> inv'9 (Seq.get self i) @@ -3699,7 +3699,7 @@ module M_creusot_contracts__stdqy35z1__iter__map_inv__qyi4413682431414748756__ne let%span sinvariant56 = "../../../creusot-contracts/src/invariant.rs" 34 20 34 44 let%span smap_inv57 = "../../../creusot-contracts/src/std/iter/map_inv.rs" 80 12 82 73 let%span smap_inv58 = "../../../creusot-contracts/src/std/iter/map_inv.rs" 159 12 163 47 - let%span sseq59 = "../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95 + let%span sseq59 = "../../../creusot-contracts/src/logic/seq.rs" 620 20 620 95 let%span sboxed60 = "../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18 use prelude.prelude.Borrow @@ -3870,7 +3870,7 @@ module M_creusot_contracts__stdqy35z1__iter__map_inv__qyi4413682431414748756__ne axiom inv_axiom'9 [@rewrite] : forall x : t_Item'0 [inv'13 x] . inv'13 x = invariant'6 x - predicate invariant'4 [#"../../../creusot-contracts/src/logic/seq.rs" 610 4 610 30] (self : Seq.seq t_Item'0) = + predicate invariant'4 [#"../../../creusot-contracts/src/logic/seq.rs" 619 4 619 30] (self : Seq.seq t_Item'0) = [%#sseq59] forall i : int . 0 <= i /\ i < Seq.length self -> inv'13 (Seq.get self i) predicate inv'11 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : Seq.seq t_Item'0) @@ -3957,7 +3957,7 @@ module M_creusot_contracts__stdqy35z1__iter__map_inv__qyi4413682431414748756__ne axiom inv_axiom'10 [@rewrite] : forall x : borrowed t_F'0 [inv'14 x] . inv'14 x = invariant'7 x - predicate invariant'5 [#"../../../creusot-contracts/src/logic/seq.rs" 610 4 610 30] (self : Seq.seq (borrowed t_F'0)) + predicate invariant'5 [#"../../../creusot-contracts/src/logic/seq.rs" 619 4 619 30] (self : Seq.seq (borrowed t_F'0)) = [%#sseq59] forall i : int . 0 <= i /\ i < Seq.length self -> inv'14 (Seq.get self i) @@ -4181,7 +4181,7 @@ module M_creusot_contracts__stdqy35z1__iter__map_inv__qyi4899712594723907874__pr let%span siter15 = "../../../creusot-contracts/src/std/iter.rs" 46 15 46 32 let%span siter16 = "../../../creusot-contracts/src/std/iter.rs" 47 15 47 32 let%span siter17 = "../../../creusot-contracts/src/std/iter.rs" 48 14 48 42 - let%span sseq18 = "../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95 + let%span sseq18 = "../../../creusot-contracts/src/logic/seq.rs" 620 20 620 95 let%span sinvariant19 = "../../../creusot-contracts/src/invariant.rs" 34 20 34 44 let%span sboxed20 = "../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18 @@ -4214,7 +4214,7 @@ module M_creusot_contracts__stdqy35z1__iter__map_inv__qyi4899712594723907874__pr axiom inv_axiom'2 [@rewrite] : forall x : t_Item'0 [inv'5 x] . inv'5 x = invariant'2 x - predicate invariant'0 [#"../../../creusot-contracts/src/logic/seq.rs" 610 4 610 30] (self : Seq.seq t_Item'0) = + predicate invariant'0 [#"../../../creusot-contracts/src/logic/seq.rs" 619 4 619 30] (self : Seq.seq t_Item'0) = [%#sseq18] forall i : int . 0 <= i /\ i < Seq.length self -> inv'5 (Seq.get self i) predicate inv'0 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : Seq.seq t_Item'0) @@ -4352,7 +4352,7 @@ module M_creusot_contracts__stdqy35z1__iter__map_inv__qyi4899712594723907874__pr let%span sops26 = "../../../creusot-contracts/src/std/ops.rs" 122 14 122 28 let%span sops27 = "../../../creusot-contracts/src/std/ops.rs" 127 14 128 105 let%span sinvariant28 = "../../../creusot-contracts/src/invariant.rs" 34 20 34 44 - let%span sseq29 = "../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95 + let%span sseq29 = "../../../creusot-contracts/src/logic/seq.rs" 620 20 620 95 let%span smap_inv30 = "../../../creusot-contracts/src/std/iter/map_inv.rs" 80 12 82 73 let%span smap_inv31 = "../../../creusot-contracts/src/std/iter/map_inv.rs" 159 12 163 47 let%span smap_inv32 = "../../../creusot-contracts/src/std/iter/map_inv.rs" 130 14 130 81 @@ -4442,7 +4442,7 @@ module M_creusot_contracts__stdqy35z1__iter__map_inv__qyi4899712594723907874__pr axiom inv_axiom'5 [@rewrite] : forall x : t_Item'0 [inv'8 x] . inv'8 x = invariant'5 x - predicate invariant'2 [#"../../../creusot-contracts/src/logic/seq.rs" 610 4 610 30] (self : Seq.seq t_Item'0) = + predicate invariant'2 [#"../../../creusot-contracts/src/logic/seq.rs" 619 4 619 30] (self : Seq.seq t_Item'0) = [%#sseq29] forall i : int . 0 <= i /\ i < Seq.length self -> inv'8 (Seq.get self i) predicate inv'3 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : Seq.seq t_Item'0) @@ -4554,7 +4554,7 @@ module M_creusot_contracts__stdqy35z1__iter__map_inv__qyi4899712594723907874__pr axiom inv_axiom'4 [@rewrite] : forall x : borrowed t_F'0 [inv'7 x] . inv'7 x = invariant'4 x - predicate invariant'1 [#"../../../creusot-contracts/src/logic/seq.rs" 610 4 610 30] (self : Seq.seq (borrowed t_F'0)) + predicate invariant'1 [#"../../../creusot-contracts/src/logic/seq.rs" 619 4 619 30] (self : Seq.seq (borrowed t_F'0)) = [%#sseq29] forall i : int . 0 <= i /\ i < Seq.length self -> inv'7 (Seq.get self i) @@ -5188,7 +5188,7 @@ module M_creusot_contracts__stdqy35z1__iter__skip__qyi3195031491774060502__produ let%span siter11 = "../../../creusot-contracts/src/std/iter.rs" 46 15 46 32 let%span siter12 = "../../../creusot-contracts/src/std/iter.rs" 47 15 47 32 let%span siter13 = "../../../creusot-contracts/src/std/iter.rs" 48 14 48 42 - let%span sseq14 = "../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95 + let%span sseq14 = "../../../creusot-contracts/src/logic/seq.rs" 620 20 620 95 let%span sboxed15 = "../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18 type t_I'0 @@ -5236,7 +5236,7 @@ module M_creusot_contracts__stdqy35z1__iter__skip__qyi3195031491774060502__produ axiom inv_axiom'2 [@rewrite] : forall x : t_Item'0 [inv'3 x] . inv'3 x = invariant'1 x - predicate invariant'0 [#"../../../creusot-contracts/src/logic/seq.rs" 610 4 610 30] (self : Seq.seq t_Item'0) = + predicate invariant'0 [#"../../../creusot-contracts/src/logic/seq.rs" 619 4 619 30] (self : Seq.seq t_Item'0) = [%#sseq14] forall i : int . 0 <= i /\ i < Seq.length self -> inv'3 (Seq.get self i) predicate inv'1 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : Seq.seq t_Item'0) @@ -5309,7 +5309,7 @@ module M_creusot_contracts__stdqy35z1__iter__skip__qyi3195031491774060502__produ let%span siter15 = "../../../creusot-contracts/src/std/iter.rs" 46 15 46 32 let%span siter16 = "../../../creusot-contracts/src/std/iter.rs" 47 15 47 32 let%span siter17 = "../../../creusot-contracts/src/std/iter.rs" 48 14 48 42 - let%span sseq18 = "../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95 + let%span sseq18 = "../../../creusot-contracts/src/logic/seq.rs" 620 20 620 95 let%span sboxed19 = "../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18 type t_I'0 @@ -5357,7 +5357,7 @@ module M_creusot_contracts__stdqy35z1__iter__skip__qyi3195031491774060502__produ axiom inv_axiom'2 [@rewrite] : forall x : t_Item'0 [inv'3 x] . inv'3 x = invariant'1 x - predicate invariant'0 [#"../../../creusot-contracts/src/logic/seq.rs" 610 4 610 30] (self : Seq.seq t_Item'0) = + predicate invariant'0 [#"../../../creusot-contracts/src/logic/seq.rs" 619 4 619 30] (self : Seq.seq t_Item'0) = [%#sseq18] forall i : int . 0 <= i /\ i < Seq.length self -> inv'3 (Seq.get self i) predicate inv'1 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : Seq.seq t_Item'0) @@ -5622,7 +5622,7 @@ module M_creusot_contracts__stdqy35z1__iter__zip__qyi2281060687216883844__produc let%span siter11 = "../../../creusot-contracts/src/std/iter.rs" 46 15 46 32 let%span siter12 = "../../../creusot-contracts/src/std/iter.rs" 47 15 47 32 let%span siter13 = "../../../creusot-contracts/src/std/iter.rs" 48 14 48 42 - let%span sseq14 = "../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95 + let%span sseq14 = "../../../creusot-contracts/src/logic/seq.rs" 620 20 620 95 let%span sboxed15 = "../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18 type t_A'0 @@ -5673,7 +5673,7 @@ module M_creusot_contracts__stdqy35z1__iter__zip__qyi2281060687216883844__produc axiom inv_axiom'3 [@rewrite] : forall x : t_Item'0 [inv'5 x] . inv'5 x = invariant'2 x - predicate invariant'0 [#"../../../creusot-contracts/src/logic/seq.rs" 610 4 610 30] (self : Seq.seq t_Item'0) = + predicate invariant'0 [#"../../../creusot-contracts/src/logic/seq.rs" 619 4 619 30] (self : Seq.seq t_Item'0) = [%#sseq14] forall i : int . 0 <= i /\ i < Seq.length self -> inv'5 (Seq.get self i) predicate inv'1 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : Seq.seq t_Item'0) @@ -5693,7 +5693,7 @@ module M_creusot_contracts__stdqy35z1__iter__zip__qyi2281060687216883844__produc axiom inv_axiom'4 [@rewrite] : forall x : t_Item'1 [inv'6 x] . inv'6 x = invariant'3 x - predicate invariant'1 [#"../../../creusot-contracts/src/logic/seq.rs" 610 4 610 30] (self : Seq.seq t_Item'1) = + predicate invariant'1 [#"../../../creusot-contracts/src/logic/seq.rs" 619 4 619 30] (self : Seq.seq t_Item'1) = [%#sseq14] forall i : int . 0 <= i /\ i < Seq.length self -> inv'6 (Seq.get self i) predicate inv'2 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : Seq.seq t_Item'1) @@ -5794,7 +5794,7 @@ module M_creusot_contracts__stdqy35z1__iter__zip__qyi2281060687216883844__produc let%span siter15 = "../../../creusot-contracts/src/std/iter.rs" 46 15 46 32 let%span siter16 = "../../../creusot-contracts/src/std/iter.rs" 47 15 47 32 let%span siter17 = "../../../creusot-contracts/src/std/iter.rs" 48 14 48 42 - let%span sseq18 = "../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95 + let%span sseq18 = "../../../creusot-contracts/src/logic/seq.rs" 620 20 620 95 let%span sboxed19 = "../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18 type t_A'0 @@ -5843,7 +5843,7 @@ module M_creusot_contracts__stdqy35z1__iter__zip__qyi2281060687216883844__produc axiom inv_axiom'3 [@rewrite] : forall x : t_Item'0 [inv'5 x] . inv'5 x = invariant'2 x - predicate invariant'0 [#"../../../creusot-contracts/src/logic/seq.rs" 610 4 610 30] (self : Seq.seq t_Item'0) = + predicate invariant'0 [#"../../../creusot-contracts/src/logic/seq.rs" 619 4 619 30] (self : Seq.seq t_Item'0) = [%#sseq18] forall i : int . 0 <= i /\ i < Seq.length self -> inv'5 (Seq.get self i) predicate inv'1 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : Seq.seq t_Item'0) @@ -5863,7 +5863,7 @@ module M_creusot_contracts__stdqy35z1__iter__zip__qyi2281060687216883844__produc axiom inv_axiom'4 [@rewrite] : forall x : t_Item'1 [inv'6 x] . inv'6 x = invariant'3 x - predicate invariant'1 [#"../../../creusot-contracts/src/logic/seq.rs" 610 4 610 30] (self : Seq.seq t_Item'1) = + predicate invariant'1 [#"../../../creusot-contracts/src/logic/seq.rs" 619 4 619 30] (self : Seq.seq t_Item'1) = [%#sseq18] forall i : int . 0 <= i /\ i < Seq.length self -> inv'6 (Seq.get self i) predicate inv'2 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : Seq.seq t_Item'1) @@ -21807,7 +21807,7 @@ module M_creusot_contracts__stdqy35z1__vec__qyi6844585276173866460__resolve_cohe let%span sindex3 = "../../../creusot-contracts/src/logic/ops/index.rs" 23 8 23 31 let%span sinvariant4 = "../../../creusot-contracts/src/invariant.rs" 24 8 24 18 let%span svec5 = "../../../creusot-contracts/src/std/vec.rs" 65 20 65 41 - let%span sseq6 = "../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95 + let%span sseq6 = "../../../creusot-contracts/src/logic/seq.rs" 620 20 620 95 let%span sboxed7 = "../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18 use prelude.prelude.Borrow @@ -21871,7 +21871,7 @@ module M_creusot_contracts__stdqy35z1__vec__qyi6844585276173866460__resolve_cohe axiom inv_axiom'3 [@rewrite] : forall x : t_T'0 [inv'3 x] . inv'3 x = invariant'3 x - predicate invariant'2 [#"../../../creusot-contracts/src/logic/seq.rs" 610 4 610 30] (self : Seq.seq t_T'0) = + predicate invariant'2 [#"../../../creusot-contracts/src/logic/seq.rs" 619 4 619 30] (self : Seq.seq t_T'0) = [%#sseq6] forall i : int . 0 <= i /\ i < Seq.length self -> inv'3 (Seq.get self i) predicate inv'2 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : Seq.seq t_T'0) @@ -22407,7 +22407,7 @@ module M_creusot_contracts__stdqy35z1__iter__cloned__qyi10472681371035856984__pr let%span siter8 = "../../../creusot-contracts/src/std/iter.rs" 46 15 46 32 let%span siter9 = "../../../creusot-contracts/src/std/iter.rs" 47 15 47 32 let%span siter10 = "../../../creusot-contracts/src/std/iter.rs" 48 14 48 42 - let%span sseq11 = "../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95 + let%span sseq11 = "../../../creusot-contracts/src/logic/seq.rs" 620 20 620 95 let%span sboxed12 = "../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18 let%span sinvariant13 = "../../../creusot-contracts/src/invariant.rs" 24 8 24 18 @@ -22446,7 +22446,7 @@ module M_creusot_contracts__stdqy35z1__iter__cloned__qyi10472681371035856984__pr axiom inv_axiom'2 [@rewrite] : forall x : t_T'0 [inv'3 x] . inv'3 x = invariant'1 x - predicate invariant'0 [#"../../../creusot-contracts/src/logic/seq.rs" 610 4 610 30] (self : Seq.seq t_T'0) = + predicate invariant'0 [#"../../../creusot-contracts/src/logic/seq.rs" 619 4 619 30] (self : Seq.seq t_T'0) = [%#sseq11] forall i : int . 0 <= i /\ i < Seq.length self -> inv'3 (Seq.get self i) predicate inv'1 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : Seq.seq t_T'0) @@ -22522,7 +22522,7 @@ module M_creusot_contracts__stdqy35z1__iter__cloned__qyi10472681371035856984__pr let%span siter8 = "../../../creusot-contracts/src/std/iter.rs" 46 15 46 32 let%span siter9 = "../../../creusot-contracts/src/std/iter.rs" 47 15 47 32 let%span siter10 = "../../../creusot-contracts/src/std/iter.rs" 48 14 48 42 - let%span sseq11 = "../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95 + let%span sseq11 = "../../../creusot-contracts/src/logic/seq.rs" 620 20 620 95 let%span sboxed12 = "../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18 let%span sinvariant13 = "../../../creusot-contracts/src/invariant.rs" 24 8 24 18 @@ -22572,7 +22572,7 @@ module M_creusot_contracts__stdqy35z1__iter__cloned__qyi10472681371035856984__pr axiom inv_axiom'2 [@rewrite] : forall x : t_T'0 [inv'3 x] . inv'3 x = invariant'1 x - predicate invariant'0 [#"../../../creusot-contracts/src/logic/seq.rs" 610 4 610 30] (self : Seq.seq t_T'0) = + predicate invariant'0 [#"../../../creusot-contracts/src/logic/seq.rs" 619 4 619 30] (self : Seq.seq t_T'0) = [%#sseq11] forall i : int . 0 <= i /\ i < Seq.length self -> inv'3 (Seq.get self i) predicate inv'1 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : Seq.seq t_T'0) @@ -22635,7 +22635,7 @@ module M_creusot_contracts__stdqy35z1__iter__copied__qyi18224474876607687026__pr let%span siter8 = "../../../creusot-contracts/src/std/iter.rs" 46 15 46 32 let%span siter9 = "../../../creusot-contracts/src/std/iter.rs" 47 15 47 32 let%span siter10 = "../../../creusot-contracts/src/std/iter.rs" 48 14 48 42 - let%span sseq11 = "../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95 + let%span sseq11 = "../../../creusot-contracts/src/logic/seq.rs" 620 20 620 95 let%span sboxed12 = "../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18 let%span sinvariant13 = "../../../creusot-contracts/src/invariant.rs" 24 8 24 18 @@ -22685,7 +22685,7 @@ module M_creusot_contracts__stdqy35z1__iter__copied__qyi18224474876607687026__pr axiom inv_axiom'2 [@rewrite] : forall x : t_T'0 [inv'3 x] . inv'3 x = invariant'1 x - predicate invariant'0 [#"../../../creusot-contracts/src/logic/seq.rs" 610 4 610 30] (self : Seq.seq t_T'0) = + predicate invariant'0 [#"../../../creusot-contracts/src/logic/seq.rs" 619 4 619 30] (self : Seq.seq t_T'0) = [%#sseq11] forall i : int . 0 <= i /\ i < Seq.length self -> inv'3 (Seq.get self i) predicate inv'1 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : Seq.seq t_T'0) @@ -22748,7 +22748,7 @@ module M_creusot_contracts__stdqy35z1__iter__copied__qyi18224474876607687026__pr let%span siter8 = "../../../creusot-contracts/src/std/iter.rs" 46 15 46 32 let%span siter9 = "../../../creusot-contracts/src/std/iter.rs" 47 15 47 32 let%span siter10 = "../../../creusot-contracts/src/std/iter.rs" 48 14 48 42 - let%span sseq11 = "../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95 + let%span sseq11 = "../../../creusot-contracts/src/logic/seq.rs" 620 20 620 95 let%span sboxed12 = "../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18 let%span sinvariant13 = "../../../creusot-contracts/src/invariant.rs" 24 8 24 18 @@ -22787,7 +22787,7 @@ module M_creusot_contracts__stdqy35z1__iter__copied__qyi18224474876607687026__pr axiom inv_axiom'2 [@rewrite] : forall x : t_T'0 [inv'3 x] . inv'3 x = invariant'1 x - predicate invariant'0 [#"../../../creusot-contracts/src/logic/seq.rs" 610 4 610 30] (self : Seq.seq t_T'0) = + predicate invariant'0 [#"../../../creusot-contracts/src/logic/seq.rs" 619 4 619 30] (self : Seq.seq t_T'0) = [%#sseq11] forall i : int . 0 <= i /\ i < Seq.length self -> inv'3 (Seq.get self i) predicate inv'1 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : Seq.seq t_T'0) @@ -22922,7 +22922,7 @@ module M_creusot_contracts__stdqy35z1__iter__enumerate__qyi2718914205750388896__ let%span siter9 = "../../../creusot-contracts/src/std/iter.rs" 47 15 47 32 let%span siter10 = "../../../creusot-contracts/src/std/iter.rs" 48 14 48 42 let%span senumerate11 = "../../../creusot-contracts/src/std/iter/enumerate.rs" 45 12 49 79 - let%span sseq12 = "../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95 + let%span sseq12 = "../../../creusot-contracts/src/logic/seq.rs" 620 20 620 95 let%span sboxed13 = "../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18 type t_I'0 @@ -22957,7 +22957,7 @@ module M_creusot_contracts__stdqy35z1__iter__enumerate__qyi2718914205750388896__ axiom inv_axiom'2 [@rewrite] : forall x : t_Item'0 [inv'3 x] . inv'3 x = invariant'2 x - predicate invariant'1 [#"../../../creusot-contracts/src/logic/seq.rs" 610 4 610 30] (self : Seq.seq t_Item'0) = + predicate invariant'1 [#"../../../creusot-contracts/src/logic/seq.rs" 619 4 619 30] (self : Seq.seq t_Item'0) = [%#sseq12] forall i : int . 0 <= i /\ i < Seq.length self -> inv'3 (Seq.get self i) predicate inv'1 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : Seq.seq t_Item'0) @@ -23049,7 +23049,7 @@ module M_creusot_contracts__stdqy35z1__iter__enumerate__qyi2718914205750388896__ let%span siter9 = "../../../creusot-contracts/src/std/iter.rs" 46 15 46 32 let%span siter10 = "../../../creusot-contracts/src/std/iter.rs" 47 15 47 32 let%span siter11 = "../../../creusot-contracts/src/std/iter.rs" 48 14 48 42 - let%span sseq12 = "../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95 + let%span sseq12 = "../../../creusot-contracts/src/logic/seq.rs" 620 20 620 95 let%span sboxed13 = "../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18 type t_I'0 @@ -23078,7 +23078,7 @@ module M_creusot_contracts__stdqy35z1__iter__enumerate__qyi2718914205750388896__ axiom inv_axiom'2 [@rewrite] : forall x : t_Item'0 [inv'3 x] . inv'3 x = invariant'2 x - predicate invariant'1 [#"../../../creusot-contracts/src/logic/seq.rs" 610 4 610 30] (self : Seq.seq t_Item'0) = + predicate invariant'1 [#"../../../creusot-contracts/src/logic/seq.rs" 619 4 619 30] (self : Seq.seq t_Item'0) = [%#sseq12] forall i : int . 0 <= i /\ i < Seq.length self -> inv'3 (Seq.get self i) predicate inv'1 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : Seq.seq t_Item'0) @@ -23643,7 +23643,7 @@ module M_creusot_contracts__stdqy35z1__iter__map__qyi6597778842032428791__produc let%span siter16 = "../../../creusot-contracts/src/std/iter.rs" 46 15 46 32 let%span siter17 = "../../../creusot-contracts/src/std/iter.rs" 47 15 47 32 let%span siter18 = "../../../creusot-contracts/src/std/iter.rs" 48 14 48 42 - let%span sseq19 = "../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95 + let%span sseq19 = "../../../creusot-contracts/src/logic/seq.rs" 620 20 620 95 let%span sboxed20 = "../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18 let%span sinvariant21 = "../../../creusot-contracts/src/invariant.rs" 34 20 34 44 @@ -23733,7 +23733,7 @@ module M_creusot_contracts__stdqy35z1__iter__map__qyi6597778842032428791__produc axiom inv_axiom'3 [@rewrite] : forall x : borrowed t_F'0 [inv'5 x] . inv'5 x = invariant'2 x - predicate invariant'0 [#"../../../creusot-contracts/src/logic/seq.rs" 610 4 610 30] (self : Seq.seq (borrowed t_F'0)) + predicate invariant'0 [#"../../../creusot-contracts/src/logic/seq.rs" 619 4 619 30] (self : Seq.seq (borrowed t_F'0)) = [%#sseq19] forall i : int . 0 <= i /\ i < Seq.length self -> inv'5 (Seq.get self i) @@ -23758,7 +23758,7 @@ module M_creusot_contracts__stdqy35z1__iter__map__qyi6597778842032428791__produc axiom inv_axiom'4 [@rewrite] : forall x : t_Item'0 [inv'6 x] . inv'6 x = invariant'3 x - predicate invariant'1 [#"../../../creusot-contracts/src/logic/seq.rs" 610 4 610 30] (self : Seq.seq t_Item'0) = + predicate invariant'1 [#"../../../creusot-contracts/src/logic/seq.rs" 619 4 619 30] (self : Seq.seq t_Item'0) = [%#sseq19] forall i : int . 0 <= i /\ i < Seq.length self -> inv'6 (Seq.get self i) predicate inv'2 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : Seq.seq t_Item'0) @@ -23843,7 +23843,7 @@ module M_creusot_contracts__stdqy35z1__iter__map__qyi6597778842032428791__produc let%span siter16 = "../../../creusot-contracts/src/std/iter.rs" 46 15 46 32 let%span siter17 = "../../../creusot-contracts/src/std/iter.rs" 47 15 47 32 let%span siter18 = "../../../creusot-contracts/src/std/iter.rs" 48 14 48 42 - let%span sseq19 = "../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95 + let%span sseq19 = "../../../creusot-contracts/src/logic/seq.rs" 620 20 620 95 let%span sboxed20 = "../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18 let%span sinvariant21 = "../../../creusot-contracts/src/invariant.rs" 34 20 34 44 @@ -23931,7 +23931,7 @@ module M_creusot_contracts__stdqy35z1__iter__map__qyi6597778842032428791__produc axiom inv_axiom'3 [@rewrite] : forall x : borrowed t_F'0 [inv'5 x] . inv'5 x = invariant'2 x - predicate invariant'0 [#"../../../creusot-contracts/src/logic/seq.rs" 610 4 610 30] (self : Seq.seq (borrowed t_F'0)) + predicate invariant'0 [#"../../../creusot-contracts/src/logic/seq.rs" 619 4 619 30] (self : Seq.seq (borrowed t_F'0)) = [%#sseq19] forall i : int . 0 <= i /\ i < Seq.length self -> inv'5 (Seq.get self i) @@ -23956,7 +23956,7 @@ module M_creusot_contracts__stdqy35z1__iter__map__qyi6597778842032428791__produc axiom inv_axiom'4 [@rewrite] : forall x : t_Item'0 [inv'6 x] . inv'6 x = invariant'3 x - predicate invariant'1 [#"../../../creusot-contracts/src/logic/seq.rs" 610 4 610 30] (self : Seq.seq t_Item'0) = + predicate invariant'1 [#"../../../creusot-contracts/src/logic/seq.rs" 619 4 619 30] (self : Seq.seq t_Item'0) = [%#sseq19] forall i : int . 0 <= i /\ i < Seq.length self -> inv'6 (Seq.get self i) predicate inv'2 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : Seq.seq t_Item'0) @@ -24048,7 +24048,7 @@ module M_creusot_contracts__stdqy35z1__iter__map_inv__qyi9026772487048432788__pr let%span smap_inv19 = "../../../creusot-contracts/src/std/iter/map_inv.rs" 130 14 130 81 let%span smap_inv20 = "../../../creusot-contracts/src/std/iter/map_inv.rs" 133 12 138 88 let%span smap_inv21 = "../../../creusot-contracts/src/std/iter/map_inv.rs" 123 12 125 63 - let%span sseq22 = "../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95 + let%span sseq22 = "../../../creusot-contracts/src/logic/seq.rs" 620 20 620 95 let%span smap_inv23 = "../../../creusot-contracts/src/std/iter/map_inv.rs" 146 12 151 71 let%span sinvariant24 = "../../../creusot-contracts/src/invariant.rs" 34 20 34 44 let%span sboxed25 = "../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18 @@ -24132,7 +24132,7 @@ module M_creusot_contracts__stdqy35z1__iter__map_inv__qyi9026772487048432788__pr axiom inv_axiom'6 [@rewrite] : forall x : t_Item'0 [inv'10 x] . inv'10 x = invariant'6 x - predicate invariant'2 [#"../../../creusot-contracts/src/logic/seq.rs" 610 4 610 30] (self : Seq.seq t_Item'0) = + predicate invariant'2 [#"../../../creusot-contracts/src/logic/seq.rs" 619 4 619 30] (self : Seq.seq t_Item'0) = [%#sseq22] forall i : int . 0 <= i /\ i < Seq.length self -> inv'10 (Seq.get self i) predicate inv'2 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : Seq.seq t_Item'0) @@ -24242,7 +24242,7 @@ module M_creusot_contracts__stdqy35z1__iter__map_inv__qyi9026772487048432788__pr axiom inv_axiom'5 [@rewrite] : forall x : borrowed t_F'0 [inv'9 x] . inv'9 x = invariant'5 x - predicate invariant'1 [#"../../../creusot-contracts/src/logic/seq.rs" 610 4 610 30] (self : Seq.seq (borrowed t_F'0)) + predicate invariant'1 [#"../../../creusot-contracts/src/logic/seq.rs" 619 4 619 30] (self : Seq.seq (borrowed t_F'0)) = [%#sseq22] forall i : int . 0 <= i /\ i < Seq.length self -> inv'9 (Seq.get self i) @@ -24308,7 +24308,7 @@ module M_creusot_contracts__stdqy35z1__iter__map_inv__qyi9026772487048432788__pr let%span siter15 = "../../../creusot-contracts/src/std/iter.rs" 47 15 47 32 let%span siter16 = "../../../creusot-contracts/src/std/iter.rs" 48 14 48 42 let%span smap_inv17 = "../../../creusot-contracts/src/std/iter/map_inv.rs" 80 12 82 73 - let%span sseq18 = "../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95 + let%span sseq18 = "../../../creusot-contracts/src/logic/seq.rs" 620 20 620 95 let%span smap_inv19 = "../../../creusot-contracts/src/std/iter/map_inv.rs" 159 12 163 47 let%span smap_inv20 = "../../../creusot-contracts/src/std/iter/map_inv.rs" 130 14 130 81 let%span smap_inv21 = "../../../creusot-contracts/src/std/iter/map_inv.rs" 133 12 138 88 @@ -24392,7 +24392,7 @@ module M_creusot_contracts__stdqy35z1__iter__map_inv__qyi9026772487048432788__pr axiom inv_axiom'3 [@rewrite] : forall x : borrowed t_F'0 [inv'5 x] . inv'5 x = invariant'3 x - predicate invariant'1 [#"../../../creusot-contracts/src/logic/seq.rs" 610 4 610 30] (self : Seq.seq (borrowed t_F'0)) + predicate invariant'1 [#"../../../creusot-contracts/src/logic/seq.rs" 619 4 619 30] (self : Seq.seq (borrowed t_F'0)) = [%#sseq18] forall i : int . 0 <= i /\ i < Seq.length self -> inv'5 (Seq.get self i) @@ -24415,7 +24415,7 @@ module M_creusot_contracts__stdqy35z1__iter__map_inv__qyi9026772487048432788__pr axiom inv_axiom'4 [@rewrite] : forall x : t_Item'0 [inv'6 x] . inv'6 x = invariant'4 x - predicate invariant'2 [#"../../../creusot-contracts/src/logic/seq.rs" 610 4 610 30] (self : Seq.seq t_Item'0) = + predicate invariant'2 [#"../../../creusot-contracts/src/logic/seq.rs" 619 4 619 30] (self : Seq.seq t_Item'0) = [%#sseq18] forall i : int . 0 <= i /\ i < Seq.length self -> inv'6 (Seq.get self i) predicate inv'2 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : Seq.seq t_Item'0) @@ -25013,7 +25013,7 @@ module M_creusot_contracts__stdqy35z1__iter__skip__qyi3195031491774060502__produ let%span siter9 = "../../../creusot-contracts/src/std/iter.rs" 46 15 46 32 let%span siter10 = "../../../creusot-contracts/src/std/iter.rs" 47 15 47 32 let%span siter11 = "../../../creusot-contracts/src/std/iter.rs" 48 14 48 42 - let%span sseq12 = "../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95 + let%span sseq12 = "../../../creusot-contracts/src/logic/seq.rs" 620 20 620 95 let%span sboxed13 = "../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18 type t_I'0 @@ -25052,7 +25052,7 @@ module M_creusot_contracts__stdqy35z1__iter__skip__qyi3195031491774060502__produ axiom inv_axiom'2 [@rewrite] : forall x : t_Item'0 [inv'3 x] . inv'3 x = invariant'1 x - predicate invariant'0 [#"../../../creusot-contracts/src/logic/seq.rs" 610 4 610 30] (self : Seq.seq t_Item'0) = + predicate invariant'0 [#"../../../creusot-contracts/src/logic/seq.rs" 619 4 619 30] (self : Seq.seq t_Item'0) = [%#sseq12] forall i : int . 0 <= i /\ i < Seq.length self -> inv'3 (Seq.get self i) predicate inv'1 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : Seq.seq t_Item'0) @@ -25128,7 +25128,7 @@ module M_creusot_contracts__stdqy35z1__iter__skip__qyi3195031491774060502__produ let%span siter9 = "../../../creusot-contracts/src/std/iter.rs" 46 15 46 32 let%span siter10 = "../../../creusot-contracts/src/std/iter.rs" 47 15 47 32 let%span siter11 = "../../../creusot-contracts/src/std/iter.rs" 48 14 48 42 - let%span sseq12 = "../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95 + let%span sseq12 = "../../../creusot-contracts/src/logic/seq.rs" 620 20 620 95 let%span sboxed13 = "../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18 type t_I'0 @@ -25176,7 +25176,7 @@ module M_creusot_contracts__stdqy35z1__iter__skip__qyi3195031491774060502__produ axiom inv_axiom'2 [@rewrite] : forall x : t_Item'0 [inv'3 x] . inv'3 x = invariant'1 x - predicate invariant'0 [#"../../../creusot-contracts/src/logic/seq.rs" 610 4 610 30] (self : Seq.seq t_Item'0) = + predicate invariant'0 [#"../../../creusot-contracts/src/logic/seq.rs" 619 4 619 30] (self : Seq.seq t_Item'0) = [%#sseq12] forall i : int . 0 <= i /\ i < Seq.length self -> inv'3 (Seq.get self i) predicate inv'1 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : Seq.seq t_Item'0) @@ -25405,7 +25405,7 @@ module M_creusot_contracts__stdqy35z1__iter__zip__qyi2281060687216883844__produc let%span siter9 = "../../../creusot-contracts/src/std/iter.rs" 46 15 46 32 let%span siter10 = "../../../creusot-contracts/src/std/iter.rs" 47 15 47 32 let%span siter11 = "../../../creusot-contracts/src/std/iter.rs" 48 14 48 42 - let%span sseq12 = "../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95 + let%span sseq12 = "../../../creusot-contracts/src/logic/seq.rs" 620 20 620 95 let%span sboxed13 = "../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18 type t_A'0 @@ -25442,7 +25442,7 @@ module M_creusot_contracts__stdqy35z1__iter__zip__qyi2281060687216883844__produc axiom inv_axiom'3 [@rewrite] : forall x : t_Item'0 [inv'5 x] . inv'5 x = invariant'2 x - predicate invariant'0 [#"../../../creusot-contracts/src/logic/seq.rs" 610 4 610 30] (self : Seq.seq t_Item'0) = + predicate invariant'0 [#"../../../creusot-contracts/src/logic/seq.rs" 619 4 619 30] (self : Seq.seq t_Item'0) = [%#sseq12] forall i : int . 0 <= i /\ i < Seq.length self -> inv'5 (Seq.get self i) predicate inv'1 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : Seq.seq t_Item'0) @@ -25462,7 +25462,7 @@ module M_creusot_contracts__stdqy35z1__iter__zip__qyi2281060687216883844__produc axiom inv_axiom'4 [@rewrite] : forall x : t_Item'1 [inv'6 x] . inv'6 x = invariant'3 x - predicate invariant'1 [#"../../../creusot-contracts/src/logic/seq.rs" 610 4 610 30] (self : Seq.seq t_Item'1) = + predicate invariant'1 [#"../../../creusot-contracts/src/logic/seq.rs" 619 4 619 30] (self : Seq.seq t_Item'1) = [%#sseq12] forall i : int . 0 <= i /\ i < Seq.length self -> inv'6 (Seq.get self i) predicate inv'2 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : Seq.seq t_Item'1) @@ -25571,7 +25571,7 @@ module M_creusot_contracts__stdqy35z1__iter__zip__qyi2281060687216883844__produc let%span siter9 = "../../../creusot-contracts/src/std/iter.rs" 46 15 46 32 let%span siter10 = "../../../creusot-contracts/src/std/iter.rs" 47 15 47 32 let%span siter11 = "../../../creusot-contracts/src/std/iter.rs" 48 14 48 42 - let%span sseq12 = "../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95 + let%span sseq12 = "../../../creusot-contracts/src/logic/seq.rs" 620 20 620 95 let%span sboxed13 = "../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18 type t_A'0 @@ -25622,7 +25622,7 @@ module M_creusot_contracts__stdqy35z1__iter__zip__qyi2281060687216883844__produc axiom inv_axiom'3 [@rewrite] : forall x : t_Item'0 [inv'5 x] . inv'5 x = invariant'2 x - predicate invariant'0 [#"../../../creusot-contracts/src/logic/seq.rs" 610 4 610 30] (self : Seq.seq t_Item'0) = + predicate invariant'0 [#"../../../creusot-contracts/src/logic/seq.rs" 619 4 619 30] (self : Seq.seq t_Item'0) = [%#sseq12] forall i : int . 0 <= i /\ i < Seq.length self -> inv'5 (Seq.get self i) predicate inv'1 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : Seq.seq t_Item'0) @@ -25642,7 +25642,7 @@ module M_creusot_contracts__stdqy35z1__iter__zip__qyi2281060687216883844__produc axiom inv_axiom'4 [@rewrite] : forall x : t_Item'1 [inv'6 x] . inv'6 x = invariant'3 x - predicate invariant'1 [#"../../../creusot-contracts/src/logic/seq.rs" 610 4 610 30] (self : Seq.seq t_Item'1) = + predicate invariant'1 [#"../../../creusot-contracts/src/logic/seq.rs" 619 4 619 30] (self : Seq.seq t_Item'1) = [%#sseq12] forall i : int . 0 <= i /\ i < Seq.length self -> inv'6 (Seq.get self i) predicate inv'2 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : Seq.seq t_Item'1) @@ -26624,7 +26624,7 @@ module M_creusot_contracts__stdqy35z1__iter__fuse__qyi7691061398646472980__is_fu let%span siter21 = "../../../creusot-contracts/src/std/iter.rs" 46 15 46 32 let%span siter22 = "../../../creusot-contracts/src/std/iter.rs" 47 15 47 32 let%span siter23 = "../../../creusot-contracts/src/std/iter.rs" 48 14 48 42 - let%span sseq24 = "../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95 + let%span sseq24 = "../../../creusot-contracts/src/logic/seq.rs" 620 20 620 95 let%span sinvariant25 = "../../../creusot-contracts/src/invariant.rs" 34 20 34 44 let%span sboxed26 = "../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18 @@ -26746,7 +26746,7 @@ module M_creusot_contracts__stdqy35z1__iter__fuse__qyi7691061398646472980__is_fu axiom inv_axiom'5 [@rewrite] : forall x : t_Item'0 [inv'6 x] . inv'6 x = invariant'3 x - predicate invariant'0 [#"../../../creusot-contracts/src/logic/seq.rs" 610 4 610 30] (self : Seq.seq t_Item'0) = + predicate invariant'0 [#"../../../creusot-contracts/src/logic/seq.rs" 619 4 619 30] (self : Seq.seq t_Item'0) = [%#sseq24] forall i : int . 0 <= i /\ i < Seq.length self -> inv'6 (Seq.get self i) predicate inv'0 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : Seq.seq t_Item'0) @@ -26802,7 +26802,7 @@ module M_creusot_contracts__stdqy35z1__iter__map_inv__qyi4413682431414748756__ne let%span sops28 = "../../../creusot-contracts/src/std/ops.rs" 121 15 121 26 let%span sops29 = "../../../creusot-contracts/src/std/ops.rs" 122 14 122 28 let%span sops30 = "../../../creusot-contracts/src/std/ops.rs" 127 14 128 105 - let%span sseq31 = "../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95 + let%span sseq31 = "../../../creusot-contracts/src/logic/seq.rs" 620 20 620 95 let%span smap_inv32 = "../../../creusot-contracts/src/std/iter/map_inv.rs" 80 12 82 73 let%span smap_inv33 = "../../../creusot-contracts/src/std/iter/map_inv.rs" 159 12 163 47 let%span smap_inv34 = "../../../creusot-contracts/src/std/iter/map_inv.rs" 130 14 130 81 @@ -26890,7 +26890,7 @@ module M_creusot_contracts__stdqy35z1__iter__map_inv__qyi4413682431414748756__ne axiom inv_axiom'7 [@rewrite] : forall x : t_Item'0 [inv'11 x] . inv'11 x = invariant'6 x - predicate invariant'3 [#"../../../creusot-contracts/src/logic/seq.rs" 610 4 610 30] (self : Seq.seq t_Item'0) = + predicate invariant'3 [#"../../../creusot-contracts/src/logic/seq.rs" 619 4 619 30] (self : Seq.seq t_Item'0) = [%#sseq31] forall i : int . 0 <= i /\ i < Seq.length self -> inv'11 (Seq.get self i) predicate inv'5 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : Seq.seq t_Item'0) @@ -27009,7 +27009,7 @@ module M_creusot_contracts__stdqy35z1__iter__map_inv__qyi4413682431414748756__ne axiom inv_axiom'6 [@rewrite] : forall x : borrowed t_F'0 [inv'10 x] . inv'10 x = invariant'5 x - predicate invariant'2 [#"../../../creusot-contracts/src/logic/seq.rs" 610 4 610 30] (self : Seq.seq (borrowed t_F'0)) + predicate invariant'2 [#"../../../creusot-contracts/src/logic/seq.rs" 619 4 619 30] (self : Seq.seq (borrowed t_F'0)) = [%#sseq31] forall i : int . 0 <= i /\ i < Seq.length self -> inv'10 (Seq.get self i) @@ -27282,6 +27282,44 @@ module M_creusot_contracts__ghost__qyi17645547594388049322__clone__refines [#".. goal refines : [%#sghost0] forall self : t_GhostBox'0 . inv'0 self -> inv'0 self /\ (forall result : t_GhostBox'0 . result = self /\ inv'1 result -> result = self /\ inv'1 result) end +module M_creusot_contracts__logic__fmap__qyi4648834920430559677__clone__refines [#"../../../creusot-contracts/src/logic/fmap.rs" 438 4 438 27] (* as std::clone::Clone> *) + let%span sfmap0 = "../../../creusot-contracts/src/logic/fmap.rs" 438 4 438 27 + + use prelude.prelude.Borrow + + type t_FMap'0 + + predicate inv'0 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : t_FMap'0) + + axiom inv_axiom'0 [@rewrite] : forall x : t_FMap'0 [inv'0 x] . inv'0 x = true + + predicate inv'1 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : t_FMap'0) + + axiom inv_axiom'1 [@rewrite] : forall x : t_FMap'0 [inv'1 x] . inv'1 x = true + + goal refines : [%#sfmap0] forall self : t_FMap'0 . inv'0 self + -> (forall result : t_FMap'0 . result = self -> result = self /\ inv'1 result) +end +module M_creusot_contracts__logic__fset__qyi11096226875104347554__clone__refines [#"../../../creusot-contracts/src/logic/fset.rs" 312 4 312 27] (* as std::clone::Clone> *) + let%span sfset0 = "../../../creusot-contracts/src/logic/fset.rs" 312 4 312 27 + + use prelude.prelude.Borrow + + type t_T'0 + + use set.Fset + + predicate inv'0 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : Fset.fset t_T'0) + + axiom inv_axiom'0 [@rewrite] : forall x : Fset.fset t_T'0 [inv'0 x] . inv'0 x = true + + predicate inv'1 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : Fset.fset t_T'0) + + axiom inv_axiom'1 [@rewrite] : forall x : Fset.fset t_T'0 [inv'1 x] . inv'1 x = true + + goal refines : [%#sfset0] forall self : Fset.fset t_T'0 . inv'0 self + -> (forall result : Fset.fset t_T'0 . result = self -> result = self /\ inv'1 result) +end module M_creusot_contracts__logic__int__qyi3540547019284611154__clone__refines [#"../../../creusot-contracts/src/logic/int.rs" 37 4 37 27] (* *) let%span sint0 = "../../../creusot-contracts/src/logic/int.rs" 37 4 37 27 @@ -27300,6 +27338,50 @@ module M_creusot_contracts__logic__int__qyi3540547019284611154__clone__refines [ goal refines : [%#sint0] forall self : int . inv'0 self -> (forall result : int . result = self -> result = self /\ inv'1 result) end +module M_creusot_contracts__logic__seq__qyi8239750555979287100__clone__refines [#"../../../creusot-contracts/src/logic/seq.rs" 609 4 609 27] (* as std::clone::Clone> *) + let%span sseq0 = "../../../creusot-contracts/src/logic/seq.rs" 609 4 609 27 + let%span sinvariant1 = "../../../creusot-contracts/src/invariant.rs" 24 8 24 18 + let%span sseq2 = "../../../creusot-contracts/src/logic/seq.rs" 620 20 620 95 + let%span sboxed3 = "../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18 + + use prelude.prelude.Borrow + + type t_T'0 + + use seq.Seq + + use prelude.prelude.Int + + use seq.Seq + + use seq.Seq + + predicate inv'3 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : t_T'0) + + predicate invariant'2 [#"../../../creusot-contracts/src/std/boxed.rs" 27 4 27 30] (self : t_T'0) = + [%#sboxed3] inv'3 self + + predicate inv'2 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : t_T'0) + + axiom inv_axiom'2 [@rewrite] : forall x : t_T'0 [inv'2 x] . inv'2 x = invariant'2 x + + predicate invariant'1 [#"../../../creusot-contracts/src/logic/seq.rs" 619 4 619 30] (self : Seq.seq t_T'0) = + [%#sseq2] forall i : int . 0 <= i /\ i < Seq.length self -> inv'2 (Seq.get self i) + + predicate inv'1 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : Seq.seq t_T'0) + + axiom inv_axiom'1 [@rewrite] : forall x : Seq.seq t_T'0 [inv'1 x] . inv'1 x = invariant'1 x + + predicate invariant'0 [#"../../../creusot-contracts/src/invariant.rs" 23 4 23 30] (self : Seq.seq t_T'0) = + [%#sinvariant1] inv'1 self + + predicate inv'0 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : Seq.seq t_T'0) + + axiom inv_axiom'0 [@rewrite] : forall x : Seq.seq t_T'0 [inv'0 x] . inv'0 x = invariant'0 x + + goal refines : [%#sseq0] forall self : Seq.seq t_T'0 . inv'0 self + -> inv'0 self /\ (forall result : Seq.seq t_T'0 . result = self /\ inv'1 result -> result = self /\ inv'1 result) +end module M_creusot_contracts__snapshot__qyi5567339964777190687__clone__refines [#"../../../creusot-contracts/src/snapshot.rs" 59 4 59 27] (* as std::clone::Clone> *) let%span ssnapshot0 = "../../../creusot-contracts/src/snapshot.rs" 59 4 59 27 diff --git a/creusot/tests/creusot-contracts/creusot-contracts/why3session.xml b/creusot/tests/creusot-contracts/creusot-contracts/why3session.xml index dbee8e622..5dd6e3c8e 100644 --- a/creusot/tests/creusot-contracts/creusot-contracts/why3session.xml +++ b/creusot/tests/creusot-contracts/creusot-contracts/why3session.xml @@ -1759,6 +1759,11 @@ + + + + + @@ -2818,6 +2823,11 @@ + + + + + @@ -2838,6 +2848,11 @@ + + + + + diff --git a/creusot/tests/creusot-contracts/creusot-contracts/why3shapes.gz b/creusot/tests/creusot-contracts/creusot-contracts/why3shapes.gz index e11c5b3f114491a58bd8f0820928675e83db43e7..8ec0dfb92d3a559057d335d4e98b8423dd06ee60 100644 GIT binary patch delta 18655 zcmV)CK*GPW#{r4R0e>Hh2mk;800030?7i8JBsr2G_-PXDs5M`z&P*`ZQtm4>Xb z(z=d5gIU#i*MA!tvUVG?XK>pNzALNT%X;bz{*3CNUdxqwZ@#SB!^6X={N>l@zr7vE zY2A4E_wctP7(<>wxDz+@072bjsZ`~%rKi)e-w`v_s(r&fgaeocKz|Rupq94o5%hvvV&b%Bq zoDna_C8-auFNb?ZT&GIXK8WM84?7t7@8QFn3nXol{wAePTad%pcg6co_THFwSCwtv zw#R=Pu)5#uifZ@!yVu}4@1Um#1HH)J@9$2tTWZ|rjK#`4B<;7pEp%3R6aajIajb+q$eWj$=!{T`JQ zuc(}OL*>NlDkol3IdNCz#9fsW_f<~3s&e8Ns+{-*Dkpx4=)$jA{@oEpY%(ut3D2~p zAw1K@*r3jErj7k!ujYQK3-gZjiq)CnqOU{hrtyK}&J3GWe*of2*~^Z=`I-%7oqu_W zlLNcWGUsCCew>ekCNHx0aB+ zxBvY5zYS9BWBK&q-Cv8C0N*TsJb%0npPoN{PS2k|hIemQrAGL8RA3m}&>)^6JmoXI z-u49ddLpv!S&~1N`u0=#?T0}+gs1np{JUV_Dg7{ske|-fz^#i*LrF~{Ww*qt8!&YC z*N-3a=TtuZpw1iyC(oJR?4~}nvGa0_O2(*m#;EQZBb;$FMi397DjsqG#XUd^QIkdsak3XKZSlHg|CqKMirJwcLtWwNacf#E3>BF=ScTe?) zQJgM@5yFo@h7dzcA-!2=Na`wSEY+tBj>r=B$#PXB)Tj61U1O*XJ%#l7F6(?pMR%mr!$B6;p4{-|27iRny6aOhGOfSVL(&*pUTIl=eJK; zz`uRUk}9Og3qo78IFTZ6NO4hO!x6M*H$5?yezTkU&`3l#l<2FZJe3;BdY0xj#W@Xi~&^FGPwv$=<4 zq}U$GjOkmF(PtwhV|F{HCz3H6DcdCHg?ybbEqUWdPYE)lCGZI?A%rxjQQ^n4-Rndv zmr8gQ{-ez4Q`j#Met&=VXFIO|XCHo&l!rewxGm?nFF*b`FCe>(9IiH3mZ1p)?IX62 zdsnERhw_7V^!Dd>AKsVzgZkkwe?Fhp$eqwA8-%i--v2dxdUH64XSM_CS^ z8-BRqhd0CDUqj$*M1a||KZAO+Om~+_3q=Npyz#3inKfj9X(0pXmDakL7+9ww_~szJ zi&f~FH{in>f2!e6HT5ZP@3- zuTNKb|5o7@udOC>S@`BeHY$9xn>tTl$Nz@BWwHlX{+s>e8A8X%LW@{d5shb+LL=C( zsy6KcC zNjkicN&^GZs0}QV`62~J<$n@w?W3pQTG-i%C~V8O4;wV}EudSVT2P40*HsZ7~2gwOBamruhAB4g~o^y(K6 zSnfaVFn_rI(~axIP9MfKWRUuO#FJbSS6O&|`|$K`z|J`ENqqH@LtoXQFYD0P_4@h! zU@e%rV4{T|py7NW8Mlj*9R#r(Xz;cN79OEeaWb~B= z)oC+T;yr2fj>GDQTdEf~j{ap$_t<4A(uUfxj}*<8+R^sBEhV~P$?<0rKgx=*2VcxK z5r5rKxC?*k1U#n=9-$?mMzS<(+SGQWlTD({@-&*!fU)@AQsXf1tHOUQ&x2RTtWw2O zGdhc&;Y|8W_Dtrr7zp}KYv@}u4A@@=>p|NKo{3wI8Egi!Bb^50rY2|DZm8>a0gEy4 zr(TrRx`7#nUz8c^F7gJ8le&OEx>j0Cet&6pY$PyXLpry?PF;f>BJMmr}mjnBN>M(uK9@)KQ$T-bz+Di zd#2wZeW2c6C#I2fsTUkof{_=*AcT7S{L~=m6>m-uM&7(CAL0Z@n7$`1B!j@VXB>p> z%)T@DQPR#5<5QOwJD3c;i9Jk)@PBE>YDXn3xcU>!$b?BAj3t)ngbQg9;+`nz_zdw( zYQh6F7_t!lBILgzOAcH^>MnT>_PbB8 zCQ?Dw(_lG%3jZpY{?|*pV#DWXtRy-UKZPH|e+)JJURI#q>$#VbDKQz+`F}-$hpDY^ z1#AIGpUEr$nJa+IQXv=s{p&|S z=)X>#_%?%nx`z`w0j{}W)yYq=?w7>%Ec&Id^h-;>76l$eQ+*nEi?%b+_=tWvJ%9XM zewV^0IkdOw$WP(-%Y=<+TYqPsav9AQzx(xL`ODL%a+hq_G_Wrvr2ngO>oKiHvqIk2 zaK)fpzFtlB7J2;3sfKr-ChXm_xa<#iyUx69xZA}!oQi~vJU##IcYpfZuOFWOR6ad@ z`k&IfH!mZg`#DJ3+ar~4Gwo-hTl4;A%T&^{V_dy2;kD4lmH zeOR#cxZ7R`{q6kgk$+P8fKqvnQq2XW4vm?WA>pDW(<%bp$h32@d8WpkwZUP9 zX|Z&;C0*Zx>FXweFqt9*l?PbnAwqUA23#5Yh~;h%AnN!(76l?dS`+tj@le>Wo9XFp zF0n)_H#?5sN2}}QN2AUTS_eJievGayEa4vW%4WoOSy(zkZ+{zEw&1^mon?j8J4`KM zVP{D@MwWRqb3NGL)?A3y6A$KsM%u^q3O;YYXrycG1lMhH*k?huj6Ah8L*+Lc9eF8n zewxdfHRw4*FUqXUhLZPYvuKZmtb5Us?{*1U^?mg>LprldL&oOEXkhuSGLRSRmHT3-<(i&cH>P6=Egt&1%hWOC0v1 zXU2!u3m3)^B)t6faO|KN0@VG;GzOMelQBP;=_T=ziKmYo! z;Q1gxsso?GL-!o$liy_-(Qz}_3c8KDo2XAeKZl>+{>z8=0S(0e^&cXa>r^w6fI78iA!(qch!YsN3jta~j&#D<`1ss-F9$6}PALczfLFaM#1= zZeJh@RR4m9jX&ThObHfoMXU0o`?cHtdr-t84KI8SQ?QI(xeQ*-Hm)Im?r{hm`KLKC z_1uG!%QoGt1c86E1TvF=IDS`vT80}>iY=;)O@AC0|9P*QuP=t!A^m(Y39YjWa;h^o zUG~1Wa=~?akLy-(aX(LA`&_pQfV<6gyy3br#^dm(TG%SM~ znm0FTKJ0|bt^@s-Q=xyG=xGwsdJ@qc$EKm!Gz=Tzm4SSFB)x4PZp|w&%lVD()DP4; zk>OhM!cL-ZvVOt=^{<}hH!RZ*ay4=`XMf-gIS=O|yYScW3n@qrmViN(5Mc*vxZ7RB@ zxUq#1vH;jqzMkLybNICfN**XpKQxkvb>npZx<#5=YJYS|X3HH%Bz7_h};=@yeUYoM-29lIWO z>^7pXhc07}UB*5sEoQ36?jl@-GDt82jqd+-cogp?u4EncNUc@cMm<8?BVu|HyWtks zimcBcF4E^fi5_E$?qa*ZcasC{l7GWUDBl@v+|kC%v|DK7J+$pdylt}<$m>DWs(;}+ z5M&CATSrp&0J?7jXK|1VLjANjN>xA2Hi#DWv&>&*H%U2or#^+>pV6iHq}G_)%yn*V zVX$b7!F^8`FlP9v`@zz1pnL^3Eo?%Uj<_^;IHsib4X4|F4)Jnf_*izSWq*jdb2uee z7F+BqKrW43@v`*Vk~y16{bF`tH9asJ-}?M4ORNj5u?ynnQWsNn8E8_ca1R(FO}3K+ z^DKop&r-acB}fYk->XYw-`wpG@0+F}qGdqw7~8V!R?8B@DBPH-HJm+z?;EqiYHmBi}1E`8)6`7OsH5g^*>{m8JT^gMtsQ z*Yq>v$z z`8x=VxGOLu`A$)>HdL!-CsWN#wsC~*9Y2S5a(r2EbditdB7faJdJ1fPI-~KW+qc$6 zK69Szcc9Lb{SKPjvfKDvGtIeXnR9DHp>K9V-^_%oL(gz<<`u>hrF4eFaDu7G>hQC; zgO&%LC*RO2e{}>}jNz+8(8IB+gJY|%pRXDaSw5AIe+^R@z+nFRZI$|VvLkiF*ef~u zGkRoZ8?S9fUVk*BS?`V18ZCS6eADbX(%o~^{m!`ZYUndgD3^OZANtqk9+Gb5rf%jY zwKBX>^UKlt)`Ug+eEmbWBDQ^cr=fNZ&i8Y0zMX@ceP+}R#ncVOwC*wVn^B-&jRL$e zO6%@>)7|%`H%961^nvd65ySO2J6}iLrb>&no9F8$n}70ZBB}9CJ4bAXbHrQ9DbIJxb32r0HFxp zAiULrhJU@%#*j8|lHjI6_;RSbrr{kVy}A!`Utl;UoI<1~(=TCoU;gbTy27WV)`q;< z5O>>l_tovbzDiOTO|6Z5OY`0}+6+6euhZsm0P~V!ZxCm^G3qec$S;iHTl?Q&=-t>T z7RGS8Z4AF0@V;4m2Uj~Jx`)6oGMe*>R)&Pz#D6m2ZBUT6hW0zP^l#GkHA>wv(_hi@ zUr4Im0oDz(w=B80XuDPW=F&HW5yIX^3>&t$t*% zy99gO?aO`r-YnirKdV9C!B*jEP1)h;e!`Zcs4Fq@G_jN%eZ0<5U)Su5*eN`{SrSrX zrhohJvpi%dar%osZ?f)Pw>H%_io!B$Tt(N3H}LwsyZe$AcU^OHnsYuo*Vf^6?&&TI z{+f#B1JZYq(p3CDO8DkY?h1pamErM4{Td!{xagRqzN}}%VYWRdi{2PT^}SA(Z`QB- zxqjLDo9jm$U*@d2t-D`e1@2vOUg*>@$A3BiMos2!ecPk;4}$*(!T+yB@ZT!{Ko1XAEeLXW!RkJOG{b57rSnTqr)w8{VSlfC z{Jy^ZyBT6^?B?A78?T}MG8P!v^?TC((6ckSt*7zgqRH{Tg@Mf7Hz0F!lg!NxGT#wH z6PcS|?qCPFOa70i@mG{J#7o^rSvbTkEs+f`jH>z;?Z1GsFD;z6qOinR|AmzORi@5+ zC>wSHvvw{*7_YkPp;%u_*?5z(@qY$oUyJZsmfN}fW}ZAq^;igZ7z+VC76R6>5Y%EJbc==1=gmPT z-(1hWd7k}*Hs9j_+#PWM+~WXDj{`89H~`h-0920yP@6aaJ;wp4IS@b%k$(V7pE*H0 zi%Ia%zt+Cr@jCwT)~5Ao+`+?ok%*)7wVhui)4%4l%@JK{r-jJ&BAe4f zoA;^egM0%*$^@`-?ag%A7WJf5aZ&y z4IJNG*$V|4udkQzlEd(%`G)&dw2@ziBe~6QJ6uFCC!iXS)XoVozJD;V(ofD=0&i5mh={5s$Sh6TOFYg~%B>5yHQrcE^Y zE}8rwnB)-e+x0>wY(G8zXTzuWAJUceY7|GW_j>c{yEgG*>`+gM$EkwXD0< zEC#{25G-5GN1!ca-+#F6Xak$&WnT!}od~MO(fHAQyIhZH;w6x4*B<82^(w;ivd#0l z&Fh7mhm~7yTat?u*KfAaULuTFGqt{P@8u$Gvx;+D#@X~Do9ianF6FS?oOrQ9upKit zZ&T=g3|aSM$a*Oxp(z_(NW%H7`vG{}55Q|U{fl^PyC~K6tbg^x^7rc_F|X-t`uliO zuoKPg8MQctKE1tH@(+Lc^M>IxpS2&fyBn0gY*@SAusko=n#aFGI~#0_a0KicFW;o` zeYU>T^n0Dg=i1$d?uRLwbjz3zi>$Y)$1+3%jluEPsIXXu?JP-qi5e!~T~27L1jq zFbrzwsQg*ziHpeiVbBZc?WzehJxEyh^Dq7Bul5iJ^b3K8;CSJU)|nCQYkjn9c3rXi z`aQmG`vpCxT;JnwFE!C^kMG(R-yNKGpmV?e$*pySy(iv&Zu|3Thp+G0;ZxVyxvT7a zsj>IN6@S=IR~$w9V^^bbC({2gZku+4xyS8$W2B}(@-l66g%>sCQ@<93On+3WwzK_Z z8M9U|C3Sldd$e)w75JQP1PG4z0W}pcl${a-jH}j5DRNV(7+>{13>2!(+E$LMUpK4Y z1EHhpuTP(zo=d(Ks5g{9KoDfj%YUTa?zr+TFux0-T!Ckh;FR{qy7Ta{k#t!pphOSkg6$uki5lDCA|%x23y$Ol~L?&rd<@7p7ZN>Fm`y(eZOt2s4p+!yRpe5`q{9X zzX%1hU(aQOwD|in*U;}Xt8Ji|ZI6u2&uH6;gN8@Nz6}StdpOA5=AdihapEBN%YRE) z4)0pS{=qQ+V3>a}%*-%1iRYH>_hQ4>3@1~$`$9Jk9D%cGRSNgsA9!o-gLluo-eYsV zYi5_RB3I_P5AhZU?UxxwHAVl-*J%&Z@UCgvebDJ2)AVKgD`0Xx+0G+Xt5>IH5dik}{_9n?u`k$P{`19)RfkQak0m^pAeWuZw;ha+3J*7( zJ%!B&L)XG4$mN}^JtE8@G@29`HHpFdj7Tw$#;so&ualLt; z-hKY`^w%;UvDqWDYe?rKr1Kuqc|v-46+TJ_-afS+ynRs(E)8E0_MA8kxLc-H;_LFA_{n*LtdCbcyA}UrXJc9kI z>Pz&DhtU4ZpP#P2?scQ=1uG3F4#M+?w@>e%!(ZS2^Xva6OMl8gO&LjTPS$W!eYq(z zya_CCeQIYjnqt(hn_oN{wvK2UE-H2H{kTPj-$}D$DCb%m!Z~SkLn$Sge`CVyD;n z!mzgWfvXK&98Cc%aJDMn-q4&z-0wMGq-`R9p=lM+?>YywdI~QNjN1FSl7%?FL_BPX zrs(cD3)N0yyD5Br_ihe4?-A;5-9~$?bvWNQ72c@$?e_5DGV%TNdGYP+y*UopU;T!2 zKh_HC`G3TIxVWD!-UJo*nBpE%+)1$qjOz#y?Y;`oKb)cz#D zw-*KDT9P;B3sKr`Kb9tPY_u;$<{xPu$zmw58h^`TFslsQJdHQqK7e{X9FUZ8JTRPd z_(>AB*U6&ZA5a)N(1*7>qA>KOkME$29GgH`4gTWshtNv`tT6d{8ehMH1ebS7%{3&w zB@B%XM=ySoKo?A^A~;%2&K0?bwRQ6s(kCOEMNI2mF@M-Cd0 zaes6N5ZVPYc5!xyh0e{`zZT>EPTw9J-%H|yP&DJ0ei2bGxP5PMJQwSO)AN(#zg)j$Wp~_emIX)SwzEii zy%1e1N4QL)57S#i+qXq$!R1$Db;|;m^MBi)n#KMl{PD}~P~_ds8&eqN>86V*9PYbc z`SjIv6@Gj7_UQKc-K%m|6GpS68oCb`y4gkja(ZsNVAXcPm-kEH-t`hIHD!Hl+KB!! z|9buN!TZ(Ypw-#V%?+=-FB)q{nPvO3Xu+Q8Vfn0gR}%)Oz`_TjA8xkpm#xbNeSfcc zzdbtGp@jE;d;6}#n*AJGZ|0_Gi%-5xTMT0C*7mSr@A|e_uRTrgr1|JG{Gn|(uFkVw zVy`xEC%v)0)_p2ME+V0h(g@12Nc7LD-`{%2(S-2q{UN7)i_xm@Z?9KYg_ql}u-ZYEL zNxAHzUc%p8%>tW)lj`u`vYd7NLt|uYjErZP#Q`-kp$jruOuFim4(I;-&&^4HzGKoS z5?`ZpGZjs9SR~#v|FRGLLua`|GQh7OgTr3X;kd?%%Rx1^{%WG(dx%EZ;(tCd!Fyt2 zb@qKd|4v9_;kNr(m{|=(bPZc(;P@q`x|BbhXR|Wp!{t2=QlfFWZ|k6WvnE$wtu5VP zs0HZ@T-rOPTprq5v&#ZnYXkbMj}CgiYhsO1(*p3D8ANZPiR05`FPLX|6>0F?(eEqS%Wnf z8tigu+G?B&9To0bd@g2j3^D33?@>SZ=J`%t6ThRbc}2-s4DWktqxUHmOJ$SJ{kE;H zY;xm4-cdHyp0fFcJAaIkYjJxU&r0i*2$JJ1#>CgdZG|5{m(^@sdpvbHHxJ?6r-L>w zHNHipVQYA(|84gb2mT%GAKTsViVC{sySOX$GJm*wXTP(Gm<~H}CER2b zON{hp6~mdckYBN91L$CmdUc7O;P4{k**I|((P&62LR^S^kv3OoAVui z&CtEPX>QoO>76U+h73N+prZ`Dyx8t+(_#^$)jfA}hp~@NYD}8`U1b-NY26+D4F|A` zx^LOQ;VAeUb$|8?;PgO~7QX>~(Hh>7UM3#&o?h0;!rL^7W|~AZ_luudy?Uy{reqoz zxYw&e&MKH6Ri^_1HO6QR`y1OEh3+=yZy@Z>BZM0> zaiQM5KtSIo%qLV#3i0msx`TMa9?Nwp0`b_U;_hFz#``mMyUux#Ya6BIh0vN+<_jwE zd}a!GFMlu(SBbkqZAU%cIbpU|sGA*S_k`KnjWm57pD)*<~v2<$4wFZaO<^M+rBi+|n&VI9=pF!0ZxpRXa|RR}qMltT|s zX^ffvO(fNH4CPwx!^5`ra0qlfO|g?a1Z+=^|B<9FLbo5*F@$?|n6L~x-M!0rC&+Mz zL}+?j=KbgJ?%m)1ua6&oU7vl}6&L1G2AmfMKUQ*MWf)nTNgiH@PtPAer{~Wf!@IZZ za(~T$a#&;?+I>8L-3ad+12{anGQGoaUSFczQ#*h7hlO+*&L02x<5*~!xB)F;v8u0b z2RRRW6u%ql{AQ1To_d({olxdz%sJkqe3ZThfBn9ohU*ngJpLC`&3szsV#7F~pmAC7$0$vv~f$`9Wt zv|D6f4>x8s&~M+W@f2XkQ4fRH{iyP_{_ep)x7+GRQMGMuzN-BqXSz;)XPc%I9Con_ zuKpNOe+vm#r{4Fc@unSTWor(vHn-^?jP30AFW)~Z?p{{hzO1;}N9lK&ryV`}|9|6X zI@-Z(Day=<$(`L_P~&I^&F!oVL$BSw&S}~p zOqa}NEtz2{nOD&$D@ot4;O{r^>wk{J;~}l=TXza_*>1dq#N2u30hY77SJt`%S?l(J zHe1PN#DCwB-60-_Y4!71ax;=1ipQNAhXx*X)U#ca&td6R(Abu)H@KKp^E-=T?fqBU*Yrn$$!@-=T4^* zJpI>G==$5w?>{~L_u=BCMe(zFdYY{ft73x)eihP(_s`+!{d5Jz=yP9}<83*f$_;Or zf(Yw2fO41Z|!j?8=hO-(sr`Lu0TE~f(C2N*s)|EYYG>;dNM#ZcPh zv?4U_B1hZr3Y$PPcpY^Rplwts!NA=_?NM|Jxk z@SYBEY4E!hx_`aL0}VEhbol)K-#&(42PUv%ue;;RX>Z`NQ&&Q^P zA>59}i@0RJxVV9%zJIAAwU;*Z@Zr~mV`R<=pWlBhA^j=Dck*ir3;FQtoBDb&$`8K| z#52GclP>Iu^W`e@Yq@6wEBD{05;&IelLtMJ$G zZWMju;0wP#f1Cti4?`N!lkK2 zO<{Ie3@*`M!1S{V# z(xg?VL=swJoPX1;6>?G?M+fyw5QBdfqprTP6=!ml2t%VFidSQ%i-YS8910mMih!*~X0z|TQ_w${h$M8hhEwHTf)hf<0hzQR0RD8P^4=n)(~ zf`dnJ0#E9@N3ha2^9WX-qIbnRk^m*=Bx*is^g#maYfX9DAPX+;fMq0{jtK1-VPh&K zTa$k=j*x9GuInt`-33q1KO`SO8}GR?MIj@xeAJW@Og?ROKfEkQm$Ly5&da3;(V+s& zC9}7M-553R{Rq$7NAMCItslYjBY1iQkB{J`J;8^61Sjpjn5K;2A+SsthSmZ&|oxBDf@`ZJfhN%sQ3{T{g39( zHOX!p$-@8dDtZaXcVY+F2A=z0!o(qN$!bZ{VXLP!6%L0(76~SC`2aIdey4HapXLH8 zfZA(cR(d^Tvy?nUW$!xHTkP^&gMVXQ4b3)V9Va{UgoX(ul33(a&bKZ}|K4vTTA+W0 zE^8~Npr8aSLf>A>L`%#w7XABrf+-r4HzsRL__H)7ZcNnpnUmVM{JrC6)>9YlUH0mN z(vHmuvC!1edIfE)@oC2&H729&a&F|blJ~Neos89bed~hpUihTrJG&tR9cJjsIve#F zj=gHsJnvew+NT|#HhJZNZhnu#kT`$sTB8FCHE-iMWb zhI`q#Fm5dNM`DQywS=TppH;1*IK`Y+fEZayIX^e1Qg|NdD|53N8p4asvZ17!#okI=xp94REcoDe&psUOy|okd^bz<$AZeSPk>efUE?}ul@Z+x1dg0Ye0~c`@{a`t?NAM9Hcv4-l`Kvk z^ywBo{n)=)rLpoKovG5dP%6m`I;hJYC{zNvMd?Mam{jX4aINt&e(Hb6*&&CaO+{rT z(T7~Jyar`KNoNss2eCTY$tqd<>ca7s2hyv69?|ERy5}DKEE5#t_cBtCbM+?1uXBhd zKIEz%uuj01DQk&$+EVMSt(u@8Y@&?D1?u}GL8W1NS!I;5-g-mRR{~0r6j;e-j=AO- zyY~&nqt}RUDG!gv233FLs?&~#$?=&a_ze%36iZO4zvKGLMsl}Z#2^@dxk-TgooW5HH6N3c z<3y=*^;BSIzQy~bA_$nTA{A^V?NZ`QsX1703&!{9A$Dr)FG2T?1@6tj4c3jj8GJ14}s5b@&06qZ6 z)ei;Q_i3Q-_eFn)XbopHUo6P0B^=^j;|(p+_>ZaIUyN5cxyGMcS z;hE>KzdfGyh%UO6tZXT)Mjc(%-SIJZOB;;z#V^L=z*x1hXJgzC?v33VyEb-dj5Hj2 z&|EDJTDlX;wWL5-p<1c;x@V+Fesg?+60ExpK_`Tp#N>a0Dp=oR%XrKFLo6BH6e`be- zZoOk>z94_DR7zJS$OVRU8-rvxggNIvXQWUQq)6WBKCblzf((kaHNeOyK0sRx)K3d& zX>UOQHz8{Bj8U7Ee9lu!G%4N$WzO$XDpK%w(xf20YH@^$7d2VaVlJ}iWol6#@ht`R zyW_9roO+5*S1Oh}PA_E+8fHA~a>FQ_P&6TLLiT_6#wYwMFXCiEn~J%P36O#l0EeSa z=W*F_c((j*{7KB+eKQl!3CY7bR?+&6D%)G5fcE3x9sd9TKslMDv#q)7(}@5{hR3f{ zJ|f&is0lu;Fb`ata5mv+g3msZCTvX@e<#m+MVOl~HF`73Th|i_`G#Vbe zQXug!6*HDETZhI9?&!`a52&CPGl@5dQpA70RLpCn?%DCdf_qP_1ob-B24JS2D^oIU zV$#I8iBS^+yRkOWY@*Rby@^^A)g~%Ul$$6u(FZTQ22Di|E~js*vpo9!-e;cMoAA8L zesg@Rys7MzIA(2P*~FrWc@vajf6M>@M&$hE^LWPB^84fWX#p-QjX_unZ}b^FNW}xz?tK@>5AU6bCgDxOngsqVKVA0{ z+$5+;V18>8&n6x}UHjtx+p#a(hHrmGK80L0QD#1Sn#X3HSL!Uae#zK(;n}6nZH99C zLbv`tgzP*NMpqA5zvjG$5Y|(rn*l!*fGLWub)I_j8@Bx8JM@dhu2ib|@y!A9+eGRC z$hL_#s&}XDPw&z%5<8{sW6Z_s9Hoq`qt+2Ev^qjuG zk>hJVBgdlf15O!Gt&=^`97Sq10BybZYL+hOZWPi~PlJq5G z*8$B9PxP;^#b^RvMF(sl7Sn%i`jO->89U37!)Ko%r^9O@lL2MvWa^dQ^KMPBzRs`t zj*^EMuKhuAQUzaW>yV5=0uPIO4$&mP=rd;oV@-UZnXkQ==~$wmm3pcD{Tl!;_chly zy-3+nv+QcIBs;nuvw~TY>w~0U%a@H`>ndgJ9erk>(`XLMQFH)-=x=}f3glCNA!qn1 z=g=SNLz-zJt51^*`|g3S6fW{!>*$w02OV@q0JiY7kGlHwiq3gUF}@AMI0r#~`wO3k zr}Z;pcd-rDQ3r58s(BfU-}v%-9`fbS1&}?`R|Rs;x!c z9>DFh~x_UH}+n%>~3QUitnX(pC7g9jMNt=>1CHN>%(!rdFF`AB(02wyynp z{!N>jG&Sr)P2r276?kxmuiiLIwZH-lebWJ_vFe569;Y;QpnJWkTT|DjE=`@AIyHr( z#(x-m%8sKNl@_f>z!NYAo6$As{ubYQ>k_2~KO zag0a6GH6+Nw@~UNsEdQGwbS*^$LGfp6O{O>1AVIrT_4k;t+kT%bM;D^@#%4ZGn=P! zKfPw6d|M>dKmYn5+Tyv^ROpt*))Z$o?!Ky5x%Xv!{{6C7rkchAy+o9v z6Yknx#sYs%blu;@KRph%M+Cagqz(||7GgM~5G)A%wnS^%r^n$y0v>$v!9xwkIWTZ! zJ9EssE}2__9RKX+2W${x(BNDhFWLzmSpb<`;pund;7^Z3c=eJFc~d;5AhGL7a1!7( zr}f@1`sr~bCm!TmWZ2W=2ArJHgcpk(y6?o0Pmh0NCDTx$p~~k(6fO@u+Ix-~YBvsR z8aG$->Cbnd4@T6kX!?Gzh-AH}GW(fy@85`~@%i^~;FFzE_?y(NNbOPRNk~Mjb6eju zYSZ}q_YFB5?OX$F?egHlbNI3WaH!oD7R~ZUVgcb2XaJs6a*ym{Y~YS8tVf0OL@=wQ8 z9q3(Olh^7w*szK`T0lqM*5C2yAB)G=*uJtyT{~fMd3=KO8Ox|@{_%LC&q~Lr8|cth zD_~euXi>tG`@X9y-Sz%|`&*oav?e6y4)lLa3~{mSmZ)Os|LL*D@!eN>N>AF+$P72c zu|$UCEbn7Q)9OvDHLcpT%IoNo9YYDq^#f{Xg_+ngIA>9g4?W0_`)w-_zs?G$g9N4g zIMX^{ejW1nH&gz!AAGFKh8`Txd)MW4oZxu^e)IONwfx8ZkooeubtlZzm)0J@33q={ zm8G}7^S^1Re;kXp4}eW%b$D6X;z|J=N60AeHfN(>>z#ib%W?u_X}(eakg#06*3R7F zpm#Y@R(_4ouoBIRH!IexXtN^C3jRMV8!-p4;i+J*C`_KUS^`pi))6?a(Hq%fRDOH> zBS0DD9^>QzfOZM$#D%xX>6hzk<=21n`gg`JP&GgHi3}G=-JsF-wO!8yEbGQE&4{r+ z8Dp0tr=Wcxa@r|nEvosLDt=sx*mexC$WBoz=w{qCfhI#T3$V0{z&Fxo+rX{2z$s>h z^H>>9=dd~aVQPG9*T=RJvZTaA=NnNXc|p8b=2(UN8iW{J6Ukl_GlrE4XN!LUqtB=? zhU#FtHOUReZ>Owsi%EbuqZwBMQ`0BhdOT1*iIv`}@$K z8%VglmwqY?iAI%C3c%l3J1pZcx!1W^Gl8wPG{f~RaKXkgYctLlmr{SXC$65X;Htw_ zb64wd%_+A|_?-KH7{eZDF@;b$D+)X>w!q3-_JJMfjU#^;BfcR?O#CIg6y(qs2=hgR zdJx!WG?2x*xy)y-{zDuG{85l!i6+b;Pc>X#9dARaGycvP|M+*1`U>vgSh~SX@kn*u zG)DG^rr~+73DssQ&6IzeDc$2C0ip<9_qRCeG{7Ss+*pFCqTQpzIP$!W8=v|A#lHK@ z`WUa$IA=^G+5(s1fuhH64}z)x`@U+=d_&SctDlpzqB;+cM(1FGc(TsFo*%zBF1UA^ zdq&tc*xDYNBPesvp?trE&7zrkGqYy+jbXhG?{&Q2@r*T$jq$RX2KwE9ET_n-MRRtB zH<+#AC3E+rZ}^jcGUkTeucv|tK57;ww6MafGrXMJ<6_SL>zD?oVaG9Rvv>Zsjx%9l zhe-I}f4CC-}bO*CyiKM~70i3YZ*I(K|!y;!f-bt>_<#Ydmm48Fk~`RXAApv-S))_uXqH;*ZC*9uonnWz2KB zl;tp=*x;J`*q2;sDb13bCB2S!2Abv+SXUA+G$cbk1X8YCJcDI_G)r%m)+`k|BM8(B zENWrD(e(`9$@84;XS}V+xml%V75mp_nXd)X=a}9nobx6$sI^a1CXt-)Yphzcs?Dmr zbdCOq-LSAeu$idcyJgJ@Q0d#kx;CrXtVXlyFRv@-Se?Oyo~v|VTu5n#JNvxu&4rs6 zYF^4S2g6VKovA0?FR(?xWB7IM#Pq^U8*Is~g(7a0NgrE#?GE!0~on zE!n(8^Wx31KFoXp#RcNsG)usb-~?@s9wFV@^BSiTHGlT6uU=W@P_OD}7%OHV_IYTB zS;wtII7M^v=I}cwZBEjh_+@gmz$2X%h$iX}lSKt@NjbNFcH|86N4jw`#;VOJUs;fl zI;c^v5sTq1nMECIq^0*gk9D0h?0>a69OI;n<$xE%7JCQmb0&dR?6741KqtKxS$aKQ zKuGkhX*Ev=+(C+!>#&XW-1lSWaw)yfaspa+mgP)Z$Z5?{ZXJY3Us`C`sqV0}sjv$h z2J7z43^N~p`Rg0$S--#BVD^X7eAW?CJkIU}myfh67aipf(Eo04Ubv%*e@fZzLr(@e zfg>bDE?UPQ!YZ_SDQ(Bw1Hdkq`{EF0d#;BtUGIVn41SU|DqqDxRUybJK z&DCB-`#yUO=s

PzcP1Z3a(Z`Rh7_z2;eK^#zysgWT;RnfMm!Ys!1ve8CyOA2E zLjCPKI#Y>E{U}?FyjO6Ef_X@vkYF@El zZJyaYqj~xZzFyO93O!^SQg|LuZ12YB$9;FMU9|*B`!ci$X05_N&cnHm`RM*J1-P-d+Nefm9@Yf z)CX($fX&Lqz<AH5O&2>f|0qkv%)zv`|Tl!w_#)DaxR|<@_bHuEx!v7MEJGJLX*0nFjJsvDO zwk^uL2wr5cK&a5aTh`%BQO~*C)@R#*rx}tFzK2FEK>4dufX7?wy?%o(&X&euxNgMm zriEkKW*Z`>8%$>>``wl<`nCs^gv8k4*)?Wv%UT(w+xe~~1#s;}UjG9$!+GHiodEzT CnB7?b delta 18567 zcmV)7K*zs{$N{p)0e>Hh2mk;800030?7iEr966F8_#R(TZ@D{(0%#ZB7OBQ)bMwp* zP~8LU3<86F5qPaST`DP4I;!rPuOFDZlYR;Jh&Z~`?9SGMjy!lVl14M5(acExZ~x(U zpZ*knEuVh(*Yfex(}(x}$M4MV{=@%%3a>)?%dcgfbCp&1ktTW@_PNISpQSHyz9wpwI z<*RjMID6B2S?Op_ukaSEcf67l6I@@j(=+a27Z<(7yVdfUbgn{bLQo^ z;f#1WE=hfOeL37S;yP85_CXw%eb~Xse-9ttTp($a^fxJW+JYR$zAN5$viHWcyQ*yS zwmtsafYtqGS5&*--@OLcc?Uf`80bazet&nG-BRN|XDn9cA!)z$ZK(swpNmPtM!1Zc zz=An`8h@05H+Pjf5+JLB_ca=xKfHZ<|9n>MyQd40JCi?D2*=zVb?Dw|7xLp$>@4a@-cDopRN0E^ zsZzt?PlF7;Rp5p?`qLnJuL0Q+x-Tn!vj>-=_J008RPe9R9DX6q!HVW~X=jhVXL@^i zm46!~u&C4N>}AD|h`Ckyr{k4=UF6n2;h&Dz_(hTX7Wiuw?&!yjrTzX5%bn{Te8GCR zHU``+x7C-(ZTtec4Tn6mN7;Y8TlikBbBkCPm9C22E9DOuZh`B6Iug6vGPn1b|8yjL zS7q*!zt?Nr)0L}Sah>XLMRm6q)j!@V8-H)rx;^%^_PsH2_#D(hj(?)Rvi zctz#J8!9JWS2^*T%89!wC+@18xUX{JRh1LJQ02rgP&x5SL>GR|^6!o)Vv~7EOL(R& z4dIzK#s+nUGi~e-do}kwnBk zoE+F~mN^$A_v3sVG-L!;!^#fGH)-fT+=xaZ%()BC?ldk^j7B-WjG<^3O@{}lfERQ^rS-`2dp zzWwLd|80<3AIql?@BUiE1o&q8WM+`;{RdiHfNk@PA{C_-6JDoYi4a* z0{-n&mQ*1{UJ%-%#fcPoLyC(M8;+ngyXlFs^qbw(hejg0p+sLL<*C$2*7IZ^@F(o^ z=atEZ>yr)p^CB|rj(NEdb<@0z>DzhP5rc~s55(Z2#AaS_v4C(B1An}ks~>-CmiOJ{ zdA8bzZ6AKc&{|k}l`>iHzpDBqA#N^$2Rz=^1ECeXMF@1A5NKI{g?HZIo%cybpUpia zBgOVeW=!9bj6NG78ME6lJ&}yrNZBSiFXZclX~`QudPJPpTd5D@PGTWKihc)IQ#IEq&)ng!EHImefjanc>&pNt9_#gtZz7lYiZLoye_?Zv$ssL{^0S;n%0DTzISSit1M=T^7EH(nb$&c2j3Wc1&yt zP0&6#)!*zV&k))NE!Oj8712FbDKvups_K`B|Ke_%;Q;O@Uu+fL@1RKYV&lAKvGu=cf%^c5KT5?nvOA2#+gn@q&=12mj3gxGc+v4hNXV+h-7 z;-^rzO``aT&)^%eBebtM4eYuNYzq!zuePy`Ahja&<{-Tb5$u~-Tx%OQC}2A`8w%LX zoY-M*!|u1igSEo^a!C*Ur(gecL;O(xDGpIsC4UHw?2}VlW%@+VgtDCH{&i~eBF+by z@in~-^VzLWV0%S-YCJAMkm7S$R~$ng`(*T`2-RsbRpRJq^p5;mfNiN>JTCf|HQi$u zwn!Ul$39XtTWUw!^R|@ehBe8bNn9Q)!XDfv+eCCj;l4UhC*V14aNaBdHIk)SDWE9uVpXaH$_9=+8*Bi zGHmqQw(U&Za?G&3m(Ale7&kRJ!*)Ymw+mS8c0cu^tkw<8F#Mv-Sa*>(7>Cpa{Lu^2 zTJlQ^VIzS78`9au&tL9Cs<`&_F;az0&3{16Kb_I+jUCN^RMc(E*i2cdH%LW0H95n! zL*3okLOUZ>iu!c}bB0@#St51F8{qp(qzC^=(@Ixrv`?$-}Q*^5Dvn zhu?e2!@lI~_^#WGxoH{?+YRxVBaej_DzLnW$SE-v-WP4S(BC zd~6>}BSt5l7(TVnbQ;MxRPmxul=!L9aHtbQ4B0dN4(S8+_Bt_*q)WZvs1l64AhsLS zcqDh^wT|@& z_}#A`%U_;8mAhoarh$DaA%Fc}m0OQ#HJTOjzJ@CXG~-+uk@{HOBi>C^v|-o1Gl0o~6*(%v4ae4A-M6WyBk zH(REXUiE>uO~5SQWP5fX;3NcR(OG|`v*M>(7I-+*u$!3oe%qe*4S&Vh7~`2~Zj9-; zF(%oY(XugyodGX^^O+Z-im!+&7E#43QN@cjmd%;%0+PJ~$qFR9?&j;wn$7Oa3mo$m z9JAn<{kmtvHWl`8JO=BvKnAtDsoGOKUO?%*OX?|v!-eGD93p-2NF|y2?nSbkX0k`Htte$u<7c|m7 zu2=AR`$Z#NV<)(7lfym>vSs9{r5P%}+33hiiSyH3&a6St8G2D>Wj2(&H=9L!BxK!- zj(oRE$g1zFui-piMQj|0YlWrubR?LTaSw{rnt$e)}&U-V4aqyPx0wmk)oDFfiz;7;po4+Id}p&2Ou(#ldRYXp{Fjm~tp zp>Cto&3|cVTd$mewyS#XmsZ@K*5mCVp2M{aqq}{9C{XGng|PiReeHAIDpu__ z*YSqy#vq`t4g}Oa5Kzxaw*mq6ULfFM$lN7?s||reCvaG%ZM<0*1U`j@*U?ugwA;fSr2WUL0kqg z%zw_b^x-eRzAMiXa5t1$#NN&z#Yy$%TLBuD!41uun=~JGqFUE6`OB%$zfJTsiD*5E z=#FF4P;458jqu7qzCGyOwhy=F6`1Ax#&_xmYMsb%EqP%l(KlH?;eh&APxBj=X=kn) zIh!-^hMb3^2Vk1#cSY%YiFznJ)BYkDs(*j!jRROUAMqSZqBbmpJ-8NobnSwSM`!!{ z^6$?gXFolcUq3Z!p2JNh;6t&A0LP+lmh?6i-BR4x!U$Oa>?vQ*Z~r;`+9N3sl%^k= zO}524!VpY1>wT**D{~Ym*}eMasK7%P?Nb-&poY`9}QP?M?#Z2|!UWAKK z1_?%>(fz*;kK(<=m8_#4skKVms7GjfL`*MYH{9Y{k@Zo*Mfw~l(PK=}U2GTlZgQYq zau^BaJEM&|+IX3E3vIlIw*82=ZGYARc|FQn^)Flpf=pp?>rm?+K=*CnEY4g(sGk<6 zp6aLB2GOE^miepfCMgH+)Ti+KGrBY%sv1+9xz5ck3>J+sxbNu##tc7oKUf;hey_l$ zg-z(v5trr;$CT8*;dI;2Azm&FAImPa3^8{O2inSFi+u&irI9OMmR?&jXMZ!PU(61y zrUz!@Tc4k0iFJWBc0t@+>SBs615N4_?g2xj$##-po~01yS&Eml1ZiR6dv$5-o4Xz2 zebY2VvzhGN_rZm%kq z;3;8rP2pnXd!;6S2VTX(6@T!z5VEYgvQ%GqQ1IdPnto<{{C->K3di?a*C{Hk@IC@n zuaDY46K$AbF)q6BG>d$ToPW^AKY!@sJ~+o~&+E$t z>jqH`GtE6-fM*=dISVr4Yh<*Ab%TD!;ui>B2L^2jM-cJ?ia8U0EvXDGo=LB1Wazuz z1Sw#nibH29?NY@K+e}nJ2UM{S=YYCoXK)Z?upAM($>BV1Fcui-ISWEiR|#PQ>lPsl z#n-CpmJrmI5YWAd5P#5pH6cigXMznONZ;2g z;(aD#nftbZ5ib=aLu|u$79p$9h-2Y#ZHseLY;1Noe+PjPcLjzd-zh5AhHBO9WU86T zHjc2p^XbrzmM;sAF7nY_q}xYNfvrzxG`@8E*4oHt&XfHP)PH%h-$8R*b{n5-ra9Lv zb8c-Y^vzD_o0)KR=ot>qyux^*l+JJ%PB0Z&9ex&f(DK0ZAF?@9hdN@{f zaBS7}^Hl>P%ct`3uVD%U7|dV4ty14kcBF0?dnHGIMvu&FhUE1|9}<@ru|Zin*hhVpEu zynetM?UrKXN`~pq)h*F1vKDmHzxt6rTA$e?XxpD+Pz=n;tZ~GE+k+eRA zHD@o53tl7+=G>?E@8y<=o;N|sgWmJwkJs|!XeQnmgtuDIuvgj`(&kMP+%yPZ4t3Ww zyo01y_kUsT3k=7EQ;5`L`XvnS%fH=3SNN3F+K@LJ;%?jSzPjDlS4rxkskM=BY2Ld= zn_&m`b=n*bU|v$}4dRS9Mja*_`GqljYyTSzy&D_F!Wd4sjp3IA-ZzWy;A)3N_Yn9+ zMsr@#%8+oISO&Ze3i8&_ey5iHP1?RjsXJ!+D}P%43rV#*z`9}fmL>NVZMSOQT>6Hv zJYor#$1i8M#J+9q>BzJtpmuh=r#q=N4UulU)sGBzmtc>(eYvmSo5g$SXEo?M*eX1& zDLXvfPuOx4btOigCYF+;kJmZs>zaKLJB6n=OG0YQbRT|}hYTf7f6?bn*1hZ2rrJhP zSbt`XtLQrM2425+cVDvNu4`^ibIxby+B&?>J>6x&UsKV1K>99Hnu^~?3E#ZQU19LF zGCaPhU&C7q7afz-m-TEo%(mxb(Ho~)Xd*SCK+LyV2xyc=NSHPm0m0)GR$ zeoxvTdUhta^)y~wG&$b4Fp#*{))1Oc&Ym+ z3x~L+C9>g#QB~if{TER7rG@iW6qXq4zmT%O%G7xeWy4Nj*3Lx;<5hP(6zgj#8*frJ z-k|Jj5nju3JD1-~lnuXJpY%&~et%uq#&;6`VnqJFg8%Sb)zYbWX^Wg>Z+l5YS^GU>yrVEfzwzSO|UI9Axs%_3WGH*-vQmJr2O#5eL9M4#4y{ z0JDh$P(2Pn^*8{vi38Ac9Dtew0n`u)u=JS|w6mB55B+QH`yH?2A8&11pMS<3JggUq zI67b3`9(7QYfjr7(WQ1;h-@#iIW0ske0qBS$9LuV!~5}?<==Yt+u@{XdzeyPo+@By|Xmx@GI3K>g2lzOiMFVFx z`(V4jo%=yBriV3c?jAAUAb$wdd5IwCQ5!vIV?7x{5-jJz*N<5I*;hwQpEZKBC{$>ayYB!_t4t`{<4`{|uN8$P}N zkglv(qd0oK*ZUVkxw@Xu%jtTfxdPG~90cI2W!Rh-*0&ZZaHTsOgXDTn3e#ETVz?U=E7n?m6yHefB4IvHw>rw zto@+f-JtYk!`k(R-|I9!*X}lSKTOf2V~#g! zu5|Km(#$w7_N5if?nLhNM9_NihT>H!xH_&Io!byY>Tj56-!F~20{;7;_|1xco$&8) zOO#%uitB2r#eXgNb(9#pZ(^te zR{Du3RBHPS(1Cse^UYJ=@~#r@QMSBHyLDFykBZe=wHc!Ghhqi5ZHZ>OzNUp)$=y0# zu>AOAYbuXg*mcEV0i;J0F6#HDhQ}WEx9qoItTcsTP=7;5<!V$>>x$ji@9}lpFX%bt`W}CKsfliTeAl-4 z?%=coo%{7qZmlEiJ@NK)+n-N6e0|3bpSsS@U1jG>jlCbPz<#>oDAFIh8jU-V{)chf zv>VJlZhzk!BQ^bzmuZ_Tyr?0c`n4cr`lC{{o$W8nn6-K-soUe#qm65?z~^)$KybVd zsHuRV?35T_T(w?Gk()}z_yG4|piphrwsKtkx>@}m2pv^_efsqDT=KO*y`lU8N=HR+ z##>!phcTyKCiQm5m2ZLhT?pk0gxgbc-Bh`q`hWGy6zieQKF#ImE@L>Cxlg+zn!0}w z&Uppr|8f)BK}Yu70c*~=9M@q(JG#|K5xcm%m&&f7@QT-dRdN+PxS*eVLfwWwENk5t zWcPjBKbV`RP0EDg7xs5;-Cs6+pP7HB$17*UwyoVh-*7^F|NdTc=3Jx83qSS6(2g9| zUw_GF+dz&xxcp^O=BkW&eLRv2Pxl&Ko3|Agd3XE1zd)d0cNpHc^1puBs`PqqU3(E< zx|P>Wo`JZRyd}hDHe2pNKHx%kKNo&|@4lSp4vA>PbMF5)Jm;_RoL|3#vBPuz8}ZyE z$FH;6+K9c&Vb=xfxWgiQM{wak80sGk^?whBx|^YP*SO=o+v~mE-_1~#;Q^5)t&8LR zep+|Kdm+nc7CSw+yvKl7FOB?0eR&DrjZGfW&xYOnMJSm4dM+EJ#ow2?hJK$}Z3D$@ zdt_{WM%zvtG(0NyZ8*r?!$Iyg2VE1769>6pUcz#C*BbT@hWQ7>{DWa;hPg>Rw|{KE z7aP82IGM`b7rJra2%Jr;Qn>g2z*}=4ynE*L9-H%BGrNoxxiZInh_^UszsxYIDf(x= zPJ57scTLmogHHdLroY=XT|@xB=vkUK&*d-cXKAQ;uIY?DVpyW1-n@VQ@Maj(P@J37 zikr`hr{Xv~sPvx)*Y!};G?$xcE`K+36fU@z+G8VE;e@M_KmI6hbcpx*%~8e-rF}rZ zGalA=#*Z)NtdiPIW^cX)kma@Whc9Mbys9GJ#Jv}@xV@Og&8-TDFJ^IjF^lIHvt|-# zFJ@7Dj)mHbS#<7h`~G6qT(7;DMeW5b8XgsTb@mrz1L~nYP_u}zo<3l{m46GR6@bh7 z_)EVM40^rc;x?ca)dBbSzuJ{$s$E$&L@3N}YYlDbb#2pM0h8;=b{?r(y*f3E0I;w3 zU$3%_eZl_npD$jlI&30+EaABXx$JDd?O=RVc)028DGc{JNEj-(Ag2gW$z}S(ds%;2 zT$L~aN-)+PBMe|X#CJz;!+&@+%Qwfu3*owbu&zOM4d~^YU_HjQzl$W)^?!%=e=JvD z=~zWePY&`oyQ%Y?X$N7^2hrAZ@(iJU==Nb(l4OXpSfxxM+h0|El1o3m3b~YD-~Q!8 zF7IURc@7_+-@g0sM?uIstGv%GKmE&^T0?(?Uozn1xk%^sOuLpmQJo%fK= z6Vk)0@KHMO_Nn#Y?YknO*m@6TXWgnTsA3V0vzOWhthv(K?)=GfnnP<1Z#`a#j`6np zTIH%=dk^5P(jQhtKYu)fx3g$3-hbLz?e75auy{jsB8Bp63D46|ZpoQ`@#LG`)cF~m z{tnJ2l5PkV5}tmupFBh8$4*|)V_sGfQL#$l5$so0U!rF`g!W(l{B-qouN!4ASZO$M z5S~B0eR}^K{`&TxU;j5*QvPYmNNRJkhMVfkO_AYEV0r6PJAa$e6r* zvX_s7wd<(Y4}a_~CVq&tQEkyzZck3^oE{V1TOSbprAJNw0sJ5KYgCD ze&w*d7TQv)wv8^b7VYlS%&O)X=)61aZ@v+nC8ca$3jBX&PPsw| zJ*d^RsB_bz&dpjrwWF{7zmO{;)@*EyKgQ+RP;)ZWLHEX468;$cfPMR(6xsCE+DP2uyqcXQBrk5G5( zHrivY!}-3c@J7XNw}%gxiSMV+i*IM|&2hl~>NlMGu~t~mC-%d|{cQ0jsJO=z_mJXF zialUlUw@F|?u)JKaY*2|9?ubOhq%aEjIw`qeG1n~Q@aFvooHGc-v-X=t-oKJ?I8S$ zi-^!)`z-_Of0aiU$1fbF_9ywhy(k#hlDsirh|+fZu{4omqkSnd z|48#l7DIv6SQdj>W#Hy%yy^A<)a&7Zq>ST%;eVXNPm-{`P8Rk4fWpv$KD^x#g`qEf zdV6L){8tL6P!HGS<$q*wta?pT`qdS1mE|9T{vqLO&ZpQw#822wn z1An)-2HtRUFyd8+j||X_U-sgi&h1d$YN$IHxx_<1SAzXZ2<~uj`u5=XUJ@UKq8Y#R zi->x`?R$gcxmX{Zo}V25<@zNnyW@7VEI1msokhy)h3Hy2!etVDnBE%NzAZWnF25S9 zTNb#S-~QAr_AlX&Uv`Hg?{40h!YEHSU4KmBaNqsPr>~}~@Y}n$N4L-KUX`<&Fq$3J z(0#bj%`WPf({tMetF{Ziyk7$Mu9sM;DeGg?M)Z&Q*Xy4T-me}9ti4{Z zYs&DlnVEmR{<$vhPuat-ZCkBZ;}OEl6MB(%v!U^3c|rT^7(<8_;Kc zbkOr%6KjN;7J%Q(AbJZ;9G@n8!92sONQ37lC$Py0yqI;f9Qv-MVaxS;&GiQeYD*`; zRaC;X6fEOhbeGrravv`Fet%04uwZ!ZUvSCrdPNi67%>G@ti-^rfzs`P@_KIPfnMC< z(4nvNkcG*Oc6eY%>(INJh*=V;T_R_}zHffMY@kcIJ=%rsN~SkP>h4)Vu~uKIDYw+o zpQmy{vH$tcKdAF!-TLL@$9oC*SXX&9($)TAKeRZ+!dxsF*F^bE3V*Wm><;=6PWsSQ z&0`!cTwHz8VXo<>8$^fLsqIp7w+6dipDrQI8mzg{V3$kNR^wdgsBq8Xb1{o!h*5`m zkNUYc&v)vY_#Ji4D@w*PVT@dh+uL|n zTBk&i9B(luz8-EX{D1hltY+id+a}pIDlQ$eai+8N5S8yvtIzG2b#3_4d{#3 z@Q(B{@u2tgvVTq<7w^r|USDvP_-e%nGe<6Eat|AHZ}wTpKkPFt9%v1_LhRzIb}`TX zVfX6i=O$gKNtewN-lj=3(AzJIvoh8F-Bw9-`L(L zbngqeg$4Lh04-SgkaEn9K%i?y2EA*$OIfwG17w*kwSRZ+;yji+PwgS}-Ej@)7Dn}R z55;{xc8ILqVF)r;h}UNV$Lj-M$>D;217UX_A>5dW3-#^=0{T8-KA~b#hqXGgH8OfqA$}+!bm&>haDAv$aCq z>?pe@%zxHyr0MJUgxNY4>Hf1KYX7W=ddcaVmx6uaah6-Kc22SEtpHa|^t+pxm7`}F z!@HO*YO_Ucwy4jR8H=`=(ru=6n<>4D8f&jYtOI>}YClJ?c`D){c6yz$4(T64U{@)A zxes2LH~cbO^d1Q7p#Fw|fByV@4GFJ8$oZojdVhFIW6bn#BB`chDA#fy9=5fIL!jen zik;*kV0&`>k0f;wy8W<@A>6aWgk{+2?p?+^L54ddLetwa?>~ok@Ba3Gef;q2`s~B5 zxGVr3?ug|4)DV@ag&g{P6D+Vvj;(Wi1g+MbEqc_WNOBRcI^Ax(~-gRqYo!({=JY+ccfvu!~)A^~aF`n*KYwS~ zdmETf4_lW zcN`uMX=UHKQ;^Gc<0T~K&N~mVoPXWDveq5QTDK3h*-ADe{`-#X4)HiltDnb`o00TT zJnqyuH1MdSp6!}^4ok0s#y+45dv@D?;NgaFaul3c50bz+lL#n?PhgUw+{mE=>V4ozgwaE*MECF&|vdOhtKc- z?PK_LU;;b#y1TD8duR7smv8OkG`fKnv_8b-{>v)xYP5M_Bi5%DQuVYhwTj*e?>>C^ z^XFd|Y%&@fmLmsPv)OQ-VC{-&B#mOKW)e@aw|GG3SKO??0B1{uJUn z`85T2eE9WEeZA=KhksuOG8kZtNf(yE`I?mXpWnTklbhh#vCAE4Mcpp9j;3n*(dBxw zcl|}PdbERb=L3E4RrqUoHwrOv)rDW5KTaa82NVsCs^em_gY^%sEx262`egO%Fq%1R z$Ao%;Mzy+b2CpFD(rBWluD5{H_H#6Fj05S>O76`vwGGYv;TEDj+e4A|ELcNSCyn>L ziCJQK(aZXxv(GKa8-K@(aj4zb<52sr$Kh~vMoXgG@E9bUE zL5jKBF|rv947?@&*i@lf1wJCwp*ia-dRrh)yd~q7wOf{lAoeQpak8;&N4GhFoI4!X zRf9uWP;%spSW9FNWAU;GJ65Q4z$plO7>CFmIT|TDBkKW8v3~{%o^y! z%0GAnD==hk+#?u!N+e+-#!1MN(NzJJ>{#q2SRp6Xadc3>1TjuA>gp?7aST_97BmW? zcqnGNIH+GSvVW-oOaKX`sV-*H7(fipF^uPV2K*eSJCa}{=Oh9?Y4kyY!=E7%gKeC0mm*j*x9GuInG(+yzh0G9({B8}GR?MSme9v0~Je5{&+7@cwRiS&kuR z100-}3l5?~1(-`_ZwtFI0^ZvZp4X4y`4K!lg2zYj(r>|oe+1_q!P!S}(yo34$B*FX z6myp2GcLH8As0DL)I$z3OXs}D*TV;&NNwW8`;ADYZYDsa!%|3+rYU0CA>I9 zNtPvbhpc{Aal_$Iw?%?U6bCT##2+OE_-!Bna1XX@Mmghz2Y=h`>^AW8k5mNIXCiC$$Qz#PR44zzBRshUw+W> zo!yX44m0#uosC)x$6hsRo_F0C@9GaaK5g>K1D*LEg&|kkwMH$_*>ZpX{_%0=zX<(g z^?%?am?o=Kg`n}ou6xXznr3Ruh@&>9{IFPdb)BlS#&oSzxx`9K*DxLL1S2#5kyr?w z-T0?;bk`2=!%9EHy=+_!Wwyqw9~y^QDMw0{ zZ6v2mNDBs9=JHUFo9kw-jXCeUa5QHB*ngNx;d!8y%*|?O?k+aVhAL_nd#h&Y9oNUk zf{%Ci?8DKjTg%Z-0$uybbg%Rm3*TU*{E>jrt&w|@6m`}qS)qpF!ntYI7=N+kJ0STZ z0i7d^sxaH|vt<&N^fs3eI#^TQ0YziwKNi$NO-$1E(79zjN%I&Cb%UH$<1ZF#jDLgv zp@1~YkS@?I_^8Fb8l(mG)Pl>3zh_D69}6nSJ^}I!G>Yq-RYr6(&@^%)iTQU>{>OrX z4yXq7m#3JWN){&%dTxuJe(Wz+YOLjt&Q$4JD3xRe9n@G4)FuH9qV%Fy7^?9KTx-0H zpIUHsNLy%AQCUg!7Qbk|24z8cW`7Yh1hG2V$tqd<>cVj!aavymB#1u8)IIm;XPKa| zzL$}DoU0wN@;ZlT;zO?L0k;I4n6j35r!BSKI;jzQyCzCvT%e>+5>ySAmsLg?>#ZF$ zekA}CNr9DY=9p`av3uW8FM5smn(}aMZ1O6(>a^owa(pHUe!~O4#1d59?|-=ZvXR_v z7cq#xpU#hE)KT_2fV6x`&9ix9vsbSsoyg8&?p1q9Lci=FBooe;com`t(A)a0)!9ZZ zMwiVo7Ljm%KQ0x4>IveSek{bbu+A9=Ft+z6JH|zMbo1tZq)(~n5?F&bKdWmg{xy}0 zXPd?%^hS<)^g&Xk&i^|n)dn;v4TjV+&J zF!DkjJ>jTkitjPc+N5<=lX}4l-=>AW-FHDnxu{6)(c_Seq~O!NbQ^pE2r z_n*Pv=xT72m^@I?>U(S% zZwVj$_V{RW^+}NZ&3|%if^ar!F1#{8Q@P{wZ;y|*D?^(ga$rMONm;#DLT-R*-1{-D zacbj~#>tJ78Yhlh8%H*dXdK=+ta0e8pSh{by|gd0<7Nd|Fzvfe5GStM!y8v?T(xnP z#+4gaYFu%=+Bmau#vL>L1)-!;x-y~kKcw3jB*P)HIs6uW)qloFk-XD=3{hk$j>2mV z@GgoEkP`#7&;s(=ySNWoNo`WHNr@)KpYxPrO^P-t@{g2?6#N}EDdh!7))6XR)MQPI zxyYiIsYQ9j*A&?Aj=z?3>M1&1saWnfy_7jM}M8p<8t8eZ28^zlbE~vW+t8!@`ZD(qKz9Bv$x&=O~k)D{y{T8l31t(y>zCh+ zxtf#W0$lw;kR_$fuvNEhwJ%7>PZsl&SSndM=c+4#7=OwIy?hZpw{t+mK2^+U%<6m5 zU^LC3>6MGuT_Hs}=~o0H^tobQXU?&$W*-)A9HW<^GabFtHytX%pDN~FWsQv{0@;(G z5)q$E`Dq$Fc4a-HpDJc7U$zd772MHjQ6A_(EoKsLsHBK|s+iYE-LvC^1^1p<3F>vM z4OmP+SATM3+{CDffxlRrXg1MkqTWQUiE0y-Cdy5en&8GgtHqPLO*6cr({2&f~r-YyS55eOiF=N@Ea~!W%sU4<7M=n|sHP@7_CMO#**P zli(&nKV0_`nAh6Gvxx%;;!WIsxc0^Mw_{(n4d04<3b|^c%zXAVkIg!-Y*}i2%Gh_| z*?*+eGRC__c|asCU=w5AV`X5<8{sW6Z_s9Hoq`qt+2E%rK= z$M(70#t_yHLPxn0H>vt5V_(NAzKCZ(yMG+Tl04R4V3Ul@+s*u0V^6&D@}MQMCwV!J z4r$B&^pD}EChvYuIpp@>xj zl>TBGB|ODdk)qlKj|}P1Y=EnpntEunCV!eAdh;f z{rww6ll+|Pn_i^ss9AQkSdtwbj9I}S$@PVbpZRIy*Sbm>dqeKMTzJGh*D}{@^*E;;E&p`*B5dbGVt)Q+xy`l@=QjBl& zFU~=b-~Pns;c5Mh*j;RcThsy1k7{1V;x~%?o(FyUa{(~Vva2o*kJQ5(RL88~2ABOl z7x~oZkZNmDw?{AljvaA_(bj}FmcHBns(kw2Vt{EMeeIcLjSNW77ud3n=6|6pySnG` z`LC-wbO6^?k$d3jodo_rlq8P~;EU`W^(z5p0Om%nuySMXMa%9srl9ysDt;%~)p$FP6OhuS(jKq$$A*ftupK6#!YYX^E!DFaG3Qv{=)EKc#8mrUga{ z<+UAbXV$(MZKX^EWTJP0tAERzxS!JrEM>|^7jO<@B89|#yh zC}OLRwm>Cc=qW}AKq)lP7(_?#`Ig7m#Le<=#mP zG_`1oeaxDgHZ}SA{2MnlY6@=)fOSFE)d%(M@W>lysTSCIp$9tP8dkmVlhf7ArfyAL zo4Pc0ZtBz&t{7IETK>;*&^Q8OfYOdA6{vCFx_BFqiI;?_86O@;6$aG4uQEn@mfblf zgfFE7;dQS^_YaR_Jbwa~LCeCsg;FO$T^yXOovwF2K0c0^Aih@}=s`{B`j{4Nt(B~w zt5?#r503-P*gTc{=`}0&0d2j`qHssx+wQ3T@z)2@7SFY&Lbo)wrZ}r{_f@^hy)XUa z@0YzY)if4JB%&0ZaM$)S7SN#U{x16Aaj-oi&~+wtKpnRb!++(3U?pKe6lkNf0Mcu zsXYok35kexZtI&yG>wmc-;l$d&NaZvE)V)Uhc6p|fZBZjPWeY-0j&~k{yeGV9@)j% zzz|u+TQ8Mf6Y<=Zkq>{?Mm-A@@owF048XJuO263FIGqw8z(T0I9FR*^>wNXOgyJ0AXH@%S3sSN5oDC+sSZPf$B!8CA_c z9#8aH=@@kb>Dg)p*oq1*O89HP-_`Z5_y5=5;w+>!Avt$oWMYVmWw%5XOaEVwHIDDT z%2RsMj(7G9>49#nNg`t2V9Dw89;VUPqVg7)nsC9}qw*jKP+{1&eZg(Sv-y z-?jqr>#T4sND#-5Gpz%D*P)Bv(ds|!2T$s8ixbQYP{W5y3{2aUSE8`canjb4fhNGiykY)SY zu776&eD#bE=U^&WpNz4~kyFq<5IOCXvKG~R3=+Rwi`aGyaK%nhD(Gh1HGvsJG7I3d zi?cW4XWPK7x4;}`g^O4jPUo;Wyk2U2ZP&-P60)SkL)sfrB6&f)Sms!T{F;3j!JS85 z6f=gE3YUrj)6S?cdFpfb0pqK?Z8oE527lK?xKR$Mz31Z*Lf!j(Y=9Q!DjMs3j?aA5 z=NOu6RX?Sk+GXL++y%{v{U8f@seQ)O?3tIlkH8N(dvTaJ*no>Ncsl63s%5srto>$B~K3-6pT;Q_i?rlAxUr_60WFHHRTjj*jNn5v7x$R1Ik zo*IGHcPTj4FS)-j8gv6Uy!X;ig}KnEGD-o&8*7JU947ZV7ios;THs`jW7TGy%{ZE| zzqpjTJ#qD91tT2}nY&tt15UYh!hh%7|H~Nm0Ej7s%2`q1U$F(Y)Upq(J#QTT&oOY{ zy^$maL+4!za_9@R_##3*2plsS$YR}G<}+9SC5{7@C@8K(6Go4x8ZNJnx1rP-zcR+Z z{v8B(?hYoU8;lW;RM$;oWPfNHp7)wiZl=`iIexvzLvC@@X@EyO=&%G+MSr_ThY93) zn=n4}|C4?9ne{PIrE$&yPYAI0m`Jn*F2e&wkKY~yQ~l?@D$jgF(mt!7le3~a55Gm{ zV1anD&cB}@KRGTKcA9%e*fvXS1z&1M?S z)SIcH-_3H0tXec@XZU>C8eTGYPx^m~KlwLfZdmtvD(K#$W?@1LD||P@%eg%+=Kpz2 zGyI#)ESkOZw{@HeJ3`#seCmvqNF`dhfLHqWy#0$f>0lU#FQYq{6-y)yZVaIQ>ht`x z$bU6vKd^iYwiR2Z3M_aa@tWO3VqJUP?=(9GhqjPr!Oeo21?HzV^K9nP%)Nh^TQgku zF3p^q!CCp={3b_6UzKWy+;UecU~)`F?+mScpR51*xW)qtluoEk7TE;x5OIZ#hi48`%k9{eWmeec}Uws|#3^dItu%RSgXh?>72-I7-cm_*r zmf9?(Su%7+5U3Z}&B98f>luH(ljk|x&v@I6W53!gvsp&7^w$Elb4>3OE_f3f)Y_*h zlSt0@HCClrRoTO8Bp3vez1!V~pYw67@34R7l?@+OH?(!( z3V>8v%n9~>Qx;LW5o>gJrC_L-nexLhi5rybCTu+^KxoVDyAM4X=md_C5V>d_=da%fFCef%U!X>TusG@M5qy(Q%KN`4k#o=3dI8PN^pc z?Bw?hIA+3`))s&4*6;ZI!}zcK^1hvaS-APtcv4OjUuIz0DdwB;!uo#x zhm=!6?m~KuEj7mKbLlvi>)iM6xAVVgScR(v{0VCi^Z|eMQK1})_4et0=3o9fKc=)X zs|UfrhGG_m`4M{ZJDsodzhqeOJ|jiqtXP{i0gJ;24rjG>id3yMVjw3$q)b1|Kj6|8zEo8wAfPPAU=cT{!)l}O7Q*ZuryS9N$nEGev`If)|DNQAhV&y_#{?P< z=|!R4XT9G`F8Z2bW%MIxaCPc}&h*}&mT;=&yniSAe;@Do2KQJh+$*&ks77R5q=Tw{ zYx`d`7cRBAWOKp)_SZm)VF_T4gV4SoIY9p~PVRqlzhfOb0ORIL%@sbuy3QDNbU}tr zPMyF6N^*48_w@@?T-D|(ucCdQy#{n3y8tKzX2Ujvzpwm#9l|Q}thM@rD^>@Z(sBIST=O+u7UTUYa8HW0IK(M?AWNXvBgIYbZ;9Uo+yIXkI#C8J zKXgp6K4w``9}lZ~_S*=-&70f(=JPj3^D%!9AX^(9$Lmx$uMaB<^M=yj?{bSD_9OHz zbT~uSBL_yc3={IxSE#=|q}=j{{qpouYiMzaJq;Ws&sjx|dZ~H+?46rCHFu0rpLc(( z&A`HB(Rp0Liy2p#+W_QzbA#^kkGWLd(Cmx=V!kq(7-1^|6TVXT?E&xE+@raB^Y?%E zu=|Y_UPnO1S>GOt>t~LXhYhi3z2Ar)(mc3%(2Y4T=8ZX5DZq$y_<^qzUSYPv1I5Mj zu5)_4c6&@R&=c|A^4yn?ld#ryb)B@{m z%LfGuU6aGX#PM;7lnqPK2UG{Mi-7A8?|bYh(xO~+YdO<;?j!hK*)^WJdX