From 05017e3220743d8538eb963513ecb45d569b891d Mon Sep 17 00:00:00 2001 From: arnaudgolfouse Date: Thu, 16 Jan 2025 16:10:59 +0100 Subject: [PATCH] Update tests --- .../bug/01_resolve_unsoundness.coma | 2 +- .../diagnostics/view_unimplemented.stderr | 4 +- .../should_fail/type_invariants/borrows.coma | 18 +++--- creusot/tests/should_succeed/100doors.coma | 4 +- creusot/tests/should_succeed/bdd.coma | 64 +++++++++---------- creusot/tests/should_succeed/bug/766.coma | 2 +- creusot/tests/should_succeed/bug/874.coma | 2 +- creusot/tests/should_succeed/bug/991.coma | 2 +- .../tests/should_succeed/bug/eq_panic.coma | 2 +- .../should_succeed/bug/final_borrows.coma | 4 +- .../tests/should_succeed/bug/two_phase.coma | 4 +- creusot/tests/should_succeed/cc/array.coma | 6 +- .../tests/should_succeed/cc/collections.coma | 26 ++++---- creusot/tests/should_succeed/cc/iter.coma | 6 +- creusot/tests/should_succeed/cell/02.coma | 2 +- .../should_succeed/constrained_types.coma | 2 +- creusot/tests/should_succeed/duration.coma | 2 +- .../tests/should_succeed/filter_positive.coma | 4 +- creusot/tests/should_succeed/hashmap.coma | 22 +++---- .../should_succeed/heapsort_generic.coma | 14 ++-- creusot/tests/should_succeed/hillel.coma | 26 ++++---- creusot/tests/should_succeed/index_range.coma | 22 +++---- .../should_succeed/inferred_invariants.coma | 4 +- .../tests/should_succeed/insertion_sort.coma | 4 +- creusot/tests/should_succeed/instant.coma | 4 +- .../tests/should_succeed/invariant_moves.coma | 2 +- .../tests/should_succeed/ite_normalize.coma | 6 +- .../should_succeed/iterators/02_iter_mut.coma | 16 ++--- .../iterators/03_std_iterators.coma | 18 +++--- .../iterators/08_collect_extend.coma | 10 +-- .../should_succeed/iterators/17_filter.coma | 2 +- creusot/tests/should_succeed/knapsack.coma | 4 +- .../tests/should_succeed/knapsack_full.coma | 4 +- .../tests/should_succeed/list_index_mut.coma | 2 +- .../should_succeed/list_reversal_lasso.coma | 4 +- .../tests/should_succeed/mapping_test.coma | 6 +- creusot/tests/should_succeed/option.coma | 26 ++++---- creusot/tests/should_succeed/ord_trait.coma | 4 +- .../tests/should_succeed/red_black_tree.coma | 20 +++--- .../rusthorn/inc_some_2_list.coma | 4 +- .../rusthorn/inc_some_2_tree.coma | 4 +- .../rusthorn/inc_some_list.coma | 4 +- .../rusthorn/inc_some_tree.coma | 4 +- .../selection_sort_generic.coma | 8 +-- creusot/tests/should_succeed/slices/01.coma | 6 +- .../tests/should_succeed/slices/02_std.coma | 4 +- .../tests/should_succeed/sparse_array.coma | 10 +-- .../should_succeed/syntax/05_pearlite.coma | 2 +- .../should_succeed/syntax/12_ghost_code.coma | 6 +- .../syntax/derive_macros/mixed.coma | 8 +-- .../tests/should_succeed/take_first_mut.coma | 2 +- .../traits/16_impl_cloning.coma | 2 +- creusot/tests/should_succeed/vecdeque.coma | 6 +- creusot/tests/should_succeed/vector/01.coma | 4 +- .../tests/should_succeed/vector/02_gnome.coma | 8 +-- .../vector/03_knuth_shuffle.coma | 4 +- .../vector/04_binary_search.coma | 2 +- .../vector/05_binary_search_generic.coma | 4 +- .../vector/06_knights_tour.coma | 14 ++-- .../should_succeed/vector/07_read_write.coma | 6 +- .../should_succeed/vector/08_haystack.coma | 2 +- .../should_succeed/vector/09_capacity.coma | 2 +- 62 files changed, 246 insertions(+), 246 deletions(-) diff --git a/creusot/tests/should_fail/bug/01_resolve_unsoundness.coma b/creusot/tests/should_fail/bug/01_resolve_unsoundness.coma index d81da5189..463b7ea91 100644 --- a/creusot/tests/should_fail/bug/01_resolve_unsoundness.coma +++ b/creusot/tests/should_fail/bug/01_resolve_unsoundness.coma @@ -8,7 +8,7 @@ module M_01_resolve_unsoundness__make_vec_of_size [#"01_resolve_unsoundness.rs" let%span svec6 = "../../../../creusot-contracts/src/std/vec.rs" 74 26 74 44 let%span svec7 = "../../../../creusot-contracts/src/std/vec.rs" 87 26 87 56 let%span svec8 = "../../../../creusot-contracts/src/std/vec.rs" 18 14 18 41 - let%span smodel9 = "../../../../creusot-contracts/src/model.rs" 110 8 110 22 + let%span smodel9 = "../../../../creusot-contracts/src/model.rs" 72 8 72 22 use prelude.prelude.Opaque diff --git a/creusot/tests/should_fail/diagnostics/view_unimplemented.stderr b/creusot/tests/should_fail/diagnostics/view_unimplemented.stderr index 351eeaf14..8b83754e6 100644 --- a/creusot/tests/should_fail/diagnostics/view_unimplemented.stderr +++ b/creusot/tests/should_fail/diagnostics/view_unimplemented.stderr @@ -13,9 +13,9 @@ error[E0599]: Cannot take the model of `S` `S: creusot_contracts::View` which is required by `&mut S: creusot_contracts::View` note: the trait `creusot_contracts::View` must be implemented - --> ./creusot-contracts/src/model.rs:14:1 + --> ./creusot-contracts/src/model.rs:12:1 | -14 | pub trait View { +12 | pub trait View { | ^^^^^^^^^^^^^^ = help: items from traits can only be used if the trait is implemented and in scope = note: the following trait defines an item `view`, perhaps you need to implement it: diff --git a/creusot/tests/should_fail/type_invariants/borrows.coma b/creusot/tests/should_fail/type_invariants/borrows.coma index d4c7018b2..0d02e8679 100644 --- a/creusot/tests/should_fail/type_invariants/borrows.coma +++ b/creusot/tests/should_fail/type_invariants/borrows.coma @@ -122,7 +122,7 @@ module M_borrows__simple [#"borrows.rs" 31 0 31 30] let%span sborrows2 = "borrows.rs" 30 11 30 21 let%span sborrows3 = "borrows.rs" 99 11 99 25 let%span sborrows4 = "borrows.rs" 100 10 100 25 - let%span smodel5 = "../../../../creusot-contracts/src/model.rs" 110 8 110 22 + let%span smodel5 = "../../../../creusot-contracts/src/model.rs" 72 8 72 22 let%span sresolve6 = "../../../../creusot-contracts/src/resolve.rs" 54 20 54 34 let%span sinvariant7 = "../../../../creusot-contracts/src/invariant.rs" 34 20 34 44 let%span sborrows8 = "borrows.rs" 10 20 10 32 @@ -219,7 +219,7 @@ module M_borrows__hard [#"borrows.rs" 38 0 38 28] let%span sborrows5 = "borrows.rs" 22 14 22 38 let%span sborrows6 = "borrows.rs" 99 11 99 25 let%span sborrows7 = "borrows.rs" 100 10 100 25 - let%span smodel8 = "../../../../creusot-contracts/src/model.rs" 110 8 110 22 + let%span smodel8 = "../../../../creusot-contracts/src/model.rs" 72 8 72 22 let%span sresolve9 = "../../../../creusot-contracts/src/resolve.rs" 54 20 54 34 let%span sborrows10 = "borrows.rs" 10 20 10 32 let%span sinvariant11 = "../../../../creusot-contracts/src/invariant.rs" 34 20 34 44 @@ -329,7 +329,7 @@ module M_borrows__tuple [#"borrows.rs" 45 0 45 44] let%span sborrows3 = "borrows.rs" 44 11 44 23 let%span sborrows4 = "borrows.rs" 99 11 99 25 let%span sborrows5 = "borrows.rs" 100 10 100 25 - let%span smodel6 = "../../../../creusot-contracts/src/model.rs" 110 8 110 22 + let%span smodel6 = "../../../../creusot-contracts/src/model.rs" 72 8 72 22 let%span sresolve7 = "../../../../creusot-contracts/src/resolve.rs" 54 20 54 34 let%span sresolve8 = "../../../../creusot-contracts/src/resolve.rs" 40 8 40 44 let%span sborrows9 = "borrows.rs" 10 20 10 32 @@ -446,7 +446,7 @@ module M_borrows__partial_move [#"borrows.rs" 53 0 53 47] let%span sborrows3 = "borrows.rs" 52 11 52 23 let%span sborrows4 = "borrows.rs" 99 11 99 25 let%span sborrows5 = "borrows.rs" 100 10 100 25 - let%span smodel6 = "../../../../creusot-contracts/src/model.rs" 110 8 110 22 + let%span smodel6 = "../../../../creusot-contracts/src/model.rs" 72 8 72 22 let%span sresolve7 = "../../../../creusot-contracts/src/resolve.rs" 54 20 54 34 let%span sinvariant8 = "../../../../creusot-contracts/src/invariant.rs" 34 20 34 44 let%span sborrows9 = "borrows.rs" 10 20 10 32 @@ -563,7 +563,7 @@ module M_borrows__destruct [#"borrows.rs" 61 0 61 43] let%span sborrows3 = "borrows.rs" 60 11 60 23 let%span sborrows4 = "borrows.rs" 99 11 99 25 let%span sborrows5 = "borrows.rs" 100 10 100 25 - let%span smodel6 = "../../../../creusot-contracts/src/model.rs" 110 8 110 22 + let%span smodel6 = "../../../../creusot-contracts/src/model.rs" 72 8 72 22 let%span sresolve7 = "../../../../creusot-contracts/src/resolve.rs" 54 20 54 34 let%span sinvariant8 = "../../../../creusot-contracts/src/invariant.rs" 34 20 34 44 let%span sborrows9 = "borrows.rs" 10 20 10 32 @@ -670,7 +670,7 @@ module M_borrows__frozen_dead [#"borrows.rs" 69 0 69 66] let%span sborrows4 = "borrows.rs" 99 11 99 25 let%span sborrows5 = "borrows.rs" 100 10 100 25 let%span sresolve6 = "../../../../creusot-contracts/src/resolve.rs" 54 20 54 34 - let%span smodel7 = "../../../../creusot-contracts/src/model.rs" 110 8 110 22 + let%span smodel7 = "../../../../creusot-contracts/src/model.rs" 72 8 72 22 let%span sborrows8 = "borrows.rs" 10 20 10 32 let%span sinvariant9 = "../../../../creusot-contracts/src/invariant.rs" 34 20 34 44 @@ -780,7 +780,7 @@ module M_borrows__qyi5556307355051076399__foo [#"borrows.rs" 93 4 93 25] (* SumT let%span sborrows3 = "borrows.rs" 100 10 100 25 let%span sborrows4 = "borrows.rs" 105 11 105 25 let%span sborrows5 = "borrows.rs" 106 10 106 25 - let%span smodel6 = "../../../../creusot-contracts/src/model.rs" 110 8 110 22 + let%span smodel6 = "../../../../creusot-contracts/src/model.rs" 72 8 72 22 let%span sresolve7 = "../../../../creusot-contracts/src/resolve.rs" 54 20 54 34 let%span sinvariant8 = "../../../../creusot-contracts/src/invariant.rs" 34 20 34 44 let%span sborrows9 = "borrows.rs" 87 20 87 43 @@ -892,7 +892,7 @@ module M_borrows__inc [#"borrows.rs" 101 0 101 23] let%span sborrows0 = "borrows.rs" 102 10 102 11 let%span sborrows1 = "borrows.rs" 99 11 99 25 let%span sborrows2 = "borrows.rs" 100 10 100 25 - let%span smodel3 = "../../../../creusot-contracts/src/model.rs" 110 8 110 22 + let%span smodel3 = "../../../../creusot-contracts/src/model.rs" 72 8 72 22 let%span sresolve4 = "../../../../creusot-contracts/src/resolve.rs" 54 20 54 34 use prelude.prelude.Int32 @@ -936,7 +936,7 @@ module M_borrows__dec [#"borrows.rs" 107 0 107 23] let%span sborrows0 = "borrows.rs" 108 10 108 11 let%span sborrows1 = "borrows.rs" 105 11 105 25 let%span sborrows2 = "borrows.rs" 106 10 106 25 - let%span smodel3 = "../../../../creusot-contracts/src/model.rs" 110 8 110 22 + let%span smodel3 = "../../../../creusot-contracts/src/model.rs" 72 8 72 22 let%span sresolve4 = "../../../../creusot-contracts/src/resolve.rs" 54 20 54 34 use prelude.prelude.Int32 diff --git a/creusot/tests/should_succeed/100doors.coma b/creusot/tests/should_succeed/100doors.coma index ef30ab805..d142a04ac 100644 --- a/creusot/tests/should_succeed/100doors.coma +++ b/creusot/tests/should_succeed/100doors.coma @@ -36,10 +36,10 @@ module M_100doors__f [#"100doors.rs" 18 0 18 10] let%span snum34 = "../../../creusot-contracts/src/std/num.rs" 21 28 21 33 let%span srange35 = "../../../creusot-contracts/src/std/iter/range.rs" 14 12 14 78 let%span sresolve36 = "../../../creusot-contracts/src/resolve.rs" 54 20 54 34 - let%span smodel37 = "../../../creusot-contracts/src/model.rs" 92 8 92 22 + let%span smodel37 = "../../../creusot-contracts/src/model.rs" 54 8 54 22 let%span sslice38 = "../../../creusot-contracts/src/std/slice.rs" 122 20 122 37 let%span sslice39 = "../../../creusot-contracts/src/std/slice.rs" 129 20 129 37 - let%span smodel40 = "../../../creusot-contracts/src/model.rs" 110 8 110 22 + let%span smodel40 = "../../../creusot-contracts/src/model.rs" 72 8 72 22 let%span sslice41 = "../../../creusot-contracts/src/std/slice.rs" 136 20 136 94 use prelude.prelude.UIntSize diff --git a/creusot/tests/should_succeed/bdd.coma b/creusot/tests/should_succeed/bdd.coma index 0f569f14b..8dd8ffbb7 100644 --- a/creusot/tests/should_succeed/bdd.coma +++ b/creusot/tests/should_succeed/bdd.coma @@ -12,7 +12,7 @@ module M_bdd__hashmap__qyi11648407051195780326__hash [#"bdd.rs" 79 8 79 29] (* < let%span snum10 = "../../../creusot-contracts/src/std/num.rs" 144 20 145 51 let%span snum11 = "../../../creusot-contracts/src/std/num.rs" 151 20 153 92 let%span snum12 = "../../../creusot-contracts/src/std/num.rs" 156 20 158 92 - let%span smodel13 = "../../../creusot-contracts/src/model.rs" 83 8 83 28 + let%span smodel13 = "../../../creusot-contracts/src/model.rs" 45 8 45 28 let%span sbdd14 = "bdd.rs" 86 24 86 84 let%span stuples15 = "../../../creusot-contracts/src/std/tuples.rs" 29 28 29 57 let%span sinvariant16 = "../../../creusot-contracts/src/invariant.rs" 24 8 24 18 @@ -201,8 +201,8 @@ module M_bdd__qyi4854841669736991510__eq [#"bdd.rs" 93 13 93 22] (* as hashmap::Hash> *) let%span sbdd0 = "bdd.rs" 144 14 144 46 - let%span smodel1 = "../../../creusot-contracts/src/model.rs" 92 8 92 22 + let%span smodel1 = "../../../creusot-contracts/src/model.rs" 54 8 54 22 let%span sbdd2 = "bdd.rs" 152 20 152 22 let%span sbdd3 = "bdd.rs" 199 20 199 37 let%span sbdd4 = "bdd.rs" 189 20 189 26 @@ -685,7 +685,7 @@ module M_bdd__qyi14323183011761258016__hash [#"bdd.rs" 145 4 145 25] (* as creusot_contracts::PartialEq> *) let%span sbdd0 = "bdd.rs" 204 14 204 37 - let%span smodel1 = "../../../creusot-contracts/src/model.rs" 92 8 92 22 + let%span smodel1 = "../../../creusot-contracts/src/model.rs" 54 8 54 22 let%span sbdd2 = "bdd.rs" 199 20 199 37 let%span sbdd3 = "bdd.rs" 189 20 189 26 @@ -757,7 +757,7 @@ module M_bdd__qyi11078426090797403070__grows_is_valid_bdd [#"bdd.rs" 339 4 339 5 let%span sbdd3 = "bdd.rs" 334 4 334 12 let%span sbdd4 = "bdd.rs" 301 12 306 17 let%span sbdd5 = "bdd.rs" 314 12 314 47 - let%span smodel6 = "../../../creusot-contracts/src/model.rs" 92 8 92 22 + let%span smodel6 = "../../../creusot-contracts/src/model.rs" 54 8 54 22 let%span sbdd7 = "bdd.rs" 179 20 179 37 let%span sbdd8 = "bdd.rs" 163 12 167 13 @@ -927,7 +927,7 @@ module M_bdd__qyi11078426090797403070__set_irrelevent_var [#"bdd.rs" 355 4 355 8 let%span sbdd5 = "bdd.rs" 314 12 314 47 let%span sbdd6 = "bdd.rs" 244 12 248 13 let%span sbdd7 = "bdd.rs" 214 12 221 13 - let%span smodel8 = "../../../creusot-contracts/src/model.rs" 92 8 92 22 + let%span smodel8 = "../../../creusot-contracts/src/model.rs" 54 8 54 22 let%span sbdd9 = "bdd.rs" 267 12 291 19 let%span sbdd10 = "bdd.rs" 179 20 179 37 let%span sbdd11 = "bdd.rs" 321 12 330 13 @@ -1128,7 +1128,7 @@ module M_bdd__qyi11078426090797403070__discr_valuation [#"bdd.rs" 375 4 375 82] let%span sbdd14 = "bdd.rs" 354 14 354 50 let%span sbdd15 = "bdd.rs" 357 12 363 13 let%span sbdd16 = "bdd.rs" 244 12 248 13 - let%span smodel17 = "../../../creusot-contracts/src/model.rs" 92 8 92 22 + let%span smodel17 = "../../../creusot-contracts/src/model.rs" 54 8 54 22 let%span sbdd18 = "bdd.rs" 267 12 291 19 let%span sbdd19 = "bdd.rs" 179 20 179 37 let%span sbdd20 = "bdd.rs" 321 12 330 13 @@ -1422,7 +1422,7 @@ module M_bdd__qyi11078426090797403070__bdd_canonical [#"bdd.rs" 424 4 424 62] (* let%span sbdd12 = "bdd.rs" 372 14 372 50 let%span sbdd13 = "bdd.rs" 373 14 373 33 let%span sbdd14 = "bdd.rs" 377 12 377 36 - let%span smodel15 = "../../../creusot-contracts/src/model.rs" 92 8 92 22 + let%span smodel15 = "../../../creusot-contracts/src/model.rs" 54 8 54 22 let%span sbdd16 = "bdd.rs" 226 14 226 25 let%span sbdd17 = "bdd.rs" 229 12 237 13 let%span sbdd18 = "bdd.rs" 351 15 351 24 @@ -1676,7 +1676,7 @@ module M_bdd__qyi11078426090797403070__new [#"bdd.rs" 430 4 430 52] (* Context<' let%span sbdd5 = "bdd.rs" 430 48 430 52 let%span sbdd6 = "bdd.rs" 70 18 70 47 let%span sbdd7 = "bdd.rs" 267 12 291 19 - let%span smodel8 = "../../../creusot-contracts/src/model.rs" 92 8 92 22 + let%span smodel8 = "../../../creusot-contracts/src/model.rs" 54 8 54 22 let%span sbdd9 = "bdd.rs" 321 12 330 13 let%span sbdd10 = "bdd.rs" 314 12 314 47 let%span sbdd11 = "bdd.rs" 214 12 221 13 @@ -1913,15 +1913,15 @@ module M_bdd__qyi11078426090797403070__hashcons [#"bdd.rs" 446 4 446 58] (* Cont let%span sbdd16 = "bdd.rs" 57 30 57 33 let%span sbdd17 = "bdd.rs" 57 38 57 41 let%span sbdd18 = "bdd.rs" 55 18 55 126 - let%span smodel19 = "../../../creusot-contracts/src/model.rs" 92 8 92 22 + let%span smodel19 = "../../../creusot-contracts/src/model.rs" 54 8 54 22 let%span sbdd20 = "bdd.rs" 179 20 179 37 let%span sbdd21 = "bdd.rs" 321 12 330 13 let%span sbdd22 = "bdd.rs" 301 12 306 17 let%span sbdd23 = "bdd.rs" 314 12 314 47 - let%span smodel24 = "../../../creusot-contracts/src/model.rs" 83 8 83 28 + let%span smodel24 = "../../../creusot-contracts/src/model.rs" 45 8 45 28 let%span sresolve25 = "../../../creusot-contracts/src/resolve.rs" 54 20 54 34 let%span sbdd26 = "bdd.rs" 163 12 167 13 - let%span smodel27 = "../../../creusot-contracts/src/model.rs" 110 8 110 22 + let%span smodel27 = "../../../creusot-contracts/src/model.rs" 72 8 72 22 let%span sbdd28 = "bdd.rs" 244 12 248 13 let%span sinvariant29 = "../../../creusot-contracts/src/invariant.rs" 34 20 34 44 let%span sbdd30 = "bdd.rs" 267 12 291 19 @@ -2291,7 +2291,7 @@ module M_bdd__qyi11078426090797403070__node [#"bdd.rs" 471 4 471 87] (* Context< let%span sbdd15 = "bdd.rs" 244 12 248 13 let%span sbdd16 = "bdd.rs" 301 12 306 17 let%span sbdd17 = "bdd.rs" 214 12 221 13 - let%span smodel18 = "../../../creusot-contracts/src/model.rs" 92 8 92 22 + let%span smodel18 = "../../../creusot-contracts/src/model.rs" 54 8 54 22 let%span sresolve19 = "../../../creusot-contracts/src/resolve.rs" 54 20 54 34 let%span sbdd20 = "bdd.rs" 321 12 330 13 let%span sbdd21 = "bdd.rs" 199 20 199 37 @@ -2555,7 +2555,7 @@ module M_bdd__qyi11078426090797403070__trueqy95z [#"bdd.rs" 482 4 482 42] (* Con let%span sbdd13 = "bdd.rs" 244 12 248 13 let%span sbdd14 = "bdd.rs" 321 12 330 13 let%span sresolve15 = "../../../creusot-contracts/src/resolve.rs" 54 20 54 34 - let%span smodel16 = "../../../creusot-contracts/src/model.rs" 92 8 92 22 + let%span smodel16 = "../../../creusot-contracts/src/model.rs" 54 8 54 22 let%span sbdd17 = "bdd.rs" 267 12 291 19 let%span sinvariant18 = "../../../creusot-contracts/src/invariant.rs" 34 20 34 44 let%span sbdd19 = "bdd.rs" 179 20 179 37 @@ -2785,7 +2785,7 @@ module M_bdd__qyi11078426090797403070__falseqy95z [#"bdd.rs" 490 4 490 43] (* Co let%span sbdd13 = "bdd.rs" 244 12 248 13 let%span sbdd14 = "bdd.rs" 321 12 330 13 let%span sresolve15 = "../../../creusot-contracts/src/resolve.rs" 54 20 54 34 - let%span smodel16 = "../../../creusot-contracts/src/model.rs" 92 8 92 22 + let%span smodel16 = "../../../creusot-contracts/src/model.rs" 54 8 54 22 let%span sbdd17 = "bdd.rs" 267 12 291 19 let%span sinvariant18 = "../../../creusot-contracts/src/invariant.rs" 34 20 34 44 let%span sbdd19 = "bdd.rs" 179 20 179 37 @@ -3026,7 +3026,7 @@ module M_bdd__qyi11078426090797403070__v [#"bdd.rs" 497 4 497 46] (* Context<'ar let%span sbdd24 = "bdd.rs" 214 12 221 13 let%span sbdd25 = "bdd.rs" 244 12 248 13 let%span sresolve26 = "../../../creusot-contracts/src/resolve.rs" 54 20 54 34 - let%span smodel27 = "../../../creusot-contracts/src/model.rs" 92 8 92 22 + let%span smodel27 = "../../../creusot-contracts/src/model.rs" 54 8 54 22 let%span sbdd28 = "bdd.rs" 267 12 291 19 let%span sinvariant29 = "../../../creusot-contracts/src/invariant.rs" 34 20 34 44 let%span sbdd30 = "bdd.rs" 179 20 179 37 @@ -3324,10 +3324,10 @@ module M_bdd__qyi11078426090797403070__not [#"bdd.rs" 509 4 509 56] (* Context<' let%span sbdd34 = "bdd.rs" 244 12 248 13 let%span sbdd35 = "bdd.rs" 226 14 226 25 let%span sbdd36 = "bdd.rs" 229 12 237 13 - let%span smodel37 = "../../../creusot-contracts/src/model.rs" 92 8 92 22 - let%span smodel38 = "../../../creusot-contracts/src/model.rs" 83 8 83 28 + let%span smodel37 = "../../../creusot-contracts/src/model.rs" 54 8 54 22 + let%span smodel38 = "../../../creusot-contracts/src/model.rs" 45 8 45 28 let%span sbdd39 = "bdd.rs" 189 20 189 26 - let%span smodel40 = "../../../creusot-contracts/src/model.rs" 110 8 110 22 + let%span smodel40 = "../../../creusot-contracts/src/model.rs" 72 8 72 22 let%span sresolve41 = "../../../creusot-contracts/src/resolve.rs" 54 20 54 34 let%span sbdd42 = "bdd.rs" 267 12 291 19 let%span sinvariant43 = "../../../creusot-contracts/src/invariant.rs" 34 20 34 44 @@ -3771,13 +3771,13 @@ module M_bdd__qyi11078426090797403070__and [#"bdd.rs" 533 4 533 72] (* Context<' let%span sbdd32 = "bdd.rs" 244 12 248 13 let%span sbdd33 = "bdd.rs" 226 14 226 25 let%span sbdd34 = "bdd.rs" 229 12 237 13 - let%span smodel35 = "../../../creusot-contracts/src/model.rs" 92 8 92 22 - let%span smodel36 = "../../../creusot-contracts/src/model.rs" 83 8 83 28 + let%span smodel35 = "../../../creusot-contracts/src/model.rs" 54 8 54 22 + let%span smodel36 = "../../../creusot-contracts/src/model.rs" 45 8 45 28 let%span sresolve37 = "../../../creusot-contracts/src/resolve.rs" 54 20 54 34 let%span snum38 = "../../../creusot-contracts/src/std/num.rs" 21 28 21 33 let%span sord39 = "../../../creusot-contracts/src/logic/ord.rs" 186 16 192 17 let%span stuples40 = "../../../creusot-contracts/src/std/tuples.rs" 29 28 29 57 - let%span smodel41 = "../../../creusot-contracts/src/model.rs" 110 8 110 22 + let%span smodel41 = "../../../creusot-contracts/src/model.rs" 72 8 72 22 let%span sinvariant42 = "../../../creusot-contracts/src/invariant.rs" 34 20 34 44 let%span sord43 = "../../../creusot-contracts/src/logic/ord.rs" 129 39 129 89 let%span sord44 = "../../../creusot-contracts/src/logic/ord.rs" 134 39 134 86 @@ -4363,7 +4363,7 @@ module M_bdd__qyi11078426090797403070__and [#"bdd.rs" 533 4 533 72] (* Context<' end module M_bdd__hashmap__qyi11648407051195780326__hash__refines [#"bdd.rs" 79 8 79 29] (* <(U, V) as hashmap::Hash> *) let%span sbdd0 = "bdd.rs" 79 8 79 29 - let%span smodel1 = "../../../creusot-contracts/src/model.rs" 83 8 83 28 + let%span smodel1 = "../../../creusot-contracts/src/model.rs" 45 8 45 28 let%span sbdd2 = "bdd.rs" 86 24 86 84 let%span stuples3 = "../../../creusot-contracts/src/std/tuples.rs" 29 28 29 57 let%span sinvariant4 = "../../../creusot-contracts/src/invariant.rs" 24 8 24 18 @@ -4427,9 +4427,9 @@ module M_bdd__hashmap__qyi11648407051195780326__hash__refines [#"bdd.rs" 79 8 79 end module M_bdd__qyi699402059438633899__hash__refines [#"bdd.rs" 119 4 119 25] (* as hashmap::Hash> *) let%span sbdd0 = "bdd.rs" 119 4 119 25 - let%span smodel1 = "../../../creusot-contracts/src/model.rs" 92 8 92 22 + let%span smodel1 = "../../../creusot-contracts/src/model.rs" 54 8 54 22 let%span sbdd2 = "bdd.rs" 133 12 138 13 - let%span smodel3 = "../../../creusot-contracts/src/model.rs" 83 8 83 28 + let%span smodel3 = "../../../creusot-contracts/src/model.rs" 45 8 45 28 let%span sbdd4 = "bdd.rs" 179 20 179 37 let%span sbdd5 = "bdd.rs" 163 12 167 13 @@ -4489,9 +4489,9 @@ module M_bdd__qyi699402059438633899__hash__refines [#"bdd.rs" 119 4 119 25] (* < end module M_bdd__qyi14323183011761258016__hash__refines [#"bdd.rs" 145 4 145 25] (* as hashmap::Hash> *) let%span sbdd0 = "bdd.rs" 145 4 145 25 - let%span smodel1 = "../../../creusot-contracts/src/model.rs" 92 8 92 22 + let%span smodel1 = "../../../creusot-contracts/src/model.rs" 54 8 54 22 let%span sbdd2 = "bdd.rs" 152 20 152 22 - let%span smodel3 = "../../../creusot-contracts/src/model.rs" 83 8 83 28 + let%span smodel3 = "../../../creusot-contracts/src/model.rs" 45 8 45 28 let%span sbdd4 = "bdd.rs" 199 20 199 37 let%span sbdd5 = "bdd.rs" 189 20 189 26 @@ -4545,7 +4545,7 @@ module M_bdd__qyi1284786238026687571__assert_receiver_is_total_eq__refines [#"bd end module M_bdd__qyi4854841669736991510__eq__refines [#"bdd.rs" 93 13 93 22] (* as creusot_contracts::PartialEq> *) let%span sbdd0 = "bdd.rs" 93 13 93 22 - let%span smodel1 = "../../../creusot-contracts/src/model.rs" 83 8 83 28 + let%span smodel1 = "../../../creusot-contracts/src/model.rs" 45 8 45 28 let%span sbdd2 = "bdd.rs" 163 12 167 13 use prelude.prelude.Borrow @@ -4584,8 +4584,8 @@ module M_bdd__qyi4854841669736991510__eq__refines [#"bdd.rs" 93 13 93 22] (* as creusot_contracts::PartialEq> *) let%span sbdd0 = "bdd.rs" 205 4 205 34 - let%span smodel1 = "../../../creusot-contracts/src/model.rs" 92 8 92 22 - let%span smodel2 = "../../../creusot-contracts/src/model.rs" 83 8 83 28 + let%span smodel1 = "../../../creusot-contracts/src/model.rs" 54 8 54 22 + let%span smodel2 = "../../../creusot-contracts/src/model.rs" 45 8 45 28 let%span sbdd3 = "bdd.rs" 199 20 199 37 let%span sbdd4 = "bdd.rs" 189 20 189 26 diff --git a/creusot/tests/should_succeed/bug/766.coma b/creusot/tests/should_succeed/bug/766.coma index dcbd6b2d2..b5fe60cca 100644 --- a/creusot/tests/should_succeed/bug/766.coma +++ b/creusot/tests/should_succeed/bug/766.coma @@ -2,7 +2,7 @@ module M_766__Trait__goo [#"766.rs" 10 4 10 21] let%span s7660 = "766.rs" 10 16 10 20 let%span s7661 = "766.rs" 8 14 8 18 let%span s7662 = "766.rs" 7 14 7 52 - let%span smodel3 = "../../../../creusot-contracts/src/model.rs" 101 8 101 28 + let%span smodel3 = "../../../../creusot-contracts/src/model.rs" 63 8 63 28 let%span sresolve4 = "../../../../creusot-contracts/src/resolve.rs" 54 20 54 34 let%span sinvariant5 = "../../../../creusot-contracts/src/invariant.rs" 34 20 34 44 diff --git a/creusot/tests/should_succeed/bug/874.coma b/creusot/tests/should_succeed/bug/874.coma index 1325def4a..79314dec7 100644 --- a/creusot/tests/should_succeed/bug/874.coma +++ b/creusot/tests/should_succeed/bug/874.coma @@ -21,7 +21,7 @@ module M_874__can_extend [#"874.rs" 4 0 4 19] let%span svec19 = "../../../../creusot-contracts/src/std/vec.rs" 197 20 197 33 let%span svec20 = "../../../../creusot-contracts/src/std/vec.rs" 257 20 257 57 let%span svec21 = "../../../../creusot-contracts/src/std/vec.rs" 264 12 264 41 - let%span smodel22 = "../../../../creusot-contracts/src/model.rs" 110 8 110 22 + let%span smodel22 = "../../../../creusot-contracts/src/model.rs" 72 8 72 22 let%span sslice23 = "../../../../creusot-contracts/src/std/slice.rs" 28 14 28 41 let%span sslice24 = "../../../../creusot-contracts/src/std/slice.rs" 29 14 29 42 let%span svec25 = "../../../../creusot-contracts/src/std/vec.rs" 270 14 270 45 diff --git a/creusot/tests/should_succeed/bug/991.coma b/creusot/tests/should_succeed/bug/991.coma index bcf8cee0d..2dfb42f1b 100644 --- a/creusot/tests/should_succeed/bug/991.coma +++ b/creusot/tests/should_succeed/bug/991.coma @@ -1,6 +1,6 @@ module M_991__qyi6256438357931963096__love_and_hope [#"991.rs" 22 4 22 27] (* Formula *) let%span s9910 = "991.rs" 21 14 21 28 - let%span smodel1 = "../../../../creusot-contracts/src/model.rs" 92 8 92 22 + let%span smodel1 = "../../../../creusot-contracts/src/model.rs" 54 8 54 22 let%span s9912 = "991.rs" 16 8 16 33 let%span svec3 = "../../../../creusot-contracts/src/std/vec.rs" 18 14 18 41 diff --git a/creusot/tests/should_succeed/bug/eq_panic.coma b/creusot/tests/should_succeed/bug/eq_panic.coma index c3d9ef2cd..163e78916 100644 --- a/creusot/tests/should_succeed/bug/eq_panic.coma +++ b/creusot/tests/should_succeed/bug/eq_panic.coma @@ -2,7 +2,7 @@ module M_eq_panic__omg [#"eq_panic.rs" 6 0 6 51] let%span seq_panic0 = "eq_panic.rs" 6 30 6 31 let%span seq_panic1 = "eq_panic.rs" 6 37 6 38 let%span scmp2 = "../../../../creusot-contracts/src/std/cmp.rs" 11 26 11 75 - let%span smodel3 = "../../../../creusot-contracts/src/model.rs" 83 8 83 28 + let%span smodel3 = "../../../../creusot-contracts/src/model.rs" 45 8 45 28 let%span sinvariant4 = "../../../../creusot-contracts/src/invariant.rs" 24 8 24 18 use prelude.prelude.Borrow diff --git a/creusot/tests/should_succeed/bug/final_borrows.coma b/creusot/tests/should_succeed/bug/final_borrows.coma index f24432591..f2c8a76d3 100644 --- a/creusot/tests/should_succeed/bug/final_borrows.coma +++ b/creusot/tests/should_succeed/bug/final_borrows.coma @@ -1936,7 +1936,7 @@ module M_final_borrows__index_mut_slice [#"final_borrows.rs" 208 0 208 48] let%span sfinal_borrows3 = "final_borrows.rs" 206 11 206 25 let%span sfinal_borrows4 = "final_borrows.rs" 208 42 208 48 let%span sfinal_borrows5 = "final_borrows.rs" 207 10 207 30 - let%span smodel6 = "../../../../creusot-contracts/src/model.rs" 110 8 110 22 + let%span smodel6 = "../../../../creusot-contracts/src/model.rs" 72 8 72 22 let%span sindex7 = "../../../../creusot-contracts/src/logic/ops/index.rs" 49 8 49 31 let%span sresolve8 = "../../../../creusot-contracts/src/resolve.rs" 54 20 54 34 let%span sslice9 = "../../../../creusot-contracts/src/std/slice.rs" 28 14 28 41 @@ -2099,7 +2099,7 @@ module M_final_borrows__index_mut_array [#"final_borrows.rs" 214 0 214 52] let%span sfinal_borrows3 = "final_borrows.rs" 212 11 212 25 let%span sfinal_borrows4 = "final_borrows.rs" 214 46 214 52 let%span sfinal_borrows5 = "final_borrows.rs" 213 10 213 35 - let%span smodel6 = "../../../../creusot-contracts/src/model.rs" 110 8 110 22 + let%span smodel6 = "../../../../creusot-contracts/src/model.rs" 72 8 72 22 let%span sindex7 = "../../../../creusot-contracts/src/logic/ops/index.rs" 82 8 82 32 let%span sresolve8 = "../../../../creusot-contracts/src/resolve.rs" 54 20 54 34 let%span sinvariant9 = "../../../../creusot-contracts/src/invariant.rs" 34 20 34 44 diff --git a/creusot/tests/should_succeed/bug/two_phase.coma b/creusot/tests/should_succeed/bug/two_phase.coma index c5adbaa3b..3df4adc2e 100644 --- a/creusot/tests/should_succeed/bug/two_phase.coma +++ b/creusot/tests/should_succeed/bug/two_phase.coma @@ -2,9 +2,9 @@ module M_two_phase__test [#"two_phase.rs" 6 0 6 31] let%span stwo_phase0 = "two_phase.rs" 5 10 5 37 let%span svec1 = "../../../../creusot-contracts/src/std/vec.rs" 83 26 83 48 let%span svec2 = "../../../../creusot-contracts/src/std/vec.rs" 87 26 87 56 - let%span smodel3 = "../../../../creusot-contracts/src/model.rs" 110 8 110 22 + let%span smodel3 = "../../../../creusot-contracts/src/model.rs" 72 8 72 22 let%span sindex4 = "../../../../creusot-contracts/src/logic/ops/index.rs" 27 8 27 31 - let%span smodel5 = "../../../../creusot-contracts/src/model.rs" 92 8 92 22 + let%span smodel5 = "../../../../creusot-contracts/src/model.rs" 54 8 54 22 let%span svec6 = "../../../../creusot-contracts/src/std/vec.rs" 18 14 18 41 let%span sresolve7 = "../../../../creusot-contracts/src/resolve.rs" 54 20 54 34 diff --git a/creusot/tests/should_succeed/cc/array.coma b/creusot/tests/should_succeed/cc/array.coma index 75f935b70..1d019648d 100644 --- a/creusot/tests/should_succeed/cc/array.coma +++ b/creusot/tests/should_succeed/cc/array.coma @@ -11,7 +11,7 @@ module M_array__test_array [#"array.rs" 3 0 3 19] let%span sarray9 = "array.rs" 10 30 10 31 let%span sslice10 = "../../../../creusot-contracts/src/std/slice.rs" 398 20 398 61 let%span sslice11 = "../../../../creusot-contracts/src/std/slice.rs" 405 12 405 66 - let%span smodel12 = "../../../../creusot-contracts/src/model.rs" 83 8 83 28 + let%span smodel12 = "../../../../creusot-contracts/src/model.rs" 45 8 45 28 let%span sarray13 = "../../../../creusot-contracts/src/std/array.rs" 87 20 87 24 let%span sarray14 = "../../../../creusot-contracts/src/std/array.rs" 93 20 93 33 let%span sarray15 = "../../../../creusot-contracts/src/std/array.rs" 67 20 67 57 @@ -23,7 +23,7 @@ module M_array__test_array [#"array.rs" 3 0 3 19] let%span sslice21 = "../../../../creusot-contracts/src/std/slice.rs" 418 14 418 42 let%span sslice22 = "../../../../creusot-contracts/src/std/slice.rs" 414 4 414 10 let%span sresolve23 = "../../../../creusot-contracts/src/resolve.rs" 54 20 54 34 - let%span smodel24 = "../../../../creusot-contracts/src/model.rs" 110 8 110 22 + let%span smodel24 = "../../../../creusot-contracts/src/model.rs" 72 8 72 22 let%span sslice25 = "../../../../creusot-contracts/src/std/slice.rs" 28 14 28 41 let%span sslice26 = "../../../../creusot-contracts/src/std/slice.rs" 29 14 29 42 let%span sslice27 = "../../../../creusot-contracts/src/std/slice.rs" 96 14 96 41 @@ -35,7 +35,7 @@ module M_array__test_array [#"array.rs" 3 0 3 19] let%span sarray33 = "../../../../creusot-contracts/src/std/array.rs" 78 15 78 32 let%span sarray34 = "../../../../creusot-contracts/src/std/array.rs" 79 14 79 42 let%span sarray35 = "../../../../creusot-contracts/src/std/array.rs" 75 4 75 10 - let%span smodel36 = "../../../../creusot-contracts/src/model.rs" 92 8 92 22 + let%span smodel36 = "../../../../creusot-contracts/src/model.rs" 54 8 54 22 let%span sindex37 = "../../../../creusot-contracts/src/logic/ops/index.rs" 49 8 49 31 let%span snum38 = "../../../../creusot-contracts/src/std/num.rs" 21 28 21 33 diff --git a/creusot/tests/should_succeed/cc/collections.coma b/creusot/tests/should_succeed/cc/collections.coma index f8345c7cc..cca6c0ba8 100644 --- a/creusot/tests/should_succeed/cc/collections.coma +++ b/creusot/tests/should_succeed/cc/collections.coma @@ -20,7 +20,7 @@ module M_collections__roundtrip_hashmap_into_iter [#"collections.rs" 15 0 17 18] let%span shash_map18 = "../../../../creusot-contracts/src/std/collections/hash_map.rs" 85 14 85 42 let%span shash_map19 = "../../../../creusot-contracts/src/std/collections/hash_map.rs" 87 8 87 104 let%span sresolve20 = "../../../../creusot-contracts/src/resolve.rs" 54 20 54 34 - let%span smodel21 = "../../../../creusot-contracts/src/model.rs" 110 8 110 22 + let%span smodel21 = "../../../../creusot-contracts/src/model.rs" 72 8 72 22 let%span sfmap22 = "../../../../creusot-contracts/src/logic/fmap.rs" 139 8 139 34 let%span sfmap23 = "../../../../creusot-contracts/src/logic/fmap.rs" 48 14 48 25 let%span sfmap24 = "../../../../creusot-contracts/src/logic/fmap.rs" 103 8 103 26 @@ -375,9 +375,9 @@ module M_collections__roundtrip_hashmap_iter [#"collections.rs" 32 0 32 97] let%span shash_map5 = "../../../../creusot-contracts/src/std/collections/hash_map.rs" 125 20 125 54 let%span shash_map6 = "../../../../creusot-contracts/src/std/collections/hash_map.rs" 108 12 118 29 let%span sfmap7 = "../../../../creusot-contracts/src/logic/fmap.rs" 92 8 95 9 - let%span smodel8 = "../../../../creusot-contracts/src/model.rs" 83 8 83 28 + let%span smodel8 = "../../../../creusot-contracts/src/model.rs" 45 8 45 28 let%span sseq9 = "../../../../creusot-contracts/src/logic/seq.rs" 355 20 355 77 - let%span smodel10 = "../../../../creusot-contracts/src/model.rs" 92 8 92 22 + let%span smodel10 = "../../../../creusot-contracts/src/model.rs" 54 8 54 22 let%span shash_map11 = "../../../../creusot-contracts/src/std/collections/hash_map.rs" 245 20 247 86 let%span shash_map12 = "../../../../creusot-contracts/src/std/collections/hash_map.rs" 130 14 130 45 let%span shash_map13 = "../../../../creusot-contracts/src/std/collections/hash_map.rs" 128 4 128 10 @@ -386,7 +386,7 @@ module M_collections__roundtrip_hashmap_iter [#"collections.rs" 32 0 32 97] let%span shash_map16 = "../../../../creusot-contracts/src/std/collections/hash_map.rs" 137 14 137 42 let%span shash_map17 = "../../../../creusot-contracts/src/std/collections/hash_map.rs" 139 8 139 104 let%span sresolve18 = "../../../../creusot-contracts/src/resolve.rs" 54 20 54 34 - let%span smodel19 = "../../../../creusot-contracts/src/model.rs" 110 8 110 22 + let%span smodel19 = "../../../../creusot-contracts/src/model.rs" 72 8 72 22 let%span sfmap20 = "../../../../creusot-contracts/src/logic/fmap.rs" 139 8 139 34 let%span sfmap21 = "../../../../creusot-contracts/src/logic/fmap.rs" 48 14 48 25 let%span sfmap22 = "../../../../creusot-contracts/src/logic/fmap.rs" 103 8 103 26 @@ -695,9 +695,9 @@ module M_collections__roundtrip_hashmap_iter_mut [#"collections.rs" 48 0 50 24] let%span shash_map7 = "../../../../creusot-contracts/src/std/collections/hash_map.rs" 177 20 177 54 let%span shash_map8 = "../../../../creusot-contracts/src/std/collections/hash_map.rs" 160 12 170 29 let%span sfmap9 = "../../../../creusot-contracts/src/logic/fmap.rs" 92 8 95 9 - let%span smodel10 = "../../../../creusot-contracts/src/model.rs" 83 8 83 28 + let%span smodel10 = "../../../../creusot-contracts/src/model.rs" 45 8 45 28 let%span sseq11 = "../../../../creusot-contracts/src/logic/seq.rs" 355 20 355 77 - let%span smodel12 = "../../../../creusot-contracts/src/model.rs" 110 8 110 22 + let%span smodel12 = "../../../../creusot-contracts/src/model.rs" 72 8 72 22 let%span sfmap13 = "../../../../creusot-contracts/src/logic/fmap.rs" 132 8 132 35 let%span sfmap14 = "../../../../creusot-contracts/src/logic/fmap.rs" 228 8 228 24 let%span shash_map15 = "../../../../creusot-contracts/src/std/collections/hash_map.rs" 233 20 235 112 @@ -1081,7 +1081,7 @@ module M_collections__roundtrip_hashset_into_iter [#"collections.rs" 64 0 64 90] let%span shash_set11 = "../../../../creusot-contracts/src/std/collections/hash_set.rs" 107 15 107 32 let%span shash_set12 = "../../../../creusot-contracts/src/std/collections/hash_set.rs" 108 14 108 42 let%span shash_set13 = "../../../../creusot-contracts/src/std/collections/hash_set.rs" 110 8 110 43 - let%span smodel14 = "../../../../creusot-contracts/src/model.rs" 110 8 110 22 + let%span smodel14 = "../../../../creusot-contracts/src/model.rs" 72 8 72 22 let%span shash_set15 = "../../../../creusot-contracts/src/std/collections/hash_set.rs" 58 16 65 23 let%span sfset16 = "../../../../creusot-contracts/src/logic/fset.rs" 46 8 46 26 let%span sseq17 = "../../../../creusot-contracts/src/logic/seq.rs" 355 20 355 77 @@ -1374,7 +1374,7 @@ module M_collections__roundtrip_hashset_iter [#"collections.rs" 69 0 69 87] let%span scollections0 = "collections.rs" 68 10 68 24 let%span shash_set1 = "../../../../creusot-contracts/src/std/collections/hash_set.rs" 19 0 38 1 let%span siter2 = "../../../../creusot-contracts/src/std/iter.rs" 166 26 167 120 - let%span smodel3 = "../../../../creusot-contracts/src/model.rs" 92 8 92 22 + let%span smodel3 = "../../../../creusot-contracts/src/model.rs" 54 8 54 22 let%span shash_set4 = "../../../../creusot-contracts/src/std/collections/hash_set.rs" 135 20 135 38 let%span shash_set5 = "../../../../creusot-contracts/src/std/collections/hash_set.rs" 129 8 129 38 let%span shash_set6 = "../../../../creusot-contracts/src/std/collections/hash_set.rs" 185 20 185 121 @@ -1384,10 +1384,10 @@ module M_collections__roundtrip_hashset_iter [#"collections.rs" 69 0 69 87] let%span shash_set10 = "../../../../creusot-contracts/src/std/collections/hash_set.rs" 146 15 146 32 let%span shash_set11 = "../../../../creusot-contracts/src/std/collections/hash_set.rs" 147 14 147 42 let%span shash_set12 = "../../../../creusot-contracts/src/std/collections/hash_set.rs" 149 8 149 43 - let%span smodel13 = "../../../../creusot-contracts/src/model.rs" 110 8 110 22 + let%span smodel13 = "../../../../creusot-contracts/src/model.rs" 72 8 72 22 let%span shash_set14 = "../../../../creusot-contracts/src/std/collections/hash_set.rs" 58 16 65 23 let%span sfset15 = "../../../../creusot-contracts/src/logic/fset.rs" 46 8 46 26 - let%span smodel16 = "../../../../creusot-contracts/src/model.rs" 83 8 83 28 + let%span smodel16 = "../../../../creusot-contracts/src/model.rs" 45 8 45 28 let%span sseq17 = "../../../../creusot-contracts/src/logic/seq.rs" 355 20 355 77 let%span shash_set18 = "../../../../creusot-contracts/src/std/collections/hash_set.rs" 71 11 71 33 let%span shash_set19 = "../../../../creusot-contracts/src/std/collections/hash_set.rs" 72 11 72 33 @@ -1617,7 +1617,7 @@ module M_collections__hashset_intersection [#"collections.rs" 74 0 77 15] let%span shash_set1 = "../../../../creusot-contracts/src/std/collections/hash_set.rs" 32 30 32 67 let%span siter2 = "../../../../creusot-contracts/src/std/iter.rs" 97 0 205 1 let%span siter3 = "../../../../creusot-contracts/src/std/iter.rs" 166 26 167 120 - let%span smodel4 = "../../../../creusot-contracts/src/model.rs" 92 8 92 22 + let%span smodel4 = "../../../../creusot-contracts/src/model.rs" 54 8 54 22 let%span scopied5 = "../../../../creusot-contracts/src/std/iter/copied.rs" 11 14 11 39 let%span scopied6 = "../../../../creusot-contracts/src/std/iter/copied.rs" 40 12 40 105 let%span scopied7 = "../../../../creusot-contracts/src/std/iter/copied.rs" 48 12 51 79 @@ -1638,13 +1638,13 @@ module M_collections__hashset_intersection [#"collections.rs" 74 0 77 15] let%span shash_set22 = "../../../../creusot-contracts/src/std/collections/hash_set.rs" 222 14 222 42 let%span shash_set23 = "../../../../creusot-contracts/src/std/collections/hash_set.rs" 224 8 224 43 let%span sresolve24 = "../../../../creusot-contracts/src/resolve.rs" 54 20 54 34 - let%span smodel25 = "../../../../creusot-contracts/src/model.rs" 110 8 110 22 + let%span smodel25 = "../../../../creusot-contracts/src/model.rs" 72 8 72 22 let%span shash_set26 = "../../../../creusot-contracts/src/std/collections/hash_set.rs" 58 16 65 23 let%span shash_set27 = "../../../../creusot-contracts/src/std/collections/hash_set.rs" 71 11 71 33 let%span shash_set28 = "../../../../creusot-contracts/src/std/collections/hash_set.rs" 72 11 72 33 let%span shash_set29 = "../../../../creusot-contracts/src/std/collections/hash_set.rs" 73 10 73 43 let%span shash_set30 = "../../../../creusot-contracts/src/std/collections/hash_set.rs" 81 4 81 31 - let%span smodel31 = "../../../../creusot-contracts/src/model.rs" 83 8 83 28 + let%span smodel31 = "../../../../creusot-contracts/src/model.rs" 45 8 45 28 let%span sseq32 = "../../../../creusot-contracts/src/logic/seq.rs" 382 14 383 65 let%span sseq33 = "../../../../creusot-contracts/src/logic/seq.rs" 381 4 381 12 diff --git a/creusot/tests/should_succeed/cc/iter.coma b/creusot/tests/should_succeed/cc/iter.coma index ddb4b17c1..b63771334 100644 --- a/creusot/tests/should_succeed/cc/iter.coma +++ b/creusot/tests/should_succeed/cc/iter.coma @@ -9,20 +9,20 @@ module M_iter__test_mut_ref [#"iter.rs" 3 0 3 21] let%span sslice7 = "../../../../creusot-contracts/src/std/slice.rs" 398 20 398 61 let%span sslice8 = "../../../../creusot-contracts/src/std/slice.rs" 405 12 405 66 let%span sresolve9 = "../../../../creusot-contracts/src/resolve.rs" 54 20 54 34 - let%span smodel10 = "../../../../creusot-contracts/src/model.rs" 83 8 83 28 + let%span smodel10 = "../../../../creusot-contracts/src/model.rs" 45 8 45 28 let%span sslice11 = "../../../../creusot-contracts/src/std/slice.rs" 411 14 411 45 let%span sslice12 = "../../../../creusot-contracts/src/std/slice.rs" 409 4 409 10 let%span sslice13 = "../../../../creusot-contracts/src/std/slice.rs" 416 15 416 32 let%span sslice14 = "../../../../creusot-contracts/src/std/slice.rs" 417 15 417 32 let%span sslice15 = "../../../../creusot-contracts/src/std/slice.rs" 418 14 418 42 let%span sslice16 = "../../../../creusot-contracts/src/std/slice.rs" 414 4 414 10 - let%span smodel17 = "../../../../creusot-contracts/src/model.rs" 110 8 110 22 + let%span smodel17 = "../../../../creusot-contracts/src/model.rs" 72 8 72 22 let%span sslice18 = "../../../../creusot-contracts/src/std/slice.rs" 28 14 28 41 let%span sslice19 = "../../../../creusot-contracts/src/std/slice.rs" 29 14 29 42 let%span sslice20 = "../../../../creusot-contracts/src/std/slice.rs" 96 14 96 41 let%span sslice21 = "../../../../creusot-contracts/src/std/slice.rs" 97 14 97 80 let%span soption22 = "../../../../creusot-contracts/src/std/option.rs" 11 8 14 9 - let%span smodel23 = "../../../../creusot-contracts/src/model.rs" 92 8 92 22 + let%span smodel23 = "../../../../creusot-contracts/src/model.rs" 54 8 54 22 let%span sindex24 = "../../../../creusot-contracts/src/logic/ops/index.rs" 49 8 49 31 let%span snum25 = "../../../../creusot-contracts/src/std/num.rs" 21 28 21 33 diff --git a/creusot/tests/should_succeed/cell/02.coma b/creusot/tests/should_succeed/cell/02.coma index 183ebd43f..5bc5a7224 100644 --- a/creusot/tests/should_succeed/cell/02.coma +++ b/creusot/tests/should_succeed/cell/02.coma @@ -84,7 +84,7 @@ module M_02__fib_memo [#"02.rs" 95 0 95 50] let%span s0226 = "02.rs" 24 22 24 23 let%span s0227 = "02.rs" 23 4 23 38 let%span s0228 = "02.rs" 86 8 86 47 - let%span smodel29 = "../../../../creusot-contracts/src/model.rs" 92 8 92 22 + let%span smodel29 = "../../../../creusot-contracts/src/model.rs" 54 8 54 22 let%span sslice30 = "../../../../creusot-contracts/src/std/slice.rs" 122 20 122 37 let%span sslice31 = "../../../../creusot-contracts/src/std/slice.rs" 129 20 129 37 let%span s0232 = "02.rs" 72 12 75 13 diff --git a/creusot/tests/should_succeed/constrained_types.coma b/creusot/tests/should_succeed/constrained_types.coma index 4d3be16c1..fdd4e3fd9 100644 --- a/creusot/tests/should_succeed/constrained_types.coma +++ b/creusot/tests/should_succeed/constrained_types.coma @@ -1,6 +1,6 @@ module M_constrained_types__uses_concrete_instance [#"constrained_types.rs" 14 0 14 67] let%span sconstrained_types0 = "constrained_types.rs" 9 18 9 68 - let%span smodel1 = "../../../creusot-contracts/src/model.rs" 83 8 83 28 + let%span smodel1 = "../../../creusot-contracts/src/model.rs" 45 8 45 28 let%span sord2 = "../../../creusot-contracts/src/logic/ord.rs" 282 20 282 67 let%span stuples3 = "../../../creusot-contracts/src/std/tuples.rs" 29 28 29 57 let%span sord4 = "../../../creusot-contracts/src/logic/ord.rs" 129 39 129 89 diff --git a/creusot/tests/should_succeed/duration.coma b/creusot/tests/should_succeed/duration.coma index a18fae485..6e06384c1 100644 --- a/creusot/tests/should_succeed/duration.coma +++ b/creusot/tests/should_succeed/duration.coma @@ -71,7 +71,7 @@ module M_duration__test_duration [#"duration.rs" 7 0 7 22] let%span stime69 = "../../../creusot-contracts/src/std/time.rs" 191 0 226 1 let%span stime70 = "../../../creusot-contracts/src/std/time.rs" 42 4 42 25 let%span stime71 = "../../../creusot-contracts/src/std/time.rs" 48 4 48 24 - let%span smodel72 = "../../../creusot-contracts/src/model.rs" 92 8 92 22 + let%span smodel72 = "../../../creusot-contracts/src/model.rs" 54 8 54 22 let%span stime73 = "../../../creusot-contracts/src/std/time.rs" 36 4 36 21 let%span stime74 = "../../../creusot-contracts/src/std/time.rs" 31 4 31 17 let%span soption75 = "../../../creusot-contracts/src/std/option.rs" 11 8 14 9 diff --git a/creusot/tests/should_succeed/filter_positive.coma b/creusot/tests/should_succeed/filter_positive.coma index 4f44d47ec..478e451ad 100644 --- a/creusot/tests/should_succeed/filter_positive.coma +++ b/creusot/tests/should_succeed/filter_positive.coma @@ -157,11 +157,11 @@ module M_filter_positive__m [#"filter_positive.rs" 82 0 82 33] let%span svec36 = "../../../creusot-contracts/src/std/vec.rs" 154 26 154 57 let%span svec37 = "../../../creusot-contracts/src/std/vec.rs" 155 26 155 62 let%span svec38 = "../../../creusot-contracts/src/std/vec.rs" 156 26 156 55 - let%span smodel39 = "../../../creusot-contracts/src/model.rs" 92 8 92 22 + let%span smodel39 = "../../../creusot-contracts/src/model.rs" 54 8 54 22 let%span sslice40 = "../../../creusot-contracts/src/std/slice.rs" 122 20 122 37 let%span sslice41 = "../../../creusot-contracts/src/std/slice.rs" 129 20 129 37 let%span sindex42 = "../../../creusot-contracts/src/logic/ops/index.rs" 27 8 27 31 - let%span smodel43 = "../../../creusot-contracts/src/model.rs" 110 8 110 22 + let%span smodel43 = "../../../creusot-contracts/src/model.rs" 72 8 72 22 let%span sslice44 = "../../../creusot-contracts/src/std/slice.rs" 136 20 136 94 let%span sresolve45 = "../../../creusot-contracts/src/resolve.rs" 54 20 54 34 diff --git a/creusot/tests/should_succeed/hashmap.coma b/creusot/tests/should_succeed/hashmap.coma index 96141d19c..be6bbafa5 100644 --- a/creusot/tests/should_succeed/hashmap.coma +++ b/creusot/tests/should_succeed/hashmap.coma @@ -77,7 +77,7 @@ module M_hashmap__qyi15610519155507183510__resolve_coherence [#"hashmap.rs" 63 4 end module M_hashmap__qyi9060063638777358169__hash [#"hashmap.rs" 77 4 77 25] (* *) let%span shashmap0 = "hashmap.rs" 76 14 76 58 - let%span smodel1 = "../../../creusot-contracts/src/model.rs" 83 8 83 28 + let%span smodel1 = "../../../creusot-contracts/src/model.rs" 45 8 45 28 let%span shashmap2 = "hashmap.rs" 83 20 83 21 let%span snum3 = "../../../creusot-contracts/src/std/num.rs" 21 28 21 33 @@ -558,9 +558,9 @@ module M_hashmap__qyi7664122466964245986__add [#"hashmap.rs" 158 4 158 41] (* My let%span shashmap24 = "hashmap.rs" 133 12 133 91 let%span scmp25 = "../../../creusot-contracts/src/std/cmp.rs" 11 26 11 75 let%span shashmap26 = "hashmap.rs" 97 8 97 33 - let%span smodel27 = "../../../creusot-contracts/src/model.rs" 110 8 110 22 - let%span smodel28 = "../../../creusot-contracts/src/model.rs" 92 8 92 22 - let%span smodel29 = "../../../creusot-contracts/src/model.rs" 83 8 83 28 + let%span smodel27 = "../../../creusot-contracts/src/model.rs" 72 8 72 22 + let%span smodel28 = "../../../creusot-contracts/src/model.rs" 54 8 54 22 + let%span smodel29 = "../../../creusot-contracts/src/model.rs" 45 8 45 28 let%span sslice30 = "../../../creusot-contracts/src/std/slice.rs" 122 20 122 37 let%span sslice31 = "../../../creusot-contracts/src/std/slice.rs" 129 20 129 37 let%span svec32 = "../../../creusot-contracts/src/std/vec.rs" 18 14 18 41 @@ -1138,8 +1138,8 @@ module M_hashmap__qyi7664122466964245986__get [#"hashmap.rs" 190 4 190 43] (* My let%span shashmap12 = "hashmap.rs" 122 8 122 53 let%span shashmap13 = "hashmap.rs" 31 12 34 13 let%span scmp14 = "../../../creusot-contracts/src/std/cmp.rs" 11 26 11 75 - let%span smodel15 = "../../../creusot-contracts/src/model.rs" 92 8 92 22 - let%span smodel16 = "../../../creusot-contracts/src/model.rs" 83 8 83 28 + let%span smodel15 = "../../../creusot-contracts/src/model.rs" 54 8 54 22 + let%span smodel16 = "../../../creusot-contracts/src/model.rs" 45 8 45 28 let%span sslice17 = "../../../creusot-contracts/src/std/slice.rs" 122 20 122 37 let%span sslice18 = "../../../creusot-contracts/src/std/slice.rs" 129 20 129 37 let%span shashmap19 = "hashmap.rs" 127 20 127 66 @@ -1519,8 +1519,8 @@ module M_hashmap__qyi7664122466964245986__resize [#"hashmap.rs" 209 4 209 24] (* let%span shashmap42 = "hashmap.rs" 158 26 158 29 let%span shashmap43 = "hashmap.rs" 158 34 158 37 let%span shashmap44 = "hashmap.rs" 157 14 157 122 - let%span smodel45 = "../../../creusot-contracts/src/model.rs" 110 8 110 22 - let%span smodel46 = "../../../creusot-contracts/src/model.rs" 92 8 92 22 + let%span smodel45 = "../../../creusot-contracts/src/model.rs" 72 8 72 22 + let%span smodel46 = "../../../creusot-contracts/src/model.rs" 54 8 54 22 let%span shashmap47 = "hashmap.rs" 122 8 122 53 let%span sslice48 = "../../../creusot-contracts/src/std/slice.rs" 122 20 122 37 let%span sslice49 = "../../../creusot-contracts/src/std/slice.rs" 129 20 129 37 @@ -2061,9 +2061,9 @@ module M_hashmap__main [#"hashmap.rs" 249 0 249 13] let%span shashmap27 = "hashmap.rs" 158 34 158 37 let%span shashmap28 = "hashmap.rs" 157 14 157 122 let%span shashmap29 = "hashmap.rs" 97 8 97 33 - let%span smodel30 = "../../../creusot-contracts/src/model.rs" 92 8 92 22 + let%span smodel30 = "../../../creusot-contracts/src/model.rs" 54 8 54 22 let%span snum31 = "../../../creusot-contracts/src/std/num.rs" 21 28 21 33 - let%span smodel32 = "../../../creusot-contracts/src/model.rs" 110 8 110 22 + let%span smodel32 = "../../../creusot-contracts/src/model.rs" 72 8 72 22 let%span shashmap33 = "hashmap.rs" 122 8 122 53 let%span shashmap34 = "hashmap.rs" 31 12 34 13 let%span shashmap35 = "hashmap.rs" 143 12 144 139 @@ -2701,7 +2701,7 @@ module M_hashmap__qyi15467499327297494705__resolve_coherence__refines [#"hashmap end module M_hashmap__qyi9060063638777358169__hash__refines [#"hashmap.rs" 77 4 77 25] (* *) let%span shashmap0 = "hashmap.rs" 77 4 77 25 - let%span smodel1 = "../../../creusot-contracts/src/model.rs" 83 8 83 28 + let%span smodel1 = "../../../creusot-contracts/src/model.rs" 45 8 45 28 let%span shashmap2 = "hashmap.rs" 83 20 83 21 let%span snum3 = "../../../creusot-contracts/src/std/num.rs" 21 28 21 33 diff --git a/creusot/tests/should_succeed/heapsort_generic.coma b/creusot/tests/should_succeed/heapsort_generic.coma index ac5ca7141..4976af901 100644 --- a/creusot/tests/should_succeed/heapsort_generic.coma +++ b/creusot/tests/should_succeed/heapsort_generic.coma @@ -134,8 +134,8 @@ module M_heapsort_generic__sift_down [#"heapsort_generic.rs" 41 0 43 29] let%span sheapsort_generic21 = "heapsort_generic.rs" 36 10 37 41 let%span sheapsort_generic22 = "heapsort_generic.rs" 38 10 40 78 let%span sheapsort_generic23 = "heapsort_generic.rs" 11 4 11 19 - let%span smodel24 = "../../../creusot-contracts/src/model.rs" 101 8 101 28 - let%span smodel25 = "../../../creusot-contracts/src/model.rs" 110 8 110 22 + let%span smodel24 = "../../../creusot-contracts/src/model.rs" 63 8 63 28 + let%span smodel25 = "../../../creusot-contracts/src/model.rs" 72 8 72 22 let%span sindex26 = "../../../creusot-contracts/src/logic/ops/index.rs" 27 8 27 31 let%span ssnapshot27 = "../../../creusot-contracts/src/snapshot.rs" 52 20 52 39 let%span sseq28 = "../../../creusot-contracts/src/logic/seq.rs" 316 8 316 41 @@ -165,10 +165,10 @@ module M_heapsort_generic__sift_down [#"heapsort_generic.rs" 41 0 43 29] let%span sord52 = "../../../creusot-contracts/src/logic/ord.rs" 89 15 89 48 let%span sord53 = "../../../creusot-contracts/src/logic/ord.rs" 90 14 90 44 let%span sord54 = "../../../creusot-contracts/src/logic/ord.rs" 95 14 95 59 - let%span smodel55 = "../../../creusot-contracts/src/model.rs" 92 8 92 22 + let%span smodel55 = "../../../creusot-contracts/src/model.rs" 54 8 54 22 let%span sslice56 = "../../../creusot-contracts/src/std/slice.rs" 122 20 122 37 let%span sslice57 = "../../../creusot-contracts/src/std/slice.rs" 129 20 129 37 - let%span smodel58 = "../../../creusot-contracts/src/model.rs" 83 8 83 28 + let%span smodel58 = "../../../creusot-contracts/src/model.rs" 45 8 45 28 let%span sslice59 = "../../../creusot-contracts/src/std/slice.rs" 28 14 28 41 let%span sslice60 = "../../../creusot-contracts/src/std/slice.rs" 29 14 29 42 let%span sresolve61 = "../../../creusot-contracts/src/resolve.rs" 54 20 54 34 @@ -638,8 +638,8 @@ module M_heapsort_generic__heap_sort [#"heapsort_generic.rs" 94 0 96 29] let%span sheapsort_generic21 = "heapsort_generic.rs" 92 10 92 35 let%span sheapsort_generic22 = "heapsort_generic.rs" 93 10 93 34 let%span svec23 = "../../../creusot-contracts/src/std/vec.rs" 83 26 83 48 - let%span smodel24 = "../../../creusot-contracts/src/model.rs" 110 8 110 22 - let%span smodel25 = "../../../creusot-contracts/src/model.rs" 101 8 101 28 + let%span smodel24 = "../../../creusot-contracts/src/model.rs" 72 8 72 22 + let%span smodel25 = "../../../creusot-contracts/src/model.rs" 63 8 63 28 let%span sheapsort_generic26 = "heapsort_generic.rs" 16 16 17 24 let%span ssnapshot27 = "../../../creusot-contracts/src/snapshot.rs" 52 20 52 39 let%span sseq28 = "../../../creusot-contracts/src/logic/seq.rs" 316 8 316 41 @@ -666,7 +666,7 @@ module M_heapsort_generic__heap_sort [#"heapsort_generic.rs" 94 0 96 29] let%span svec49 = "../../../creusot-contracts/src/std/vec.rs" 30 14 31 51 let%span sheapsort_generic50 = "heapsort_generic.rs" 87 8 87 35 let%span svec51 = "../../../creusot-contracts/src/std/vec.rs" 18 14 18 41 - let%span smodel52 = "../../../creusot-contracts/src/model.rs" 92 8 92 22 + let%span smodel52 = "../../../creusot-contracts/src/model.rs" 54 8 54 22 let%span sheapsort_generic53 = "heapsort_generic.rs" 11 4 11 19 let%span sindex54 = "../../../creusot-contracts/src/logic/ops/index.rs" 27 8 27 31 let%span sord55 = "../../../creusot-contracts/src/logic/ord.rs" 29 14 29 64 diff --git a/creusot/tests/should_succeed/hillel.coma b/creusot/tests/should_succeed/hillel.coma index 92d67b95c..5d4472aea 100644 --- a/creusot/tests/should_succeed/hillel.coma +++ b/creusot/tests/should_succeed/hillel.coma @@ -14,12 +14,12 @@ module M_hillel__right_pad [#"hillel.rs" 17 0 17 59] let%span shillel12 = "hillel.rs" 15 10 15 73 let%span shillel13 = "hillel.rs" 16 10 16 73 let%span ssnapshot14 = "../../../creusot-contracts/src/snapshot.rs" 52 20 52 39 - let%span smodel15 = "../../../creusot-contracts/src/model.rs" 110 8 110 22 + let%span smodel15 = "../../../creusot-contracts/src/model.rs" 72 8 72 22 let%span sindex16 = "../../../creusot-contracts/src/logic/ops/index.rs" 27 8 27 31 let%span svec17 = "../../../creusot-contracts/src/std/vec.rs" 83 26 83 48 let%span svec18 = "../../../creusot-contracts/src/std/vec.rs" 87 26 87 56 let%span svec19 = "../../../creusot-contracts/src/std/vec.rs" 18 14 18 41 - let%span smodel20 = "../../../creusot-contracts/src/model.rs" 92 8 92 22 + let%span smodel20 = "../../../creusot-contracts/src/model.rs" 54 8 54 22 let%span sresolve21 = "../../../creusot-contracts/src/resolve.rs" 54 20 54 34 let%span svec22 = "../../../creusot-contracts/src/std/vec.rs" 65 20 65 41 let%span sinvariant23 = "../../../creusot-contracts/src/invariant.rs" 34 20 34 44 @@ -230,7 +230,7 @@ module M_hillel__left_pad [#"hillel.rs" 34 0 34 58] let%span shillel14 = "hillel.rs" 32 10 32 88 let%span shillel15 = "hillel.rs" 33 10 33 104 let%span sindex16 = "../../../creusot-contracts/src/logic/ops/index.rs" 27 8 27 31 - let%span smodel17 = "../../../creusot-contracts/src/model.rs" 110 8 110 22 + let%span smodel17 = "../../../creusot-contracts/src/model.rs" 72 8 72 22 let%span ssnapshot18 = "../../../creusot-contracts/src/snapshot.rs" 52 20 52 39 let%span svec19 = "../../../creusot-contracts/src/std/vec.rs" 83 26 83 48 let%span svec20 = "../../../creusot-contracts/src/std/vec.rs" 107 26 107 59 @@ -238,7 +238,7 @@ module M_hillel__left_pad [#"hillel.rs" 34 0 34 58] let%span svec22 = "../../../creusot-contracts/src/std/vec.rs" 109 26 109 52 let%span svec23 = "../../../creusot-contracts/src/std/vec.rs" 110 26 110 103 let%span svec24 = "../../../creusot-contracts/src/std/vec.rs" 18 14 18 41 - let%span smodel25 = "../../../creusot-contracts/src/model.rs" 92 8 92 22 + let%span smodel25 = "../../../creusot-contracts/src/model.rs" 54 8 54 22 let%span sresolve26 = "../../../creusot-contracts/src/resolve.rs" 54 20 54 34 let%span svec27 = "../../../creusot-contracts/src/std/vec.rs" 65 20 65 41 let%span sinvariant28 = "../../../creusot-contracts/src/invariant.rs" 34 20 34 44 @@ -500,13 +500,13 @@ module M_hillel__insert_unique [#"hillel.rs" 80 0 80 62] let%span shillel18 = "hillel.rs" 79 10 79 58 let%span shillel19 = "hillel.rs" 72 10 72 41 let%span shillel20 = "hillel.rs" 71 0 71 8 - let%span smodel21 = "../../../creusot-contracts/src/model.rs" 101 8 101 28 + let%span smodel21 = "../../../creusot-contracts/src/model.rs" 63 8 63 28 let%span shillel22 = "hillel.rs" 67 8 67 72 let%span svec23 = "../../../creusot-contracts/src/std/vec.rs" 169 26 169 42 let%span sslice24 = "../../../creusot-contracts/src/std/slice.rs" 245 0 354 1 let%span siter25 = "../../../creusot-contracts/src/std/iter.rs" 97 0 205 1 let%span sindex26 = "../../../creusot-contracts/src/logic/ops/index.rs" 93 8 93 33 - let%span smodel27 = "../../../creusot-contracts/src/model.rs" 83 8 83 28 + let%span smodel27 = "../../../creusot-contracts/src/model.rs" 45 8 45 28 let%span sslice28 = "../../../creusot-contracts/src/std/slice.rs" 405 12 405 66 let%span siter29 = "../../../creusot-contracts/src/std/iter.rs" 103 26 106 17 let%span sindex30 = "../../../creusot-contracts/src/logic/ops/index.rs" 27 8 27 31 @@ -516,7 +516,7 @@ module M_hillel__insert_unique [#"hillel.rs" 80 0 80 62] let%span svec34 = "../../../creusot-contracts/src/std/vec.rs" 87 26 87 56 let%span svec35 = "../../../creusot-contracts/src/std/vec.rs" 29 14 29 47 let%span svec36 = "../../../creusot-contracts/src/std/vec.rs" 30 14 31 51 - let%span smodel37 = "../../../creusot-contracts/src/model.rs" 92 8 92 22 + let%span smodel37 = "../../../creusot-contracts/src/model.rs" 54 8 54 22 let%span siter38 = "../../../creusot-contracts/src/std/iter.rs" 82 20 82 24 let%span siter39 = "../../../creusot-contracts/src/std/iter.rs" 88 8 88 19 let%span sslice40 = "../../../creusot-contracts/src/std/slice.rs" 411 14 411 45 @@ -530,7 +530,7 @@ module M_hillel__insert_unique [#"hillel.rs" 80 0 80 62] let%span sslice48 = "../../../creusot-contracts/src/std/slice.rs" 398 20 398 61 let%span sresolve49 = "../../../creusot-contracts/src/resolve.rs" 54 20 54 34 let%span svec50 = "../../../creusot-contracts/src/std/vec.rs" 18 14 18 41 - let%span smodel51 = "../../../creusot-contracts/src/model.rs" 110 8 110 22 + let%span smodel51 = "../../../creusot-contracts/src/model.rs" 72 8 72 22 let%span sslice52 = "../../../creusot-contracts/src/std/slice.rs" 28 14 28 41 let%span sslice53 = "../../../creusot-contracts/src/std/slice.rs" 29 14 29 42 let%span sindex54 = "../../../creusot-contracts/src/logic/ops/index.rs" 49 8 49 31 @@ -1019,7 +1019,7 @@ module M_hillel__unique [#"hillel.rs" 102 0 102 56] let%span svec20 = "../../../creusot-contracts/src/std/vec.rs" 74 26 74 44 let%span sslice21 = "../../../creusot-contracts/src/std/slice.rs" 245 0 354 1 let%span siter22 = "../../../creusot-contracts/src/std/iter.rs" 97 0 205 1 - let%span smodel23 = "../../../creusot-contracts/src/model.rs" 83 8 83 28 + let%span smodel23 = "../../../creusot-contracts/src/model.rs" 45 8 45 28 let%span svec24 = "../../../creusot-contracts/src/std/vec.rs" 29 14 29 47 let%span svec25 = "../../../creusot-contracts/src/std/vec.rs" 30 14 31 51 let%span shillel26 = "hillel.rs" 67 8 67 72 @@ -1033,7 +1033,7 @@ module M_hillel__unique [#"hillel.rs" 102 0 102 56] let%span shillel34 = "hillel.rs" 77 10 77 58 let%span shillel35 = "hillel.rs" 78 10 78 87 let%span shillel36 = "hillel.rs" 79 10 79 58 - let%span smodel37 = "../../../creusot-contracts/src/model.rs" 92 8 92 22 + let%span smodel37 = "../../../creusot-contracts/src/model.rs" 54 8 54 22 let%span svec38 = "../../../creusot-contracts/src/std/vec.rs" 18 14 18 41 let%span siter39 = "../../../creusot-contracts/src/std/iter.rs" 82 20 82 24 let%span siter40 = "../../../creusot-contracts/src/std/iter.rs" 88 8 88 19 @@ -1048,7 +1048,7 @@ module M_hillel__unique [#"hillel.rs" 102 0 102 56] let%span snum49 = "../../../creusot-contracts/src/std/num.rs" 21 28 21 33 let%span srange50 = "../../../creusot-contracts/src/std/iter/range.rs" 14 12 14 78 let%span sresolve51 = "../../../creusot-contracts/src/resolve.rs" 54 20 54 34 - let%span smodel52 = "../../../creusot-contracts/src/model.rs" 101 8 101 28 + let%span smodel52 = "../../../creusot-contracts/src/model.rs" 63 8 63 28 let%span sslice53 = "../../../creusot-contracts/src/std/slice.rs" 28 14 28 41 let%span sslice54 = "../../../creusot-contracts/src/std/slice.rs" 29 14 29 42 let%span sindex55 = "../../../creusot-contracts/src/logic/ops/index.rs" 49 8 49 31 @@ -1671,7 +1671,7 @@ module M_hillel__fulcrum [#"hillel.rs" 159 0 159 30] let%span shillel23 = "hillel.rs" 157 10 157 44 let%span shillel24 = "hillel.rs" 158 10 158 86 let%span siter25 = "../../../creusot-contracts/src/std/iter.rs" 97 0 205 1 - let%span smodel26 = "../../../creusot-contracts/src/model.rs" 92 8 92 22 + let%span smodel26 = "../../../creusot-contracts/src/model.rs" 54 8 54 22 let%span shillel27 = "hillel.rs" 123 11 123 53 let%span shillel28 = "hillel.rs" 124 10 124 21 let%span shillel29 = "hillel.rs" 122 10 122 19 @@ -1713,7 +1713,7 @@ module M_hillel__fulcrum [#"hillel.rs" 159 0 159 30] let%span snum65 = "../../../creusot-contracts/src/std/num.rs" 21 28 21 33 let%span srange66 = "../../../creusot-contracts/src/std/iter/range.rs" 14 12 14 78 let%span sindex67 = "../../../creusot-contracts/src/logic/ops/index.rs" 49 8 49 31 - let%span smodel68 = "../../../creusot-contracts/src/model.rs" 110 8 110 22 + let%span smodel68 = "../../../creusot-contracts/src/model.rs" 72 8 72 22 use prelude.prelude.UInt32 diff --git a/creusot/tests/should_succeed/index_range.coma b/creusot/tests/should_succeed/index_range.coma index 08b3cd649..42d908e95 100644 --- a/creusot/tests/should_succeed/index_range.coma +++ b/creusot/tests/should_succeed/index_range.coma @@ -10,7 +10,7 @@ module M_index_range__create_arr [#"index_range.rs" 14 0 14 27] let%span svec8 = "../../../creusot-contracts/src/std/vec.rs" 87 26 87 56 let%span svec9 = "../../../creusot-contracts/src/std/vec.rs" 18 14 18 41 let%span sindex10 = "../../../creusot-contracts/src/logic/ops/index.rs" 27 8 27 31 - let%span smodel11 = "../../../creusot-contracts/src/model.rs" 110 8 110 22 + let%span smodel11 = "../../../creusot-contracts/src/model.rs" 72 8 72 22 use prelude.prelude.Opaque @@ -230,10 +230,10 @@ module M_index_range__test_range [#"index_range.rs" 27 0 27 19] let%span svec85 = "../../../creusot-contracts/src/std/vec.rs" 83 26 83 48 let%span svec86 = "../../../creusot-contracts/src/std/vec.rs" 18 14 18 41 let%span sindex87 = "../../../creusot-contracts/src/logic/ops/index.rs" 27 8 27 31 - let%span smodel88 = "../../../creusot-contracts/src/model.rs" 92 8 92 22 + let%span smodel88 = "../../../creusot-contracts/src/model.rs" 54 8 54 22 let%span sslice89 = "../../../creusot-contracts/src/std/slice.rs" 144 20 144 70 let%span sslice90 = "../../../creusot-contracts/src/std/slice.rs" 150 20 150 67 - let%span smodel91 = "../../../creusot-contracts/src/model.rs" 110 8 110 22 + let%span smodel91 = "../../../creusot-contracts/src/model.rs" 72 8 72 22 let%span sslice92 = "../../../creusot-contracts/src/std/slice.rs" 157 12 158 32 let%span sresolve93 = "../../../creusot-contracts/src/resolve.rs" 54 20 54 34 let%span sslice94 = "../../../creusot-contracts/src/std/slice.rs" 122 20 122 37 @@ -862,10 +862,10 @@ module M_index_range__test_range_to [#"index_range.rs" 78 0 78 22] let%span svec58 = "../../../creusot-contracts/src/std/vec.rs" 83 26 83 48 let%span svec59 = "../../../creusot-contracts/src/std/vec.rs" 18 14 18 41 let%span sindex60 = "../../../creusot-contracts/src/logic/ops/index.rs" 27 8 27 31 - let%span smodel61 = "../../../creusot-contracts/src/model.rs" 92 8 92 22 + let%span smodel61 = "../../../creusot-contracts/src/model.rs" 54 8 54 22 let%span sslice62 = "../../../creusot-contracts/src/std/slice.rs" 167 20 167 42 let%span sslice63 = "../../../creusot-contracts/src/std/slice.rs" 173 20 173 57 - let%span smodel64 = "../../../creusot-contracts/src/model.rs" 110 8 110 22 + let%span smodel64 = "../../../creusot-contracts/src/model.rs" 72 8 72 22 let%span sslice65 = "../../../creusot-contracts/src/std/slice.rs" 179 20 179 88 let%span sresolve66 = "../../../creusot-contracts/src/resolve.rs" 54 20 54 34 let%span sslice67 = "../../../creusot-contracts/src/std/slice.rs" 122 20 122 37 @@ -1350,10 +1350,10 @@ module M_index_range__test_range_from [#"index_range.rs" 115 0 115 24] let%span svec60 = "../../../creusot-contracts/src/std/vec.rs" 83 26 83 48 let%span svec61 = "../../../creusot-contracts/src/std/vec.rs" 18 14 18 41 let%span sindex62 = "../../../creusot-contracts/src/logic/ops/index.rs" 27 8 27 31 - let%span smodel63 = "../../../creusot-contracts/src/model.rs" 92 8 92 22 + let%span smodel63 = "../../../creusot-contracts/src/model.rs" 54 8 54 22 let%span sslice64 = "../../../creusot-contracts/src/std/slice.rs" 187 20 187 44 let%span sslice65 = "../../../creusot-contracts/src/std/slice.rs" 193 20 193 67 - let%span smodel66 = "../../../creusot-contracts/src/model.rs" 110 8 110 22 + let%span smodel66 = "../../../creusot-contracts/src/model.rs" 72 8 72 22 let%span sslice67 = "../../../creusot-contracts/src/std/slice.rs" 200 12 200 91 let%span sresolve68 = "../../../creusot-contracts/src/resolve.rs" 54 20 54 34 let%span sslice69 = "../../../creusot-contracts/src/std/slice.rs" 122 20 122 37 @@ -1843,10 +1843,10 @@ module M_index_range__test_range_full [#"index_range.rs" 154 0 154 24] let%span svec52 = "../../../creusot-contracts/src/std/vec.rs" 83 26 83 48 let%span svec53 = "../../../creusot-contracts/src/std/vec.rs" 18 14 18 41 let%span sindex54 = "../../../creusot-contracts/src/logic/ops/index.rs" 27 8 27 31 - let%span smodel55 = "../../../creusot-contracts/src/model.rs" 92 8 92 22 + let%span smodel55 = "../../../creusot-contracts/src/model.rs" 54 8 54 22 let%span sslice56 = "../../../creusot-contracts/src/std/slice.rs" 209 20 209 24 let%span sslice57 = "../../../creusot-contracts/src/std/slice.rs" 215 20 215 31 - let%span smodel58 = "../../../creusot-contracts/src/model.rs" 110 8 110 22 + let%span smodel58 = "../../../creusot-contracts/src/model.rs" 72 8 72 22 let%span sslice59 = "../../../creusot-contracts/src/std/slice.rs" 221 20 221 24 let%span sresolve60 = "../../../creusot-contracts/src/resolve.rs" 54 20 54 34 let%span sslice61 = "../../../creusot-contracts/src/std/slice.rs" 122 20 122 37 @@ -2301,10 +2301,10 @@ module M_index_range__test_range_to_inclusive [#"index_range.rs" 179 0 179 32] let%span svec55 = "../../../creusot-contracts/src/std/vec.rs" 83 26 83 48 let%span svec56 = "../../../creusot-contracts/src/std/vec.rs" 18 14 18 41 let%span sindex57 = "../../../creusot-contracts/src/logic/ops/index.rs" 27 8 27 31 - let%span smodel58 = "../../../creusot-contracts/src/model.rs" 92 8 92 22 + let%span smodel58 = "../../../creusot-contracts/src/model.rs" 54 8 54 22 let%span sslice59 = "../../../creusot-contracts/src/std/slice.rs" 229 20 229 41 let%span sslice60 = "../../../creusot-contracts/src/std/slice.rs" 235 20 235 61 - let%span smodel61 = "../../../creusot-contracts/src/model.rs" 110 8 110 22 + let%span smodel61 = "../../../creusot-contracts/src/model.rs" 72 8 72 22 let%span sslice62 = "../../../creusot-contracts/src/std/slice.rs" 241 20 241 87 let%span sresolve63 = "../../../creusot-contracts/src/resolve.rs" 54 20 54 34 let%span sslice64 = "../../../creusot-contracts/src/std/slice.rs" 122 20 122 37 diff --git a/creusot/tests/should_succeed/inferred_invariants.coma b/creusot/tests/should_succeed/inferred_invariants.coma index f941ed1c8..26fcfcd86 100644 --- a/creusot/tests/should_succeed/inferred_invariants.coma +++ b/creusot/tests/should_succeed/inferred_invariants.coma @@ -269,14 +269,14 @@ module M_inferred_invariants__y [#"inferred_invariants.rs" 41 0 41 26] let%span sinferred_invariants5 = "inferred_invariants.rs" 51 13 51 14 let%span sinferred_invariants6 = "inferred_invariants.rs" 52 15 52 17 let%span ssnapshot7 = "../../../creusot-contracts/src/snapshot.rs" 52 20 52 39 - let%span smodel8 = "../../../creusot-contracts/src/model.rs" 110 8 110 22 + let%span smodel8 = "../../../creusot-contracts/src/model.rs" 72 8 72 22 let%span svec9 = "../../../creusot-contracts/src/std/vec.rs" 83 26 83 48 let%span svec10 = "../../../creusot-contracts/src/std/vec.rs" 152 27 152 46 let%span svec11 = "../../../creusot-contracts/src/std/vec.rs" 153 26 153 54 let%span svec12 = "../../../creusot-contracts/src/std/vec.rs" 154 26 154 57 let%span svec13 = "../../../creusot-contracts/src/std/vec.rs" 155 26 155 62 let%span svec14 = "../../../creusot-contracts/src/std/vec.rs" 156 26 156 55 - let%span smodel15 = "../../../creusot-contracts/src/model.rs" 92 8 92 22 + let%span smodel15 = "../../../creusot-contracts/src/model.rs" 54 8 54 22 let%span svec16 = "../../../creusot-contracts/src/std/vec.rs" 18 14 18 41 let%span sslice17 = "../../../creusot-contracts/src/std/slice.rs" 122 20 122 37 let%span sslice18 = "../../../creusot-contracts/src/std/slice.rs" 129 20 129 37 diff --git a/creusot/tests/should_succeed/insertion_sort.coma b/creusot/tests/should_succeed/insertion_sort.coma index 76c9889d8..1dd9528e8 100644 --- a/creusot/tests/should_succeed/insertion_sort.coma +++ b/creusot/tests/should_succeed/insertion_sort.coma @@ -25,7 +25,7 @@ module M_insertion_sort__insertion_sort [#"insertion_sort.rs" 21 0 21 40] let%span sslice23 = "../../../creusot-contracts/src/std/slice.rs" 245 0 354 1 let%span siter24 = "../../../creusot-contracts/src/std/iter.rs" 97 0 205 1 let%span ssnapshot25 = "../../../creusot-contracts/src/snapshot.rs" 52 20 52 39 - let%span smodel26 = "../../../creusot-contracts/src/model.rs" 110 8 110 22 + let%span smodel26 = "../../../creusot-contracts/src/model.rs" 72 8 72 22 let%span sseq27 = "../../../creusot-contracts/src/logic/seq.rs" 316 8 316 41 let%span sinsertion_sort28 = "insertion_sort.rs" 8 8 8 72 let%span srange29 = "../../../creusot-contracts/src/std/iter/range.rs" 22 12 26 70 @@ -38,7 +38,7 @@ module M_insertion_sort__insertion_sort [#"insertion_sort.rs" 21 0 21 40] let%span sslice36 = "../../../creusot-contracts/src/std/slice.rs" 28 14 28 41 let%span sslice37 = "../../../creusot-contracts/src/std/slice.rs" 29 14 29 42 let%span sinsertion_sort38 = "insertion_sort.rs" 15 8 15 35 - let%span smodel39 = "../../../creusot-contracts/src/model.rs" 92 8 92 22 + let%span smodel39 = "../../../creusot-contracts/src/model.rs" 54 8 54 22 let%span siter40 = "../../../creusot-contracts/src/std/iter.rs" 82 20 82 24 let%span siter41 = "../../../creusot-contracts/src/std/iter.rs" 88 8 88 19 let%span srange42 = "../../../creusot-contracts/src/std/iter/range.rs" 32 14 32 45 diff --git a/creusot/tests/should_succeed/instant.coma b/creusot/tests/should_succeed/instant.coma index 8bf92b98e..0e5ab7964 100644 --- a/creusot/tests/should_succeed/instant.coma +++ b/creusot/tests/should_succeed/instant.coma @@ -41,9 +41,9 @@ module M_instant__test_instant [#"instant.rs" 7 0 7 21] let%span soption39 = "../../../creusot-contracts/src/std/option.rs" 51 26 51 51 let%span stime40 = "../../../creusot-contracts/src/std/time.rs" 12 14 12 77 let%span stime41 = "../../../creusot-contracts/src/std/time.rs" 48 4 48 24 - let%span smodel42 = "../../../creusot-contracts/src/model.rs" 83 8 83 28 + let%span smodel42 = "../../../creusot-contracts/src/model.rs" 45 8 45 28 let%span soption43 = "../../../creusot-contracts/src/std/option.rs" 11 8 14 9 - let%span smodel44 = "../../../creusot-contracts/src/model.rs" 92 8 92 22 + let%span smodel44 = "../../../creusot-contracts/src/model.rs" 54 8 54 22 let%span sord45 = "../../../creusot-contracts/src/logic/ord.rs" 36 20 36 53 let%span sord46 = "../../../creusot-contracts/src/logic/ord.rs" 58 20 58 56 let%span stime47 = "../../../creusot-contracts/src/std/time.rs" 24 8 24 19 diff --git a/creusot/tests/should_succeed/invariant_moves.coma b/creusot/tests/should_succeed/invariant_moves.coma index 3d863dacd..6d588a16b 100644 --- a/creusot/tests/should_succeed/invariant_moves.coma +++ b/creusot/tests/should_succeed/invariant_moves.coma @@ -2,7 +2,7 @@ module M_invariant_moves__test_invariant_move [#"invariant_moves.rs" 5 0 5 43] let%span sinvariant_moves0 = "invariant_moves.rs" 6 16 6 22 let%span svec1 = "../../../creusot-contracts/src/std/vec.rs" 91 26 96 17 let%span svec2 = "../../../creusot-contracts/src/std/vec.rs" 18 14 18 41 - let%span smodel3 = "../../../creusot-contracts/src/model.rs" 110 8 110 22 + let%span smodel3 = "../../../creusot-contracts/src/model.rs" 72 8 72 22 let%span sresolve4 = "../../../creusot-contracts/src/resolve.rs" 54 20 54 34 use prelude.prelude.Borrow diff --git a/creusot/tests/should_succeed/ite_normalize.coma b/creusot/tests/should_succeed/ite_normalize.coma index 687d1bf00..79fb3cbee 100644 --- a/creusot/tests/should_succeed/ite_normalize.coma +++ b/creusot/tests/should_succeed/ite_normalize.coma @@ -512,10 +512,10 @@ module M_ite_normalize__qyi17570407315987535457__simplify_helper [#"ite_normaliz let%span site_normalize15 = "ite_normalize.rs" 127 8 140 9 let%span site_normalize16 = "ite_normalize.rs" 170 8 176 9 let%span site_normalize17 = "ite_normalize.rs" 159 8 165 9 - let%span smodel18 = "../../../creusot-contracts/src/model.rs" 92 8 92 22 - let%span smodel19 = "../../../creusot-contracts/src/model.rs" 83 8 83 28 + let%span smodel18 = "../../../creusot-contracts/src/model.rs" 54 8 54 22 + let%span smodel19 = "../../../creusot-contracts/src/model.rs" 45 8 45 28 let%span snum20 = "../../../creusot-contracts/src/std/num.rs" 21 28 21 33 - let%span smodel21 = "../../../creusot-contracts/src/model.rs" 110 8 110 22 + let%span smodel21 = "../../../creusot-contracts/src/model.rs" 72 8 72 22 use prelude.prelude.UIntSize diff --git a/creusot/tests/should_succeed/iterators/02_iter_mut.coma b/creusot/tests/should_succeed/iterators/02_iter_mut.coma index d8c0cdad4..055ddfa71 100644 --- a/creusot/tests/should_succeed/iterators/02_iter_mut.coma +++ b/creusot/tests/should_succeed/iterators/02_iter_mut.coma @@ -37,7 +37,7 @@ module M_02_iter_mut__qyi4305820612590367313__produces_refl [#"02_iter_mut.rs" 5 let%span s02_iter_mut0 = "02_iter_mut.rs" 50 14 50 45 let%span s02_iter_mut1 = "02_iter_mut.rs" 48 4 48 10 let%span s02_iter_mut2 = "02_iter_mut.rs" 40 12 44 13 - let%span smodel3 = "../../../../creusot-contracts/src/model.rs" 110 8 110 22 + let%span smodel3 = "../../../../creusot-contracts/src/model.rs" 72 8 72 22 let%span sslice4 = "../../../../creusot-contracts/src/std/slice.rs" 87 14 87 41 let%span sslice5 = "../../../../creusot-contracts/src/std/slice.rs" 88 14 88 84 let%span sslice6 = "../../../../creusot-contracts/src/std/slice.rs" 28 14 28 41 @@ -122,7 +122,7 @@ module M_02_iter_mut__qyi4305820612590367313__produces_trans [#"02_iter_mut.rs" let%span s02_iter_mut2 = "02_iter_mut.rs" 57 14 57 42 let%span s02_iter_mut3 = "02_iter_mut.rs" 53 4 53 10 let%span s02_iter_mut4 = "02_iter_mut.rs" 40 12 44 13 - let%span smodel5 = "../../../../creusot-contracts/src/model.rs" 110 8 110 22 + let%span smodel5 = "../../../../creusot-contracts/src/model.rs" 72 8 72 22 let%span sslice6 = "../../../../creusot-contracts/src/std/slice.rs" 87 14 87 41 let%span sslice7 = "../../../../creusot-contracts/src/std/slice.rs" 88 14 88 84 let%span sslice8 = "../../../../creusot-contracts/src/std/slice.rs" 28 14 28 41 @@ -221,7 +221,7 @@ module M_02_iter_mut__qyi4305820612590367313__next [#"02_iter_mut.rs" 64 4 64 44 let%span sslice8 = "../../../../creusot-contracts/src/std/slice.rs" 29 14 29 42 let%span sseq9 = "../../../../creusot-contracts/src/logic/seq.rs" 173 8 173 39 let%span sresolve10 = "../../../../creusot-contracts/src/resolve.rs" 54 20 54 34 - let%span smodel11 = "../../../../creusot-contracts/src/model.rs" 110 8 110 22 + let%span smodel11 = "../../../../creusot-contracts/src/model.rs" 72 8 72 22 let%span sslice12 = "../../../../creusot-contracts/src/std/slice.rs" 87 14 87 41 let%span sslice13 = "../../../../creusot-contracts/src/std/slice.rs" 88 14 88 84 let%span sinvariant14 = "../../../../creusot-contracts/src/invariant.rs" 34 20 34 44 @@ -556,7 +556,7 @@ module M_02_iter_mut__iter_mut [#"02_iter_mut.rs" 79 0 79 55] let%span svec7 = "../../../../creusot-contracts/src/std/vec.rs" 154 26 154 57 let%span svec8 = "../../../../creusot-contracts/src/std/vec.rs" 155 26 155 62 let%span svec9 = "../../../../creusot-contracts/src/std/vec.rs" 156 26 156 55 - let%span smodel10 = "../../../../creusot-contracts/src/model.rs" 110 8 110 22 + let%span smodel10 = "../../../../creusot-contracts/src/model.rs" 72 8 72 22 let%span sslice11 = "../../../../creusot-contracts/src/std/slice.rs" 28 14 28 41 let%span sslice12 = "../../../../creusot-contracts/src/std/slice.rs" 29 14 29 42 let%span svec13 = "../../../../creusot-contracts/src/std/vec.rs" 18 14 18 41 @@ -804,7 +804,7 @@ module M_02_iter_mut__all_zero [#"02_iter_mut.rs" 85 0 85 35] let%span s02_iter_mut20 = "02_iter_mut.rs" 64 26 64 44 let%span s02_iter_mut21 = "02_iter_mut.rs" 60 14 63 5 let%span svec22 = "../../../../creusot-contracts/src/std/vec.rs" 18 14 18 41 - let%span smodel23 = "../../../../creusot-contracts/src/model.rs" 110 8 110 22 + let%span smodel23 = "../../../../creusot-contracts/src/model.rs" 72 8 72 22 let%span sindex24 = "../../../../creusot-contracts/src/logic/ops/index.rs" 27 8 27 31 let%span sslice25 = "../../../../creusot-contracts/src/std/slice.rs" 28 14 28 41 let%span sslice26 = "../../../../creusot-contracts/src/std/slice.rs" 29 14 29 42 @@ -1232,7 +1232,7 @@ end module M_02_iter_mut__qyi4305820612590367313__produces_trans__refines [#"02_iter_mut.rs" 58 4 58 90] (* as common::Iterator> *) let%span s02_iter_mut0 = "02_iter_mut.rs" 58 4 58 90 let%span s02_iter_mut1 = "02_iter_mut.rs" 40 12 44 13 - let%span smodel2 = "../../../../creusot-contracts/src/model.rs" 110 8 110 22 + let%span smodel2 = "../../../../creusot-contracts/src/model.rs" 72 8 72 22 let%span sslice3 = "../../../../creusot-contracts/src/std/slice.rs" 87 14 87 41 let%span sslice4 = "../../../../creusot-contracts/src/std/slice.rs" 88 14 88 84 let%span sslice5 = "../../../../creusot-contracts/src/std/slice.rs" 28 14 28 41 @@ -1313,7 +1313,7 @@ module M_02_iter_mut__qyi4305820612590367313__next__refines [#"02_iter_mut.rs" 6 let%span s02_iter_mut1 = "02_iter_mut.rs" 33 8 33 76 let%span s02_iter_mut2 = "02_iter_mut.rs" 40 12 44 13 let%span sresolve3 = "../../../../creusot-contracts/src/resolve.rs" 54 20 54 34 - let%span smodel4 = "../../../../creusot-contracts/src/model.rs" 110 8 110 22 + let%span smodel4 = "../../../../creusot-contracts/src/model.rs" 72 8 72 22 let%span sslice5 = "../../../../creusot-contracts/src/std/slice.rs" 87 14 87 41 let%span sslice6 = "../../../../creusot-contracts/src/std/slice.rs" 88 14 88 84 let%span sinvariant7 = "../../../../creusot-contracts/src/invariant.rs" 34 20 34 44 @@ -1488,7 +1488,7 @@ end module M_02_iter_mut__qyi4305820612590367313__produces_refl__refines [#"02_iter_mut.rs" 51 4 51 26] (* as common::Iterator> *) let%span s02_iter_mut0 = "02_iter_mut.rs" 51 4 51 26 let%span s02_iter_mut1 = "02_iter_mut.rs" 40 12 44 13 - let%span smodel2 = "../../../../creusot-contracts/src/model.rs" 110 8 110 22 + let%span smodel2 = "../../../../creusot-contracts/src/model.rs" 72 8 72 22 let%span sslice3 = "../../../../creusot-contracts/src/std/slice.rs" 87 14 87 41 let%span sslice4 = "../../../../creusot-contracts/src/std/slice.rs" 88 14 88 84 let%span sslice5 = "../../../../creusot-contracts/src/std/slice.rs" 28 14 28 41 diff --git a/creusot/tests/should_succeed/iterators/03_std_iterators.coma b/creusot/tests/should_succeed/iterators/03_std_iterators.coma index 1f3a9b3f1..4b64a7d56 100644 --- a/creusot/tests/should_succeed/iterators/03_std_iterators.coma +++ b/creusot/tests/should_succeed/iterators/03_std_iterators.coma @@ -13,7 +13,7 @@ module M_03_std_iterators__slice_iter [#"03_std_iterators.rs" 6 0 6 42] let%span siter11 = "../../../../creusot-contracts/src/std/iter.rs" 97 0 205 1 let%span sslice12 = "../../../../creusot-contracts/src/std/slice.rs" 405 12 405 66 let%span siter13 = "../../../../creusot-contracts/src/std/iter.rs" 103 26 106 17 - let%span smodel14 = "../../../../creusot-contracts/src/model.rs" 92 8 92 22 + let%span smodel14 = "../../../../creusot-contracts/src/model.rs" 54 8 54 22 let%span siter15 = "../../../../creusot-contracts/src/std/iter.rs" 82 20 82 24 let%span siter16 = "../../../../creusot-contracts/src/std/iter.rs" 88 8 88 19 let%span sslice17 = "../../../../creusot-contracts/src/std/slice.rs" 411 14 411 45 @@ -30,7 +30,7 @@ module M_03_std_iterators__slice_iter [#"03_std_iterators.rs" 6 0 6 42] let%span sslice28 = "../../../../creusot-contracts/src/std/slice.rs" 29 14 29 42 let%span sindex29 = "../../../../creusot-contracts/src/logic/ops/index.rs" 49 8 49 31 let%span sseq30 = "../../../../creusot-contracts/src/logic/seq.rs" 633 20 633 95 - let%span smodel31 = "../../../../creusot-contracts/src/model.rs" 110 8 110 22 + let%span smodel31 = "../../../../creusot-contracts/src/model.rs" 72 8 72 22 let%span sinvariant32 = "../../../../creusot-contracts/src/invariant.rs" 24 8 24 18 let%span sboxed33 = "../../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18 let%span sslice34 = "../../../../creusot-contracts/src/std/slice.rs" 18 20 18 30 @@ -325,7 +325,7 @@ module M_03_std_iterators__vec_iter [#"03_std_iterators.rs" 17 0 17 41] let%span siter10 = "../../../../creusot-contracts/src/std/iter.rs" 97 0 205 1 let%span sslice11 = "../../../../creusot-contracts/src/std/slice.rs" 405 12 405 66 let%span siter12 = "../../../../creusot-contracts/src/std/iter.rs" 103 26 106 17 - let%span smodel13 = "../../../../creusot-contracts/src/model.rs" 92 8 92 22 + let%span smodel13 = "../../../../creusot-contracts/src/model.rs" 54 8 54 22 let%span svec14 = "../../../../creusot-contracts/src/std/vec.rs" 205 20 205 24 let%span svec15 = "../../../../creusot-contracts/src/std/vec.rs" 211 20 211 34 let%span sslice16 = "../../../../creusot-contracts/src/std/slice.rs" 411 14 411 45 @@ -341,7 +341,7 @@ module M_03_std_iterators__vec_iter [#"03_std_iterators.rs" 17 0 17 41] let%span svec26 = "../../../../creusot-contracts/src/std/vec.rs" 18 14 18 41 let%span sindex27 = "../../../../creusot-contracts/src/logic/ops/index.rs" 49 8 49 31 let%span sseq28 = "../../../../creusot-contracts/src/logic/seq.rs" 633 20 633 95 - let%span smodel29 = "../../../../creusot-contracts/src/model.rs" 110 8 110 22 + let%span smodel29 = "../../../../creusot-contracts/src/model.rs" 72 8 72 22 let%span sslice30 = "../../../../creusot-contracts/src/std/slice.rs" 28 14 28 41 let%span sslice31 = "../../../../creusot-contracts/src/std/slice.rs" 29 14 29 42 let%span sinvariant32 = "../../../../creusot-contracts/src/invariant.rs" 24 8 24 18 @@ -655,7 +655,7 @@ module M_03_std_iterators__all_zero [#"03_std_iterators.rs" 28 0 28 35] let%span sslice13 = "../../../../creusot-contracts/src/std/slice.rs" 459 12 459 66 let%span siter14 = "../../../../creusot-contracts/src/std/iter.rs" 103 26 106 17 let%span svec15 = "../../../../creusot-contracts/src/std/vec.rs" 18 14 18 41 - let%span smodel16 = "../../../../creusot-contracts/src/model.rs" 110 8 110 22 + let%span smodel16 = "../../../../creusot-contracts/src/model.rs" 72 8 72 22 let%span sindex17 = "../../../../creusot-contracts/src/logic/ops/index.rs" 27 8 27 31 let%span sslice18 = "../../../../creusot-contracts/src/std/slice.rs" 28 14 28 41 let%span sslice19 = "../../../../creusot-contracts/src/std/slice.rs" 29 14 29 42 @@ -1277,7 +1277,7 @@ module M_03_std_iterators__counter [#"03_std_iterators.rs" 41 0 41 27] let%span siter15 = "../../../../creusot-contracts/src/std/iter.rs" 54 14 54 88 let%span siter16 = "../../../../creusot-contracts/src/std/iter.rs" 166 26 167 120 let%span svec17 = "../../../../creusot-contracts/src/std/vec.rs" 18 14 18 41 - let%span smodel18 = "../../../../creusot-contracts/src/model.rs" 92 8 92 22 + let%span smodel18 = "../../../../creusot-contracts/src/model.rs" 54 8 54 22 let%span sslice19 = "../../../../creusot-contracts/src/std/slice.rs" 411 14 411 45 let%span sslice20 = "../../../../creusot-contracts/src/std/slice.rs" 409 4 409 10 let%span sslice21 = "../../../../creusot-contracts/src/std/slice.rs" 416 15 416 32 @@ -1310,7 +1310,7 @@ module M_03_std_iterators__counter [#"03_std_iterators.rs" 41 0 41 27] let%span smap_inv48 = "../../../../creusot-contracts/src/std/iter/map_inv.rs" 29 15 29 32 let%span smap_inv49 = "../../../../creusot-contracts/src/std/iter/map_inv.rs" 30 14 30 42 let%span sindex50 = "../../../../creusot-contracts/src/logic/ops/index.rs" 49 8 49 31 - let%span smodel51 = "../../../../creusot-contracts/src/model.rs" 110 8 110 22 + let%span smodel51 = "../../../../creusot-contracts/src/model.rs" 72 8 72 22 use prelude.prelude.UIntSize @@ -2252,7 +2252,7 @@ module M_03_std_iterators__my_reverse [#"03_std_iterators.rs" 94 0 94 37] let%span s03_std_iterators19 = "03_std_iterators.rs" 94 21 94 26 let%span s03_std_iterators20 = "03_std_iterators.rs" 93 10 93 44 let%span sslice21 = "../../../../creusot-contracts/src/std/slice.rs" 245 0 354 1 - let%span smodel22 = "../../../../creusot-contracts/src/model.rs" 110 8 110 22 + let%span smodel22 = "../../../../creusot-contracts/src/model.rs" 72 8 72 22 let%span siter23 = "../../../../creusot-contracts/src/std/iter.rs" 159 27 159 48 let%span siter24 = "../../../../creusot-contracts/src/std/iter.rs" 97 0 205 1 let%span siter25 = "../../../../creusot-contracts/src/std/iter.rs" 161 26 161 62 @@ -2266,7 +2266,7 @@ module M_03_std_iterators__my_reverse [#"03_std_iterators.rs" 94 0 94 37] let%span sindex33 = "../../../../creusot-contracts/src/logic/ops/index.rs" 93 8 93 33 let%span sslice34 = "../../../../creusot-contracts/src/std/slice.rs" 28 14 28 41 let%span sslice35 = "../../../../creusot-contracts/src/std/slice.rs" 29 14 29 42 - let%span smodel36 = "../../../../creusot-contracts/src/model.rs" 92 8 92 22 + let%span smodel36 = "../../../../creusot-contracts/src/model.rs" 54 8 54 22 let%span siter37 = "../../../../creusot-contracts/src/std/iter.rs" 82 20 82 24 let%span szip38 = "../../../../creusot-contracts/src/std/iter/zip.rs" 14 14 14 39 let%span szip39 = "../../../../creusot-contracts/src/std/iter/zip.rs" 21 14 21 39 diff --git a/creusot/tests/should_succeed/iterators/08_collect_extend.coma b/creusot/tests/should_succeed/iterators/08_collect_extend.coma index 50f3f4a7e..41989e5fa 100644 --- a/creusot/tests/should_succeed/iterators/08_collect_extend.coma +++ b/creusot/tests/should_succeed/iterators/08_collect_extend.coma @@ -10,14 +10,14 @@ module M_08_collect_extend__extend [#"08_collect_extend.rs" 26 0 26 66] let%span s08_collect_extend8 = "08_collect_extend.rs" 26 58 26 62 let%span s08_collect_extend9 = "08_collect_extend.rs" 23 2 24 82 let%span siter10 = "../../../../creusot-contracts/src/std/iter.rs" 97 0 205 1 - let%span smodel11 = "../../../../creusot-contracts/src/model.rs" 110 8 110 22 + let%span smodel11 = "../../../../creusot-contracts/src/model.rs" 72 8 72 22 let%span ssnapshot12 = "../../../../creusot-contracts/src/snapshot.rs" 52 20 52 39 let%span siter13 = "../../../../creusot-contracts/src/std/iter.rs" 103 26 106 17 let%span svec14 = "../../../../creusot-contracts/src/std/vec.rs" 87 26 87 56 let%span svec15 = "../../../../creusot-contracts/src/std/vec.rs" 18 14 18 41 let%span siter16 = "../../../../creusot-contracts/src/std/iter.rs" 82 20 82 24 let%span siter17 = "../../../../creusot-contracts/src/std/iter.rs" 88 8 88 19 - let%span smodel18 = "../../../../creusot-contracts/src/model.rs" 92 8 92 22 + let%span smodel18 = "../../../../creusot-contracts/src/model.rs" 54 8 54 22 let%span siter19 = "../../../../creusot-contracts/src/std/iter.rs" 38 14 38 45 let%span siter20 = "../../../../creusot-contracts/src/std/iter.rs" 42 15 42 32 let%span siter21 = "../../../../creusot-contracts/src/std/iter.rs" 43 15 43 32 @@ -343,7 +343,7 @@ module M_08_collect_extend__collect [#"08_collect_extend.rs" 44 0 44 52] let%span siter19 = "../../../../creusot-contracts/src/std/iter.rs" 43 15 43 32 let%span siter20 = "../../../../creusot-contracts/src/std/iter.rs" 44 14 44 42 let%span sresolve21 = "../../../../creusot-contracts/src/resolve.rs" 54 20 54 34 - let%span smodel22 = "../../../../creusot-contracts/src/model.rs" 110 8 110 22 + let%span smodel22 = "../../../../creusot-contracts/src/model.rs" 72 8 72 22 let%span svec23 = "../../../../creusot-contracts/src/std/vec.rs" 65 20 65 41 let%span sseq24 = "../../../../creusot-contracts/src/logic/seq.rs" 633 20 633 95 let%span sinvariant25 = "../../../../creusot-contracts/src/invariant.rs" 34 20 34 44 @@ -631,9 +631,9 @@ module M_08_collect_extend__extend_index [#"08_collect_extend.rs" 55 0 55 51] let%span svec10 = "../../../../creusot-contracts/src/std/vec.rs" 197 20 197 33 let%span svec11 = "../../../../creusot-contracts/src/std/vec.rs" 257 20 257 57 let%span svec12 = "../../../../creusot-contracts/src/std/vec.rs" 264 12 264 41 - let%span smodel13 = "../../../../creusot-contracts/src/model.rs" 110 8 110 22 + let%span smodel13 = "../../../../creusot-contracts/src/model.rs" 72 8 72 22 let%span sresolve14 = "../../../../creusot-contracts/src/resolve.rs" 54 20 54 34 - let%span smodel15 = "../../../../creusot-contracts/src/model.rs" 92 8 92 22 + let%span smodel15 = "../../../../creusot-contracts/src/model.rs" 54 8 54 22 let%span svec16 = "../../../../creusot-contracts/src/std/vec.rs" 270 14 270 45 let%span svec17 = "../../../../creusot-contracts/src/std/vec.rs" 268 4 268 10 let%span svec18 = "../../../../creusot-contracts/src/std/vec.rs" 275 15 275 32 diff --git a/creusot/tests/should_succeed/iterators/17_filter.coma b/creusot/tests/should_succeed/iterators/17_filter.coma index 17b7e10dc..1cb486470 100644 --- a/creusot/tests/should_succeed/iterators/17_filter.coma +++ b/creusot/tests/should_succeed/iterators/17_filter.coma @@ -789,7 +789,7 @@ module M_17_filter__less_than [#"17_filter.rs" 120 0 120 49] let%span svec38 = "../../../../creusot-contracts/src/std/vec.rs" 276 15 276 32 let%span svec39 = "../../../../creusot-contracts/src/std/vec.rs" 277 14 277 42 let%span svec40 = "../../../../creusot-contracts/src/std/vec.rs" 273 4 273 10 - let%span smodel41 = "../../../../creusot-contracts/src/model.rs" 110 8 110 22 + let%span smodel41 = "../../../../creusot-contracts/src/model.rs" 72 8 72 22 use prelude.prelude.Opaque diff --git a/creusot/tests/should_succeed/knapsack.coma b/creusot/tests/should_succeed/knapsack.coma index 2f83db4b1..bfe92f8df 100644 --- a/creusot/tests/should_succeed/knapsack.coma +++ b/creusot/tests/should_succeed/knapsack.coma @@ -119,7 +119,7 @@ module M_knapsack__knapsack01_dyn [#"knapsack.rs" 49 0 49 91] let%span svec28 = "../../../creusot-contracts/src/std/vec.rs" 180 22 180 41 let%span svec29 = "../../../creusot-contracts/src/std/vec.rs" 181 22 181 76 let%span svec30 = "../../../creusot-contracts/src/std/vec.rs" 83 26 83 48 - let%span smodel31 = "../../../creusot-contracts/src/model.rs" 92 8 92 22 + let%span smodel31 = "../../../creusot-contracts/src/model.rs" 54 8 54 22 let%span sindex32 = "../../../creusot-contracts/src/logic/ops/index.rs" 27 8 27 31 let%span svec33 = "../../../creusot-contracts/src/std/vec.rs" 18 14 18 41 let%span sknapsack34 = "knapsack.rs" 32 11 32 37 @@ -140,7 +140,7 @@ module M_knapsack__knapsack01_dyn [#"knapsack.rs" 49 0 49 91] let%span svec49 = "../../../creusot-contracts/src/std/vec.rs" 87 26 87 56 let%span sslice50 = "../../../creusot-contracts/src/std/slice.rs" 122 20 122 37 let%span sslice51 = "../../../creusot-contracts/src/std/slice.rs" 129 20 129 37 - let%span smodel52 = "../../../creusot-contracts/src/model.rs" 110 8 110 22 + let%span smodel52 = "../../../creusot-contracts/src/model.rs" 72 8 72 22 let%span sslice53 = "../../../creusot-contracts/src/std/slice.rs" 136 20 136 94 let%span sresolve54 = "../../../creusot-contracts/src/resolve.rs" 54 20 54 34 let%span svec55 = "../../../creusot-contracts/src/std/vec.rs" 65 20 65 41 diff --git a/creusot/tests/should_succeed/knapsack_full.coma b/creusot/tests/should_succeed/knapsack_full.coma index 88a92da69..1fca60ab3 100644 --- a/creusot/tests/should_succeed/knapsack_full.coma +++ b/creusot/tests/should_succeed/knapsack_full.coma @@ -346,7 +346,7 @@ module M_knapsack_full__knapsack01_dyn [#"knapsack_full.rs" 86 0 86 91] let%span svec41 = "../../../creusot-contracts/src/std/vec.rs" 181 22 181 76 let%span svec42 = "../../../creusot-contracts/src/std/vec.rs" 83 26 83 48 let%span siter43 = "../../../creusot-contracts/src/std/iter.rs" 97 0 205 1 - let%span smodel44 = "../../../creusot-contracts/src/model.rs" 92 8 92 22 + let%span smodel44 = "../../../creusot-contracts/src/model.rs" 54 8 54 22 let%span sindex45 = "../../../creusot-contracts/src/logic/ops/index.rs" 27 8 27 31 let%span svec46 = "../../../creusot-contracts/src/std/vec.rs" 18 14 18 41 let%span sknapsack_full47 = "knapsack_full.rs" 61 11 61 37 @@ -403,7 +403,7 @@ module M_knapsack_full__knapsack01_dyn [#"knapsack_full.rs" 86 0 86 91] let%span srange98 = "../../../creusot-contracts/src/std/iter/range.rs" 45 10 45 43 let%span srange99 = "../../../creusot-contracts/src/std/iter/range.rs" 47 4 50 5 let%span srange100 = "../../../creusot-contracts/src/std/iter/range.rs" 58 12 58 57 - let%span smodel101 = "../../../creusot-contracts/src/model.rs" 110 8 110 22 + let%span smodel101 = "../../../creusot-contracts/src/model.rs" 72 8 72 22 let%span sslice102 = "../../../creusot-contracts/src/std/slice.rs" 136 20 136 94 let%span svec103 = "../../../creusot-contracts/src/std/vec.rs" 65 20 65 41 let%span sinvariant104 = "../../../creusot-contracts/src/invariant.rs" 24 8 24 18 diff --git a/creusot/tests/should_succeed/list_index_mut.coma b/creusot/tests/should_succeed/list_index_mut.coma index 06bec0cfb..2c04426ce 100644 --- a/creusot/tests/should_succeed/list_index_mut.coma +++ b/creusot/tests/should_succeed/list_index_mut.coma @@ -19,7 +19,7 @@ module M_list_index_mut__index_mut [#"list_index_mut.rs" 37 0 37 61] let%span soption17 = "../../../creusot-contracts/src/std/option.rs" 62 26 62 75 let%span soption18 = "../../../creusot-contracts/src/std/option.rs" 64 20 65 100 let%span soption19 = "../../../creusot-contracts/src/std/option.rs" 31 0 423 1 - let%span smodel20 = "../../../creusot-contracts/src/model.rs" 92 8 92 22 + let%span smodel20 = "../../../creusot-contracts/src/model.rs" 54 8 54 22 let%span sresolve21 = "../../../creusot-contracts/src/resolve.rs" 54 20 54 34 use prelude.prelude.Snapshot diff --git a/creusot/tests/should_succeed/list_reversal_lasso.coma b/creusot/tests/should_succeed/list_reversal_lasso.coma index e59eb2cb8..6259eab62 100644 --- a/creusot/tests/should_succeed/list_reversal_lasso.coma +++ b/creusot/tests/should_succeed/list_reversal_lasso.coma @@ -5,7 +5,7 @@ module M_list_reversal_lasso__qyi13715866738248475091__index [#"list_reversal_la let%span svec3 = "../../../creusot-contracts/src/std/vec.rs" 163 26 163 54 let%span slist_reversal_lasso4 = "list_reversal_lasso.rs" 50 20 50 70 let%span slist_reversal_lasso5 = "list_reversal_lasso.rs" 21 8 21 31 - let%span smodel6 = "../../../creusot-contracts/src/model.rs" 92 8 92 22 + let%span smodel6 = "../../../creusot-contracts/src/model.rs" 54 8 54 22 let%span sslice7 = "../../../creusot-contracts/src/std/slice.rs" 122 20 122 37 let%span sslice8 = "../../../creusot-contracts/src/std/slice.rs" 129 20 129 37 let%span svec9 = "../../../creusot-contracts/src/std/vec.rs" 18 14 18 41 @@ -122,7 +122,7 @@ module M_list_reversal_lasso__qyi14823043098042356205__index_mut [#"list_reversa let%span slist_reversal_lasso10 = "list_reversal_lasso.rs" 50 20 50 70 let%span slist_reversal_lasso11 = "list_reversal_lasso.rs" 21 8 21 31 let%span svec12 = "../../../creusot-contracts/src/std/vec.rs" 18 14 18 41 - let%span smodel13 = "../../../creusot-contracts/src/model.rs" 110 8 110 22 + let%span smodel13 = "../../../creusot-contracts/src/model.rs" 72 8 72 22 let%span sslice14 = "../../../creusot-contracts/src/std/slice.rs" 122 20 122 37 let%span sslice15 = "../../../creusot-contracts/src/std/slice.rs" 129 20 129 37 let%span sslice16 = "../../../creusot-contracts/src/std/slice.rs" 136 20 136 94 diff --git a/creusot/tests/should_succeed/mapping_test.coma b/creusot/tests/should_succeed/mapping_test.coma index c03443cf5..236a99cb7 100644 --- a/creusot/tests/should_succeed/mapping_test.coma +++ b/creusot/tests/should_succeed/mapping_test.coma @@ -7,9 +7,9 @@ module M_mapping_test__incr [#"mapping_test.rs" 29 0 29 18] let%span smapping_test5 = "mapping_test.rs" 28 11 28 37 let%span smapping_test6 = "mapping_test.rs" 19 8 20 72 let%span ssnapshot7 = "../../../creusot-contracts/src/snapshot.rs" 52 20 52 39 - let%span smodel8 = "../../../creusot-contracts/src/model.rs" 110 8 110 22 + let%span smodel8 = "../../../creusot-contracts/src/model.rs" 72 8 72 22 let%span sresolve9 = "../../../creusot-contracts/src/resolve.rs" 54 20 54 34 - let%span smodel10 = "../../../creusot-contracts/src/model.rs" 92 8 92 22 + let%span smodel10 = "../../../creusot-contracts/src/model.rs" 54 8 54 22 use prelude.prelude.Snapshot @@ -88,7 +88,7 @@ module M_mapping_test__f [#"mapping_test.rs" 37 0 37 10] let%span smapping_test6 = "mapping_test.rs" 26 12 26 24 let%span smapping_test7 = "mapping_test.rs" 27 12 27 26 let%span smapping_test8 = "mapping_test.rs" 28 11 28 37 - let%span smodel9 = "../../../creusot-contracts/src/model.rs" 110 8 110 22 + let%span smodel9 = "../../../creusot-contracts/src/model.rs" 72 8 72 22 let%span sresolve10 = "../../../creusot-contracts/src/resolve.rs" 54 20 54 34 use prelude.prelude.Int32 diff --git a/creusot/tests/should_succeed/option.coma b/creusot/tests/should_succeed/option.coma index 7d44d64cf..0dc705849 100644 --- a/creusot/tests/should_succeed/option.coma +++ b/creusot/tests/should_succeed/option.coma @@ -313,7 +313,7 @@ module M_option__map [#"option.rs" 44 0 44 12] let%span soption12 = "option.rs" 62 23 62 35 let%span soption13 = "option.rs" 63 22 63 39 let%span soption14 = "option.rs" 65 18 65 19 - let%span smodel15 = "../../../creusot-contracts/src/model.rs" 83 8 83 28 + let%span smodel15 = "../../../creusot-contracts/src/model.rs" 45 8 45 28 let%span soption16 = "../../../creusot-contracts/src/std/option.rs" 11 8 14 9 let%span stuples17 = "../../../creusot-contracts/src/std/tuples.rs" 9 20 9 22 let%span snum18 = "../../../creusot-contracts/src/std/num.rs" 21 28 21 33 @@ -581,7 +581,7 @@ module M_option__inspect [#"option.rs" 69 0 69 16] let%span soption7 = "../../../creusot-contracts/src/std/option.rs" 23 26 23 75 let%span soption8 = "option.rs" 81 22 81 26 let%span soption9 = "option.rs" 83 18 83 19 - let%span smodel10 = "../../../creusot-contracts/src/model.rs" 83 8 83 28 + let%span smodel10 = "../../../creusot-contracts/src/model.rs" 45 8 45 28 let%span soption11 = "../../../creusot-contracts/src/std/option.rs" 11 8 14 9 let%span snum12 = "../../../creusot-contracts/src/std/num.rs" 21 28 21 33 @@ -1644,7 +1644,7 @@ module M_option__and_or_xor [#"option.rs" 187 0 187 19] let%span soption26 = "option.rs" 203 38 203 39 let%span soption27 = "option.rs" 204 35 204 36 let%span sresolve28 = "../../../creusot-contracts/src/resolve.rs" 82 8 85 9 - let%span smodel29 = "../../../creusot-contracts/src/model.rs" 83 8 83 28 + let%span smodel29 = "../../../creusot-contracts/src/model.rs" 45 8 45 28 let%span soption30 = "../../../creusot-contracts/src/std/option.rs" 11 8 14 9 let%span snum31 = "../../../creusot-contracts/src/std/num.rs" 21 28 21 33 @@ -2007,7 +2007,7 @@ module M_option__and_then [#"option.rs" 208 0 208 17] let%span soption10 = "option.rs" 226 21 226 22 let%span soption11 = "option.rs" 219 15 223 7 let%span soption12 = "option.rs" 231 41 231 45 - let%span smodel13 = "../../../creusot-contracts/src/model.rs" 83 8 83 28 + let%span smodel13 = "../../../creusot-contracts/src/model.rs" 45 8 45 28 let%span soption14 = "../../../creusot-contracts/src/std/option.rs" 11 8 14 9 let%span snum15 = "../../../creusot-contracts/src/std/num.rs" 21 28 21 33 @@ -2230,8 +2230,8 @@ module M_option__filter [#"option.rs" 235 0 235 15] let%span soption10 = "option.rs" 249 18 249 22 let%span soption11 = "option.rs" 254 22 254 23 let%span soption12 = "option.rs" 253 22 253 41 - let%span smodel13 = "../../../creusot-contracts/src/model.rs" 83 8 83 28 - let%span smodel14 = "../../../creusot-contracts/src/model.rs" 92 8 92 22 + let%span smodel13 = "../../../creusot-contracts/src/model.rs" 45 8 45 28 + let%span smodel14 = "../../../creusot-contracts/src/model.rs" 54 8 54 22 let%span soption15 = "../../../creusot-contracts/src/std/option.rs" 11 8 14 9 let%span snum16 = "../../../creusot-contracts/src/std/num.rs" 21 28 21 33 @@ -2657,7 +2657,7 @@ module M_option__or_else [#"option.rs" 278 0 278 16] let%span soption10 = "option.rs" 290 22 290 36 let%span soption11 = "option.rs" 296 23 296 28 let%span soption12 = "option.rs" 298 18 298 19 - let%span smodel13 = "../../../creusot-contracts/src/model.rs" 83 8 83 28 + let%span smodel13 = "../../../creusot-contracts/src/model.rs" 45 8 45 28 let%span soption14 = "../../../creusot-contracts/src/std/option.rs" 11 8 14 9 let%span snum15 = "../../../creusot-contracts/src/std/num.rs" 21 28 21 33 @@ -2889,7 +2889,7 @@ module M_option__insert [#"option.rs" 302 0 302 15] let%span soption14 = "../../../creusot-contracts/src/std/option.rs" 23 26 23 75 let%span soption15 = "option.rs" 313 25 313 26 let%span sresolve16 = "../../../creusot-contracts/src/resolve.rs" 54 20 54 34 - let%span smodel17 = "../../../creusot-contracts/src/model.rs" 83 8 83 28 + let%span smodel17 = "../../../creusot-contracts/src/model.rs" 45 8 45 28 let%span soption18 = "../../../creusot-contracts/src/std/option.rs" 11 8 14 9 let%span snum19 = "../../../creusot-contracts/src/std/num.rs" 21 28 21 33 @@ -3077,7 +3077,7 @@ module M_option__get_or_insert [#"option.rs" 316 0 316 22] let%span soption29 = "option.rs" 342 19 342 24 let%span soption30 = "option.rs" 347 25 347 26 let%span sresolve31 = "../../../creusot-contracts/src/resolve.rs" 54 20 54 34 - let%span smodel32 = "../../../creusot-contracts/src/model.rs" 83 8 83 28 + let%span smodel32 = "../../../creusot-contracts/src/model.rs" 45 8 45 28 let%span soption33 = "../../../creusot-contracts/src/std/option.rs" 11 8 14 9 let%span snum34 = "../../../creusot-contracts/src/std/num.rs" 21 28 21 33 @@ -3479,7 +3479,7 @@ module M_option__take_if [#"option.rs" 360 0 360 16] let%span soption16 = "option.rs" 380 22 380 44 let%span soption17 = "option.rs" 381 22 381 32 let%span soption18 = "option.rs" 387 18 387 19 - let%span smodel19 = "../../../creusot-contracts/src/model.rs" 83 8 83 28 + let%span smodel19 = "../../../creusot-contracts/src/model.rs" 45 8 45 28 let%span sresolve20 = "../../../creusot-contracts/src/resolve.rs" 54 20 54 34 let%span soption21 = "../../../creusot-contracts/src/std/option.rs" 11 8 14 9 let%span snum22 = "../../../creusot-contracts/src/std/num.rs" 21 28 21 33 @@ -4066,11 +4066,11 @@ module M_option__zip_unzip [#"option.rs" 408 0 408 18] let%span soption17 = "option.rs" 426 33 426 34 let%span soption18 = "option.rs" 427 33 427 37 let%span sresolve19 = "../../../creusot-contracts/src/resolve.rs" 82 8 85 9 - let%span smodel20 = "../../../creusot-contracts/src/model.rs" 83 8 83 28 + let%span smodel20 = "../../../creusot-contracts/src/model.rs" 45 8 45 28 let%span soption21 = "../../../creusot-contracts/src/std/option.rs" 11 8 14 9 let%span stuples22 = "../../../creusot-contracts/src/std/tuples.rs" 29 28 29 57 let%span snum23 = "../../../creusot-contracts/src/std/num.rs" 21 28 21 33 - let%span smodel24 = "../../../creusot-contracts/src/model.rs" 120 8 120 12 + let%span smodel24 = "../../../creusot-contracts/src/model.rs" 82 8 82 12 use prelude.prelude.Int32 @@ -4406,7 +4406,7 @@ module M_option__transpose [#"option.rs" 430 0 430 18] let%span soption9 = "../../../creusot-contracts/src/std/option.rs" 23 26 23 75 let%span soption10 = "option.rs" 436 49 436 50 let%span sresult11 = "../../../creusot-contracts/src/std/result.rs" 67 27 67 54 - let%span smodel12 = "../../../creusot-contracts/src/model.rs" 83 8 83 28 + let%span smodel12 = "../../../creusot-contracts/src/model.rs" 45 8 45 28 let%span soption13 = "../../../creusot-contracts/src/std/option.rs" 11 8 14 9 let%span snum14 = "../../../creusot-contracts/src/std/num.rs" 21 28 21 33 diff --git a/creusot/tests/should_succeed/ord_trait.coma b/creusot/tests/should_succeed/ord_trait.coma index 305b2a651..9dbe3edb0 100644 --- a/creusot/tests/should_succeed/ord_trait.coma +++ b/creusot/tests/should_succeed/ord_trait.coma @@ -2,7 +2,7 @@ module M_ord_trait__x [#"ord_trait.rs" 5 0 7 29] let%span sord_trait0 = "ord_trait.rs" 5 29 5 30 let%span sord_trait1 = "ord_trait.rs" 4 10 4 24 let%span scmp2 = "../../../creusot-contracts/src/std/cmp.rs" 43 26 43 77 - let%span smodel3 = "../../../creusot-contracts/src/model.rs" 83 8 83 28 + let%span smodel3 = "../../../creusot-contracts/src/model.rs" 45 8 45 28 let%span sord4 = "../../../creusot-contracts/src/logic/ord.rs" 29 14 29 64 let%span sord5 = "../../../creusot-contracts/src/logic/ord.rs" 40 14 40 61 let%span sord6 = "../../../creusot-contracts/src/logic/ord.rs" 51 14 51 61 @@ -130,7 +130,7 @@ module M_ord_trait__gt_or_le [#"ord_trait.rs" 13 0 15 29] let%span sord_trait1 = "ord_trait.rs" 13 43 13 44 let%span sord_trait2 = "ord_trait.rs" 12 10 12 60 let%span scmp3 = "../../../creusot-contracts/src/std/cmp.rs" 59 26 59 77 - let%span smodel4 = "../../../creusot-contracts/src/model.rs" 83 8 83 28 + let%span smodel4 = "../../../creusot-contracts/src/model.rs" 45 8 45 28 let%span sord5 = "../../../creusot-contracts/src/logic/ord.rs" 29 14 29 64 let%span sord6 = "../../../creusot-contracts/src/logic/ord.rs" 40 14 40 61 let%span sord7 = "../../../creusot-contracts/src/logic/ord.rs" 51 14 51 61 diff --git a/creusot/tests/should_succeed/red_black_tree.coma b/creusot/tests/should_succeed/red_black_tree.coma index 4bfe8de61..86aa6d940 100644 --- a/creusot/tests/should_succeed/red_black_tree.coma +++ b/creusot/tests/should_succeed/red_black_tree.coma @@ -6671,7 +6671,7 @@ module M_red_black_tree__qyi2476155906044564626__delete_rec [#"red_black_tree.rs let%span sred_black_tree96 = "red_black_tree.rs" 256 16 256 48 let%span sred_black_tree97 = "red_black_tree.rs" 324 14 324 25 let%span sred_black_tree98 = "red_black_tree.rs" 327 12 335 13 - let%span smodel99 = "../../../creusot-contracts/src/model.rs" 83 8 83 28 + let%span smodel99 = "../../../creusot-contracts/src/model.rs" 45 8 45 28 let%span sred_black_tree100 = "red_black_tree.rs" 37 12 41 13 let%span sred_black_tree101 = "red_black_tree.rs" 297 12 303 13 let%span sred_black_tree102 = "red_black_tree.rs" 287 12 290 13 @@ -8358,7 +8358,7 @@ module M_red_black_tree__qyi1501420612169366910__insert [#"red_black_tree.rs" 80 let%span sred_black_tree19 = "red_black_tree.rs" 106 14 106 78 let%span sred_black_tree20 = "red_black_tree.rs" 112 12 112 61 let%span sred_black_tree21 = "red_black_tree.rs" 761 20 761 27 - let%span smodel22 = "../../../creusot-contracts/src/model.rs" 110 8 110 22 + let%span smodel22 = "../../../creusot-contracts/src/model.rs" 72 8 72 22 let%span sred_black_tree23 = "red_black_tree.rs" 387 12 387 59 let%span sred_black_tree24 = "red_black_tree.rs" 297 12 303 13 let%span sred_black_tree25 = "red_black_tree.rs" 324 14 324 25 @@ -8851,7 +8851,7 @@ module M_red_black_tree__qyi1501420612169366910__delete_max [#"red_black_tree.rs let%span sred_black_tree23 = "red_black_tree.rs" 105 15 105 35 let%span sred_black_tree24 = "red_black_tree.rs" 106 14 106 78 let%span sred_black_tree25 = "red_black_tree.rs" 112 12 112 61 - let%span smodel26 = "../../../creusot-contracts/src/model.rs" 110 8 110 22 + let%span smodel26 = "../../../creusot-contracts/src/model.rs" 72 8 72 22 let%span sred_black_tree27 = "red_black_tree.rs" 761 20 761 27 let%span sresolve28 = "../../../creusot-contracts/src/resolve.rs" 54 20 54 34 let%span sred_black_tree29 = "red_black_tree.rs" 287 12 290 13 @@ -9453,7 +9453,7 @@ module M_red_black_tree__qyi1501420612169366910__delete_min [#"red_black_tree.rs let%span soption20 = "../../../creusot-contracts/src/std/option.rs" 62 26 62 75 let%span soption21 = "../../../creusot-contracts/src/std/option.rs" 64 20 65 100 let%span soption22 = "../../../creusot-contracts/src/std/option.rs" 31 0 423 1 - let%span smodel23 = "../../../creusot-contracts/src/model.rs" 110 8 110 22 + let%span smodel23 = "../../../creusot-contracts/src/model.rs" 72 8 72 22 let%span sred_black_tree24 = "red_black_tree.rs" 761 20 761 27 let%span sred_black_tree25 = "red_black_tree.rs" 235 12 241 13 let%span sred_black_tree26 = "red_black_tree.rs" 37 12 41 13 @@ -10044,8 +10044,8 @@ module M_red_black_tree__qyi1501420612169366910__delete [#"red_black_tree.rs" 86 let%span soption22 = "../../../creusot-contracts/src/std/option.rs" 62 26 62 75 let%span soption23 = "../../../creusot-contracts/src/std/option.rs" 64 20 65 100 let%span soption24 = "../../../creusot-contracts/src/std/option.rs" 31 0 423 1 - let%span smodel25 = "../../../creusot-contracts/src/model.rs" 83 8 83 28 - let%span smodel26 = "../../../creusot-contracts/src/model.rs" 110 8 110 22 + let%span smodel25 = "../../../creusot-contracts/src/model.rs" 45 8 45 28 + let%span smodel26 = "../../../creusot-contracts/src/model.rs" 72 8 72 22 let%span sred_black_tree27 = "red_black_tree.rs" 761 20 761 27 let%span sred_black_tree28 = "red_black_tree.rs" 235 12 241 13 let%span sred_black_tree29 = "red_black_tree.rs" 37 12 41 13 @@ -10635,11 +10635,11 @@ module M_red_black_tree__qyi1501420612169366910__get [#"red_black_tree.rs" 889 4 let%span sred_black_tree8 = "red_black_tree.rs" 105 15 105 35 let%span sred_black_tree9 = "red_black_tree.rs" 106 14 106 78 let%span sred_black_tree10 = "red_black_tree.rs" 112 12 112 61 - let%span smodel11 = "../../../creusot-contracts/src/model.rs" 83 8 83 28 + let%span smodel11 = "../../../creusot-contracts/src/model.rs" 45 8 45 28 let%span sred_black_tree12 = "red_black_tree.rs" 37 12 41 13 let%span sred_black_tree13 = "red_black_tree.rs" 235 12 241 13 let%span scmp14 = "../../../creusot-contracts/src/std/cmp.rs" 72 26 72 85 - let%span smodel15 = "../../../creusot-contracts/src/model.rs" 92 8 92 22 + let%span smodel15 = "../../../creusot-contracts/src/model.rs" 54 8 54 22 let%span sred_black_tree16 = "red_black_tree.rs" 170 20 170 54 let%span sred_black_tree17 = "red_black_tree.rs" 67 14 68 91 let%span sred_black_tree18 = "red_black_tree.rs" 71 12 79 13 @@ -11078,11 +11078,11 @@ module M_red_black_tree__qyi1501420612169366910__get_mut [#"red_black_tree.rs" 9 let%span sred_black_tree22 = "red_black_tree.rs" 324 14 324 25 let%span sred_black_tree23 = "red_black_tree.rs" 327 12 335 13 let%span sred_black_tree24 = "red_black_tree.rs" 342 12 348 13 - let%span smodel25 = "../../../creusot-contracts/src/model.rs" 83 8 83 28 + let%span smodel25 = "../../../creusot-contracts/src/model.rs" 45 8 45 28 let%span sred_black_tree26 = "red_black_tree.rs" 235 12 241 13 let%span sred_black_tree27 = "red_black_tree.rs" 297 12 303 13 let%span scmp28 = "../../../creusot-contracts/src/std/cmp.rs" 72 26 72 85 - let%span smodel29 = "../../../creusot-contracts/src/model.rs" 110 8 110 22 + let%span smodel29 = "../../../creusot-contracts/src/model.rs" 72 8 72 22 let%span sred_black_tree30 = "red_black_tree.rs" 761 20 761 27 let%span sred_black_tree31 = "red_black_tree.rs" 170 20 170 54 let%span sred_black_tree32 = "red_black_tree.rs" 67 14 68 91 diff --git a/creusot/tests/should_succeed/rusthorn/inc_some_2_list.coma b/creusot/tests/should_succeed/rusthorn/inc_some_2_list.coma index cb0a1ed14..1c124ee6d 100644 --- a/creusot/tests/should_succeed/rusthorn/inc_some_2_list.coma +++ b/creusot/tests/should_succeed/rusthorn/inc_some_2_list.coma @@ -102,7 +102,7 @@ module M_inc_some_2_list__qyi7504674480942992291__take_some_rest [#"inc_some_2_l let%span sinc_some_2_list6 = "inc_some_2_list.rs" 32 15 32 19 let%span sinc_some_2_list7 = "inc_some_2_list.rs" 35 8 38 9 let%span sinc_some_2_list8 = "inc_some_2_list.rs" 23 12 26 13 - let%span smodel9 = "../../../../creusot-contracts/src/model.rs" 110 8 110 22 + let%span smodel9 = "../../../../creusot-contracts/src/model.rs" 72 8 72 22 let%span sresolve10 = "../../../../creusot-contracts/src/resolve.rs" 54 20 54 34 use prelude.prelude.UInt32 @@ -250,7 +250,7 @@ module M_inc_some_2_list__inc_some_2_list [#"inc_some_2_list.rs" 70 0 70 51] let%span sinc_some_2_list5 = "inc_some_2_list.rs" 52 14 52 37 let%span sinc_some_2_list6 = "inc_some_2_list.rs" 53 14 53 42 let%span sinc_some_2_list7 = "inc_some_2_list.rs" 23 12 26 13 - let%span smodel8 = "../../../../creusot-contracts/src/model.rs" 110 8 110 22 + let%span smodel8 = "../../../../creusot-contracts/src/model.rs" 72 8 72 22 let%span sresolve9 = "../../../../creusot-contracts/src/resolve.rs" 54 20 54 34 use prelude.prelude.UInt32 diff --git a/creusot/tests/should_succeed/rusthorn/inc_some_2_tree.coma b/creusot/tests/should_succeed/rusthorn/inc_some_2_tree.coma index 0ea809eba..1ede2e80a 100644 --- a/creusot/tests/should_succeed/rusthorn/inc_some_2_tree.coma +++ b/creusot/tests/should_succeed/rusthorn/inc_some_2_tree.coma @@ -135,7 +135,7 @@ module M_inc_some_2_tree__qyi9454558703362393917__take_some_rest [#"inc_some_2_t let%span sinc_some_2_tree8 = "inc_some_2_tree.rs" 31 15 31 19 let%span sinc_some_2_tree9 = "inc_some_2_tree.rs" 34 8 40 9 let%span sinc_some_2_tree10 = "inc_some_2_tree.rs" 23 12 26 13 - let%span smodel11 = "../../../../creusot-contracts/src/model.rs" 110 8 110 22 + let%span smodel11 = "../../../../creusot-contracts/src/model.rs" 72 8 72 22 let%span sresolve12 = "../../../../creusot-contracts/src/resolve.rs" 54 20 54 34 use prelude.prelude.UInt32 @@ -333,7 +333,7 @@ module M_inc_some_2_tree__inc_some_2_tree [#"inc_some_2_tree.rs" 85 0 85 51] let%span sinc_some_2_tree5 = "inc_some_2_tree.rs" 61 14 61 37 let%span sinc_some_2_tree6 = "inc_some_2_tree.rs" 62 14 62 42 let%span sinc_some_2_tree7 = "inc_some_2_tree.rs" 23 12 26 13 - let%span smodel8 = "../../../../creusot-contracts/src/model.rs" 110 8 110 22 + let%span smodel8 = "../../../../creusot-contracts/src/model.rs" 72 8 72 22 let%span sresolve9 = "../../../../creusot-contracts/src/resolve.rs" 54 20 54 34 use prelude.prelude.UInt32 diff --git a/creusot/tests/should_succeed/rusthorn/inc_some_list.coma b/creusot/tests/should_succeed/rusthorn/inc_some_list.coma index fbf930189..448abe444 100644 --- a/creusot/tests/should_succeed/rusthorn/inc_some_list.coma +++ b/creusot/tests/should_succeed/rusthorn/inc_some_list.coma @@ -101,7 +101,7 @@ module M_inc_some_list__qyi14489061725823948544__take_some [#"inc_some_list.rs" let%span sinc_some_list5 = "inc_some_list.rs" 31 15 31 19 let%span sinc_some_list6 = "inc_some_list.rs" 34 8 37 9 let%span sinc_some_list7 = "inc_some_list.rs" 23 12 26 13 - let%span smodel8 = "../../../../creusot-contracts/src/model.rs" 110 8 110 22 + let%span smodel8 = "../../../../creusot-contracts/src/model.rs" 72 8 72 22 let%span sresolve9 = "../../../../creusot-contracts/src/resolve.rs" 54 20 54 34 use prelude.prelude.UInt32 @@ -269,7 +269,7 @@ module M_inc_some_list__inc_some_list [#"inc_some_list.rs" 67 0 67 41] let%span sinc_some_list4 = "inc_some_list.rs" 49 14 49 64 let%span sinc_some_list5 = "inc_some_list.rs" 50 14 50 35 let%span sinc_some_list6 = "inc_some_list.rs" 23 12 26 13 - let%span smodel7 = "../../../../creusot-contracts/src/model.rs" 110 8 110 22 + let%span smodel7 = "../../../../creusot-contracts/src/model.rs" 72 8 72 22 let%span sresolve8 = "../../../../creusot-contracts/src/resolve.rs" 54 20 54 34 use prelude.prelude.UInt32 diff --git a/creusot/tests/should_succeed/rusthorn/inc_some_tree.coma b/creusot/tests/should_succeed/rusthorn/inc_some_tree.coma index ece78c965..b4974e9fd 100644 --- a/creusot/tests/should_succeed/rusthorn/inc_some_tree.coma +++ b/creusot/tests/should_succeed/rusthorn/inc_some_tree.coma @@ -133,7 +133,7 @@ module M_inc_some_tree__qyi12127997673864742005__take_some [#"inc_some_tree.rs" let%span sinc_some_tree6 = "inc_some_tree.rs" 31 15 31 19 let%span sinc_some_tree7 = "inc_some_tree.rs" 34 8 40 9 let%span sinc_some_tree8 = "inc_some_tree.rs" 23 12 26 13 - let%span smodel9 = "../../../../creusot-contracts/src/model.rs" 110 8 110 22 + let%span smodel9 = "../../../../creusot-contracts/src/model.rs" 72 8 72 22 let%span sresolve10 = "../../../../creusot-contracts/src/resolve.rs" 54 20 54 34 use prelude.prelude.UInt32 @@ -335,7 +335,7 @@ module M_inc_some_tree__inc_some_tree [#"inc_some_tree.rs" 83 0 83 41] let%span sinc_some_tree4 = "inc_some_tree.rs" 59 14 59 64 let%span sinc_some_tree5 = "inc_some_tree.rs" 60 14 60 35 let%span sinc_some_tree6 = "inc_some_tree.rs" 23 12 26 13 - let%span smodel7 = "../../../../creusot-contracts/src/model.rs" 110 8 110 22 + let%span smodel7 = "../../../../creusot-contracts/src/model.rs" 72 8 72 22 let%span sresolve8 = "../../../../creusot-contracts/src/resolve.rs" 54 20 54 34 use prelude.prelude.UInt32 diff --git a/creusot/tests/should_succeed/selection_sort_generic.coma b/creusot/tests/should_succeed/selection_sort_generic.coma index 3a397dfc7..af7f77f40 100644 --- a/creusot/tests/should_succeed/selection_sort_generic.coma +++ b/creusot/tests/should_succeed/selection_sort_generic.coma @@ -21,10 +21,10 @@ module M_selection_sort_generic__selection_sort [#"selection_sort_generic.rs" 30 let%span sselection_sort_generic19 = "selection_sort_generic.rs" 29 10 29 34 let%span svec20 = "../../../creusot-contracts/src/std/vec.rs" 83 26 83 48 let%span siter21 = "../../../creusot-contracts/src/std/iter.rs" 97 0 205 1 - let%span smodel22 = "../../../creusot-contracts/src/model.rs" 101 8 101 28 + let%span smodel22 = "../../../creusot-contracts/src/model.rs" 63 8 63 28 let%span sselection_sort_generic23 = "selection_sort_generic.rs" 25 16 25 105 let%span sselection_sort_generic24 = "selection_sort_generic.rs" 12 8 12 72 - let%span smodel25 = "../../../creusot-contracts/src/model.rs" 110 8 110 22 + let%span smodel25 = "../../../creusot-contracts/src/model.rs" 72 8 72 22 let%span ssnapshot26 = "../../../creusot-contracts/src/snapshot.rs" 52 20 52 39 let%span sseq27 = "../../../creusot-contracts/src/logic/seq.rs" 316 8 316 41 let%span srange28 = "../../../creusot-contracts/src/std/iter/range.rs" 22 12 26 70 @@ -41,7 +41,7 @@ module M_selection_sort_generic__selection_sort [#"selection_sort_generic.rs" 30 let%span svec39 = "../../../creusot-contracts/src/std/vec.rs" 30 14 31 51 let%span sselection_sort_generic40 = "selection_sort_generic.rs" 19 8 19 35 let%span svec41 = "../../../creusot-contracts/src/std/vec.rs" 18 14 18 41 - let%span smodel42 = "../../../creusot-contracts/src/model.rs" 92 8 92 22 + let%span smodel42 = "../../../creusot-contracts/src/model.rs" 54 8 54 22 let%span siter43 = "../../../creusot-contracts/src/std/iter.rs" 82 20 82 24 let%span siter44 = "../../../creusot-contracts/src/std/iter.rs" 88 8 88 19 let%span srange45 = "../../../creusot-contracts/src/std/iter/range.rs" 32 14 32 45 @@ -66,7 +66,7 @@ module M_selection_sort_generic__selection_sort [#"selection_sort_generic.rs" 30 let%span sord64 = "../../../creusot-contracts/src/logic/ord.rs" 95 14 95 59 let%span sslice65 = "../../../creusot-contracts/src/std/slice.rs" 122 20 122 37 let%span sslice66 = "../../../creusot-contracts/src/std/slice.rs" 129 20 129 37 - let%span smodel67 = "../../../creusot-contracts/src/model.rs" 83 8 83 28 + let%span smodel67 = "../../../creusot-contracts/src/model.rs" 45 8 45 28 let%span sslice68 = "../../../creusot-contracts/src/std/slice.rs" 28 14 28 41 let%span sslice69 = "../../../creusot-contracts/src/std/slice.rs" 29 14 29 42 let%span sindex70 = "../../../creusot-contracts/src/logic/ops/index.rs" 27 8 27 31 diff --git a/creusot/tests/should_succeed/slices/01.coma b/creusot/tests/should_succeed/slices/01.coma index cc2a4f000..233188549 100644 --- a/creusot/tests/should_succeed/slices/01.coma +++ b/creusot/tests/should_succeed/slices/01.coma @@ -2,7 +2,7 @@ module M_01__index_slice [#"01.rs" 6 0 6 36] let%span s010 = "01.rs" 7 6 7 8 let%span s011 = "01.rs" 7 4 7 9 let%span s012 = "01.rs" 5 11 5 24 - let%span smodel3 = "../../../../creusot-contracts/src/model.rs" 92 8 92 22 + let%span smodel3 = "../../../../creusot-contracts/src/model.rs" 54 8 54 22 let%span sslice4 = "../../../../creusot-contracts/src/std/slice.rs" 28 14 28 41 let%span sslice5 = "../../../../creusot-contracts/src/std/slice.rs" 29 14 29 42 @@ -64,7 +64,7 @@ module M_01__index_mut_slice [#"01.rs" 12 0 12 37] let%span s012 = "01.rs" 13 11 13 12 let%span s013 = "01.rs" 10 11 10 24 let%span s014 = "01.rs" 11 10 11 23 - let%span smodel5 = "../../../../creusot-contracts/src/model.rs" 110 8 110 22 + let%span smodel5 = "../../../../creusot-contracts/src/model.rs" 72 8 72 22 let%span sindex6 = "../../../../creusot-contracts/src/logic/ops/index.rs" 49 8 49 31 let%span sresolve7 = "../../../../creusot-contracts/src/resolve.rs" 54 20 54 34 let%span sslice8 = "../../../../creusot-contracts/src/std/slice.rs" 28 14 28 41 @@ -152,7 +152,7 @@ module M_01__slice_first [#"01.rs" 20 0 20 44] let%span s015 = "01.rs" 16 10 19 1 let%span sslice6 = "../../../../creusot-contracts/src/std/slice.rs" 245 0 354 1 let%span sindex7 = "../../../../creusot-contracts/src/logic/ops/index.rs" 49 8 49 31 - let%span smodel8 = "../../../../creusot-contracts/src/model.rs" 92 8 92 22 + let%span smodel8 = "../../../../creusot-contracts/src/model.rs" 54 8 54 22 let%span sslice9 = "../../../../creusot-contracts/src/std/slice.rs" 28 14 28 41 let%span sslice10 = "../../../../creusot-contracts/src/std/slice.rs" 29 14 29 42 let%span sinvariant11 = "../../../../creusot-contracts/src/invariant.rs" 24 8 24 18 diff --git a/creusot/tests/should_succeed/slices/02_std.coma b/creusot/tests/should_succeed/slices/02_std.coma index 4a8aa29e9..f67e340ac 100644 --- a/creusot/tests/should_succeed/slices/02_std.coma +++ b/creusot/tests/should_succeed/slices/02_std.coma @@ -10,9 +10,9 @@ module M_02_std__binary_search [#"02_std.rs" 8 0 8 40] let%span sslice8 = "../../../../creusot-contracts/src/std/slice.rs" 326 18 327 97 let%span sresult9 = "../../../../creusot-contracts/src/std/result.rs" 53 27 53 53 let%span sresult10 = "../../../../creusot-contracts/src/std/result.rs" 18 0 135 1 - let%span smodel11 = "../../../../creusot-contracts/src/model.rs" 92 8 92 22 + let%span smodel11 = "../../../../creusot-contracts/src/model.rs" 54 8 54 22 let%span sindex12 = "../../../../creusot-contracts/src/logic/ops/index.rs" 49 8 49 31 - let%span smodel13 = "../../../../creusot-contracts/src/model.rs" 83 8 83 28 + let%span smodel13 = "../../../../creusot-contracts/src/model.rs" 45 8 45 28 let%span sseq14 = "../../../../creusot-contracts/src/logic/seq.rs" 377 8 377 40 let%span sslice15 = "../../../../creusot-contracts/src/std/slice.rs" 40 14 40 44 let%span sslice16 = "../../../../creusot-contracts/src/std/slice.rs" 41 14 41 96 diff --git a/creusot/tests/should_succeed/sparse_array.coma b/creusot/tests/should_succeed/sparse_array.coma index b15308e89..d681cc3ba 100644 --- a/creusot/tests/should_succeed/sparse_array.coma +++ b/creusot/tests/should_succeed/sparse_array.coma @@ -217,7 +217,7 @@ module M_sparse_array__qyi912363311032332466__get [#"sparse_array.rs" 105 4 105 let%span ssparse_array4 = "sparse_array.rs" 101 14 104 5 let%span svec5 = "../../../creusot-contracts/src/std/vec.rs" 162 27 162 46 let%span svec6 = "../../../creusot-contracts/src/std/vec.rs" 163 26 163 54 - let%span smodel7 = "../../../creusot-contracts/src/model.rs" 92 8 92 22 + let%span smodel7 = "../../../creusot-contracts/src/model.rs" 54 8 54 22 let%span sslice8 = "../../../creusot-contracts/src/std/slice.rs" 122 20 122 37 let%span sslice9 = "../../../creusot-contracts/src/std/slice.rs" 129 20 129 37 let%span ssparse_array10 = "sparse_array.rs" 40 12 41 82 @@ -668,14 +668,14 @@ module M_sparse_array__qyi912363311032332466__set [#"sparse_array.rs" 129 4 129 let%span ssparse_array18 = "sparse_array.rs" 119 15 119 39 let%span ssparse_array19 = "sparse_array.rs" 120 14 120 28 let%span ssparse_array20 = "sparse_array.rs" 116 4 116 12 - let%span smodel21 = "../../../creusot-contracts/src/model.rs" 110 8 110 22 + let%span smodel21 = "../../../creusot-contracts/src/model.rs" 72 8 72 22 let%span ssparse_array22 = "sparse_array.rs" 40 12 41 82 let%span sslice23 = "../../../creusot-contracts/src/std/slice.rs" 122 20 122 37 let%span sslice24 = "../../../creusot-contracts/src/std/slice.rs" 129 20 129 37 let%span svec25 = "../../../creusot-contracts/src/std/vec.rs" 18 14 18 41 let%span sslice26 = "../../../creusot-contracts/src/std/slice.rs" 136 20 136 94 let%span sresolve27 = "../../../creusot-contracts/src/resolve.rs" 54 20 54 34 - let%span smodel28 = "../../../creusot-contracts/src/model.rs" 92 8 92 22 + let%span smodel28 = "../../../creusot-contracts/src/model.rs" 54 8 54 22 let%span ssparse_array29 = "sparse_array.rs" 89 20 90 52 let%span sindex30 = "../../../creusot-contracts/src/logic/ops/index.rs" 27 8 27 31 let%span svec31 = "../../../creusot-contracts/src/std/vec.rs" 65 20 65 41 @@ -1351,9 +1351,9 @@ module M_sparse_array__f [#"sparse_array.rs" 157 0 157 10] let%span ssparse_array35 = "sparse_array.rs" 126 14 126 43 let%span ssparse_array36 = "sparse_array.rs" 127 14 127 93 let%span ssparse_array37 = "sparse_array.rs" 128 14 128 37 - let%span smodel38 = "../../../creusot-contracts/src/model.rs" 92 8 92 22 + let%span smodel38 = "../../../creusot-contracts/src/model.rs" 54 8 54 22 let%span ssparse_array39 = "sparse_array.rs" 40 12 41 82 - let%span smodel40 = "../../../creusot-contracts/src/model.rs" 110 8 110 22 + let%span smodel40 = "../../../creusot-contracts/src/model.rs" 72 8 72 22 let%span ssparse_array41 = "sparse_array.rs" 89 20 90 52 let%span sindex42 = "../../../creusot-contracts/src/logic/ops/index.rs" 27 8 27 31 let%span ssparse_array43 = "sparse_array.rs" 68 12 76 17 diff --git a/creusot/tests/should_succeed/syntax/05_pearlite.coma b/creusot/tests/should_succeed/syntax/05_pearlite.coma index eec1cbdbe..5d5ca1498 100644 --- a/creusot/tests/should_succeed/syntax/05_pearlite.coma +++ b/creusot/tests/should_succeed/syntax/05_pearlite.coma @@ -1,7 +1,7 @@ module M_05_pearlite__has_len_3 [#"05_pearlite.rs" 11 0 11 35] let%span s05_pearlite0 = "05_pearlite.rs" 10 11 10 24 let%span s05_pearlite1 = "05_pearlite.rs" 12 16 12 29 - let%span smodel2 = "../../../../creusot-contracts/src/model.rs" 92 8 92 22 + let%span smodel2 = "../../../../creusot-contracts/src/model.rs" 54 8 54 22 let%span sslice3 = "../../../../creusot-contracts/src/std/slice.rs" 28 14 28 41 let%span sslice4 = "../../../../creusot-contracts/src/std/slice.rs" 29 14 29 42 diff --git a/creusot/tests/should_succeed/syntax/12_ghost_code.coma b/creusot/tests/should_succeed/syntax/12_ghost_code.coma index 74dc30172..e7460900d 100644 --- a/creusot/tests/should_succeed/syntax/12_ghost_code.coma +++ b/creusot/tests/should_succeed/syntax/12_ghost_code.coma @@ -182,8 +182,8 @@ module M_12_ghost_code__ghost_check [#"12_ghost_code.rs" 35 0 35 20] let%span svec7 = "../../../../creusot-contracts/src/std/vec.rs" 87 26 87 56 let%span svec8 = "../../../../creusot-contracts/src/std/vec.rs" 83 26 83 48 let%span svec9 = "../../../../creusot-contracts/src/std/vec.rs" 18 14 18 41 - let%span smodel10 = "../../../../creusot-contracts/src/model.rs" 110 8 110 22 - let%span smodel11 = "../../../../creusot-contracts/src/model.rs" 92 8 92 22 + let%span smodel10 = "../../../../creusot-contracts/src/model.rs" 72 8 72 22 + let%span smodel11 = "../../../../creusot-contracts/src/model.rs" 54 8 54 22 use prelude.prelude.Opaque @@ -299,7 +299,7 @@ module M_12_ghost_code__takes_struct [#"12_ghost_code.rs" 52 0 52 36] let%span s12_ghost_code0 = "12_ghost_code.rs" 53 10 53 27 let%span s12_ghost_code1 = "12_ghost_code.rs" 51 11 51 20 let%span ssnapshot2 = "../../../../creusot-contracts/src/snapshot.rs" 52 20 52 39 - let%span smodel3 = "../../../../creusot-contracts/src/model.rs" 92 8 92 22 + let%span smodel3 = "../../../../creusot-contracts/src/model.rs" 54 8 54 22 use prelude.prelude.UInt32 diff --git a/creusot/tests/should_succeed/syntax/derive_macros/mixed.coma b/creusot/tests/should_succeed/syntax/derive_macros/mixed.coma index 3e35b3659..cbce85665 100644 --- a/creusot/tests/should_succeed/syntax/derive_macros/mixed.coma +++ b/creusot/tests/should_succeed/syntax/derive_macros/mixed.coma @@ -86,7 +86,7 @@ module M_mixed__qyi2064882709679455996__eq [#"mixed.rs" 8 16 8 25] (* as creusot_contracts::PartialEq> *) let%span smixed0 = "mixed.rs" 28 16 28 25 let%span scmp1 = "../../../../../creusot-contracts/src/std/cmp.rs" 11 26 11 75 - let%span smodel2 = "../../../../../creusot-contracts/src/model.rs" 83 8 83 28 + let%span smodel2 = "../../../../../creusot-contracts/src/model.rs" 45 8 45 28 let%span smixed3 = "mixed.rs" 40 8 43 9 let%span sinvariant4 = "../../../../../creusot-contracts/src/invariant.rs" 24 8 24 18 @@ -656,7 +656,7 @@ module M_mixed__qyi6273949305112291917__clone__refines [#"mixed.rs" 28 9 28 14] end module M_mixed__qyi2064882709679455996__eq__refines [#"mixed.rs" 8 16 8 25] (* as creusot_contracts::PartialEq> *) let%span smixed0 = "mixed.rs" 8 16 8 25 - let%span smodel1 = "../../../../../creusot-contracts/src/model.rs" 83 8 83 28 + let%span smodel1 = "../../../../../creusot-contracts/src/model.rs" 45 8 45 28 let%span smixed2 = "mixed.rs" 24 8 24 66 let%span sinvariant3 = "../../../../../creusot-contracts/src/invariant.rs" 24 8 24 18 @@ -712,7 +712,7 @@ module M_mixed__qyi2064882709679455996__eq__refines [#"mixed.rs" 8 16 8 25] (* < end module M_mixed__qyi1479716791028959114__eq__refines [#"mixed.rs" 28 16 28 25] (* as creusot_contracts::PartialEq> *) let%span smixed0 = "mixed.rs" 28 16 28 25 - let%span smodel1 = "../../../../../creusot-contracts/src/model.rs" 83 8 83 28 + let%span smodel1 = "../../../../../creusot-contracts/src/model.rs" 45 8 45 28 let%span smixed2 = "mixed.rs" 40 8 43 9 let%span sinvariant3 = "../../../../../creusot-contracts/src/invariant.rs" 24 8 24 18 diff --git a/creusot/tests/should_succeed/take_first_mut.coma b/creusot/tests/should_succeed/take_first_mut.coma index 1a5bff38a..5ed5dcc91 100644 --- a/creusot/tests/should_succeed/take_first_mut.coma +++ b/creusot/tests/should_succeed/take_first_mut.coma @@ -10,7 +10,7 @@ module M_take_first_mut__take_first_mut [#"take_first_mut.rs" 14 0 14 74] let%span sslice8 = "../../../creusot-contracts/src/std/slice.rs" 29 14 29 42 let%span sseq9 = "../../../creusot-contracts/src/logic/seq.rs" 173 8 173 39 let%span sslice10 = "../../../creusot-contracts/src/std/slice.rs" 64 20 64 65 - let%span smodel11 = "../../../creusot-contracts/src/model.rs" 110 8 110 22 + let%span smodel11 = "../../../creusot-contracts/src/model.rs" 72 8 72 22 let%span sresolve12 = "../../../creusot-contracts/src/resolve.rs" 54 20 54 34 let%span sinvariant13 = "../../../creusot-contracts/src/invariant.rs" 34 20 34 44 let%span sslice14 = "../../../creusot-contracts/src/std/slice.rs" 18 20 18 30 diff --git a/creusot/tests/should_succeed/traits/16_impl_cloning.coma b/creusot/tests/should_succeed/traits/16_impl_cloning.coma index 1742955d5..f3fe85c9a 100644 --- a/creusot/tests/should_succeed/traits/16_impl_cloning.coma +++ b/creusot/tests/should_succeed/traits/16_impl_cloning.coma @@ -1,7 +1,7 @@ module M_16_impl_cloning__test [#"16_impl_cloning.rs" 16 0 16 30] let%span s16_impl_cloning0 = "16_impl_cloning.rs" 16 15 16 16 let%span s16_impl_cloning1 = "16_impl_cloning.rs" 15 10 15 21 - let%span smodel2 = "../../../../creusot-contracts/src/model.rs" 110 8 110 22 + let%span smodel2 = "../../../../creusot-contracts/src/model.rs" 72 8 72 22 let%span sresolve3 = "../../../../creusot-contracts/src/resolve.rs" 54 20 54 34 let%span sinvariant4 = "../../../../creusot-contracts/src/invariant.rs" 34 20 34 44 let%span svec5 = "../../../../creusot-contracts/src/std/vec.rs" 65 20 65 41 diff --git a/creusot/tests/should_succeed/vecdeque.coma b/creusot/tests/should_succeed/vecdeque.coma index 51af626ca..bcd072a87 100644 --- a/creusot/tests/should_succeed/vecdeque.coma +++ b/creusot/tests/should_succeed/vecdeque.coma @@ -29,10 +29,10 @@ module M_vecdeque__test_deque [#"vecdeque.rs" 5 0 5 19] let%span svecdeque27 = "vecdeque.rs" 24 37 24 38 let%span sdeque28 = "../../../creusot-contracts/src/std/deque.rs" 91 26 91 45 let%span sdeque29 = "../../../creusot-contracts/src/std/deque.rs" 13 14 13 41 - let%span smodel30 = "../../../creusot-contracts/src/model.rs" 92 8 92 22 - let%span smodel31 = "../../../creusot-contracts/src/model.rs" 110 8 110 22 + let%span smodel30 = "../../../creusot-contracts/src/model.rs" 54 8 54 22 + let%span smodel31 = "../../../creusot-contracts/src/model.rs" 72 8 72 22 let%span sseq32 = "../../../creusot-contracts/src/logic/seq.rs" 251 8 251 27 - let%span smodel33 = "../../../creusot-contracts/src/model.rs" 83 8 83 28 + let%span smodel33 = "../../../creusot-contracts/src/model.rs" 45 8 45 28 let%span soption34 = "../../../creusot-contracts/src/std/option.rs" 11 8 14 9 let%span snum35 = "../../../creusot-contracts/src/std/num.rs" 21 28 21 33 diff --git a/creusot/tests/should_succeed/vector/01.coma b/creusot/tests/should_succeed/vector/01.coma index 5086234a5..77075d062 100644 --- a/creusot/tests/should_succeed/vector/01.coma +++ b/creusot/tests/should_succeed/vector/01.coma @@ -13,7 +13,7 @@ module M_01__all_zero [#"01.rs" 7 0 7 33] let%span svec11 = "../../../../creusot-contracts/src/std/vec.rs" 83 26 83 48 let%span siter12 = "../../../../creusot-contracts/src/std/iter.rs" 97 0 205 1 let%span sindex13 = "../../../../creusot-contracts/src/logic/ops/index.rs" 27 8 27 31 - let%span smodel14 = "../../../../creusot-contracts/src/model.rs" 110 8 110 22 + let%span smodel14 = "../../../../creusot-contracts/src/model.rs" 72 8 72 22 let%span ssnapshot15 = "../../../../creusot-contracts/src/snapshot.rs" 52 20 52 39 let%span srange16 = "../../../../creusot-contracts/src/std/iter/range.rs" 22 12 26 70 let%span siter17 = "../../../../creusot-contracts/src/std/iter.rs" 103 26 106 17 @@ -23,7 +23,7 @@ module M_01__all_zero [#"01.rs" 7 0 7 33] let%span svec21 = "../../../../creusot-contracts/src/std/vec.rs" 155 26 155 62 let%span svec22 = "../../../../creusot-contracts/src/std/vec.rs" 156 26 156 55 let%span svec23 = "../../../../creusot-contracts/src/std/vec.rs" 18 14 18 41 - let%span smodel24 = "../../../../creusot-contracts/src/model.rs" 92 8 92 22 + let%span smodel24 = "../../../../creusot-contracts/src/model.rs" 54 8 54 22 let%span siter25 = "../../../../creusot-contracts/src/std/iter.rs" 82 20 82 24 let%span siter26 = "../../../../creusot-contracts/src/std/iter.rs" 88 8 88 19 let%span srange27 = "../../../../creusot-contracts/src/std/iter/range.rs" 32 14 32 45 diff --git a/creusot/tests/should_succeed/vector/02_gnome.coma b/creusot/tests/should_succeed/vector/02_gnome.coma index 802ea019f..e7cae48fe 100644 --- a/creusot/tests/should_succeed/vector/02_gnome.coma +++ b/creusot/tests/should_succeed/vector/02_gnome.coma @@ -11,10 +11,10 @@ module M_02_gnome__gnome_sort [#"02_gnome.rs" 22 0 24 29] let%span s02_gnome9 = "02_gnome.rs" 22 38 22 39 let%span s02_gnome10 = "02_gnome.rs" 20 10 20 35 let%span s02_gnome11 = "02_gnome.rs" 21 10 21 34 - let%span smodel12 = "../../../../creusot-contracts/src/model.rs" 110 8 110 22 + let%span smodel12 = "../../../../creusot-contracts/src/model.rs" 72 8 72 22 let%span ssnapshot13 = "../../../../creusot-contracts/src/snapshot.rs" 52 20 52 39 let%span sseq14 = "../../../../creusot-contracts/src/logic/seq.rs" 316 8 316 41 - let%span smodel15 = "../../../../creusot-contracts/src/model.rs" 101 8 101 28 + let%span smodel15 = "../../../../creusot-contracts/src/model.rs" 63 8 63 28 let%span s02_gnome16 = "02_gnome.rs" 11 8 11 74 let%span svec17 = "../../../../creusot-contracts/src/std/vec.rs" 83 26 83 48 let%span svec18 = "../../../../creusot-contracts/src/std/vec.rs" 162 27 162 46 @@ -29,10 +29,10 @@ module M_02_gnome__gnome_sort [#"02_gnome.rs" 22 0 24 29] let%span svec27 = "../../../../creusot-contracts/src/std/vec.rs" 30 14 31 51 let%span s02_gnome28 = "02_gnome.rs" 17 4 17 31 let%span svec29 = "../../../../creusot-contracts/src/std/vec.rs" 18 14 18 41 - let%span smodel30 = "../../../../creusot-contracts/src/model.rs" 92 8 92 22 + let%span smodel30 = "../../../../creusot-contracts/src/model.rs" 54 8 54 22 let%span sslice31 = "../../../../creusot-contracts/src/std/slice.rs" 122 20 122 37 let%span sslice32 = "../../../../creusot-contracts/src/std/slice.rs" 129 20 129 37 - let%span smodel33 = "../../../../creusot-contracts/src/model.rs" 83 8 83 28 + let%span smodel33 = "../../../../creusot-contracts/src/model.rs" 45 8 45 28 let%span sslice34 = "../../../../creusot-contracts/src/std/slice.rs" 28 14 28 41 let%span sslice35 = "../../../../creusot-contracts/src/std/slice.rs" 29 14 29 42 let%span sresolve36 = "../../../../creusot-contracts/src/resolve.rs" 54 20 54 34 diff --git a/creusot/tests/should_succeed/vector/03_knuth_shuffle.coma b/creusot/tests/should_succeed/vector/03_knuth_shuffle.coma index 3017bc95e..167d7400a 100644 --- a/creusot/tests/should_succeed/vector/03_knuth_shuffle.coma +++ b/creusot/tests/should_succeed/vector/03_knuth_shuffle.coma @@ -12,7 +12,7 @@ module M_03_knuth_shuffle__knuth_shuffle [#"03_knuth_shuffle.rs" 13 0 13 39] let%span s03_knuth_shuffle10 = "03_knuth_shuffle.rs" 12 10 12 34 let%span svec11 = "../../../../creusot-contracts/src/std/vec.rs" 83 26 83 48 let%span siter12 = "../../../../creusot-contracts/src/std/iter.rs" 97 0 205 1 - let%span smodel13 = "../../../../creusot-contracts/src/model.rs" 110 8 110 22 + let%span smodel13 = "../../../../creusot-contracts/src/model.rs" 72 8 72 22 let%span ssnapshot14 = "../../../../creusot-contracts/src/snapshot.rs" 52 20 52 39 let%span sseq15 = "../../../../creusot-contracts/src/logic/seq.rs" 316 8 316 41 let%span srange16 = "../../../../creusot-contracts/src/std/iter/range.rs" 22 12 26 70 @@ -25,7 +25,7 @@ module M_03_knuth_shuffle__knuth_shuffle [#"03_knuth_shuffle.rs" 13 0 13 39] let%span sslice23 = "../../../../creusot-contracts/src/std/slice.rs" 258 19 258 35 let%span sslice24 = "../../../../creusot-contracts/src/std/slice.rs" 259 18 259 50 let%span svec25 = "../../../../creusot-contracts/src/std/vec.rs" 18 14 18 41 - let%span smodel26 = "../../../../creusot-contracts/src/model.rs" 92 8 92 22 + let%span smodel26 = "../../../../creusot-contracts/src/model.rs" 54 8 54 22 let%span siter27 = "../../../../creusot-contracts/src/std/iter.rs" 82 20 82 24 let%span siter28 = "../../../../creusot-contracts/src/std/iter.rs" 88 8 88 19 let%span srange29 = "../../../../creusot-contracts/src/std/iter/range.rs" 32 14 32 45 diff --git a/creusot/tests/should_succeed/vector/04_binary_search.coma b/creusot/tests/should_succeed/vector/04_binary_search.coma index b8b3fb858..4b22aed1a 100644 --- a/creusot/tests/should_succeed/vector/04_binary_search.coma +++ b/creusot/tests/should_succeed/vector/04_binary_search.coma @@ -15,7 +15,7 @@ module M_04_binary_search__binary_search [#"04_binary_search.rs" 26 0 26 71] let%span s04_binary_search13 = "04_binary_search.rs" 22 10 23 46 let%span s04_binary_search14 = "04_binary_search.rs" 24 10 25 63 let%span svec15 = "../../../../creusot-contracts/src/std/vec.rs" 83 26 83 48 - let%span smodel16 = "../../../../creusot-contracts/src/model.rs" 92 8 92 22 + let%span smodel16 = "../../../../creusot-contracts/src/model.rs" 54 8 54 22 let%span sindex17 = "../../../../creusot-contracts/src/logic/ops/index.rs" 27 8 27 31 let%span svec18 = "../../../../creusot-contracts/src/std/vec.rs" 162 27 162 46 let%span svec19 = "../../../../creusot-contracts/src/std/vec.rs" 163 26 163 54 diff --git a/creusot/tests/should_succeed/vector/05_binary_search_generic.coma b/creusot/tests/should_succeed/vector/05_binary_search_generic.coma index ab275ff98..cbb971d42 100644 --- a/creusot/tests/should_succeed/vector/05_binary_search_generic.coma +++ b/creusot/tests/should_succeed/vector/05_binary_search_generic.coma @@ -17,8 +17,8 @@ module M_05_binary_search_generic__binary_search [#"05_binary_search_generic.rs" let%span s05_binary_search_generic15 = "05_binary_search_generic.rs" 23 10 24 72 let%span s05_binary_search_generic16 = "05_binary_search_generic.rs" 25 10 26 90 let%span svec17 = "../../../../creusot-contracts/src/std/vec.rs" 83 26 83 48 - let%span smodel18 = "../../../../creusot-contracts/src/model.rs" 92 8 92 22 - let%span smodel19 = "../../../../creusot-contracts/src/model.rs" 83 8 83 28 + let%span smodel18 = "../../../../creusot-contracts/src/model.rs" 54 8 54 22 + let%span smodel19 = "../../../../creusot-contracts/src/model.rs" 45 8 45 28 let%span svec20 = "../../../../creusot-contracts/src/std/vec.rs" 162 27 162 46 let%span svec21 = "../../../../creusot-contracts/src/std/vec.rs" 163 26 163 54 let%span scmp22 = "../../../../creusot-contracts/src/std/cmp.rs" 51 26 51 76 diff --git a/creusot/tests/should_succeed/vector/06_knights_tour.coma b/creusot/tests/should_succeed/vector/06_knights_tour.coma index 83756e7c9..a18bdb655 100644 --- a/creusot/tests/should_succeed/vector/06_knights_tour.coma +++ b/creusot/tests/should_succeed/vector/06_knights_tour.coma @@ -514,7 +514,7 @@ module M_06_knights_tour__qyi4580598960913230815__available [#"06_knights_tour.r let%span svec7 = "../../../../creusot-contracts/src/std/vec.rs" 163 26 163 54 let%span s06_knights_tour8 = "06_knights_tour.rs" 32 12 34 93 let%span s06_knights_tour9 = "06_knights_tour.rs" 63 12 63 75 - let%span smodel10 = "../../../../creusot-contracts/src/model.rs" 92 8 92 22 + let%span smodel10 = "../../../../creusot-contracts/src/model.rs" 54 8 54 22 let%span sslice11 = "../../../../creusot-contracts/src/std/slice.rs" 122 20 122 37 let%span sslice12 = "../../../../creusot-contracts/src/std/slice.rs" 129 20 129 37 let%span svec13 = "../../../../creusot-contracts/src/std/vec.rs" 18 14 18 41 @@ -754,7 +754,7 @@ module M_06_knights_tour__qyi4580598960913230815__count_degree [#"06_knights_tou let%span svec34 = "../../../../creusot-contracts/src/std/vec.rs" 273 4 273 10 let%span svec35 = "../../../../creusot-contracts/src/std/vec.rs" 257 20 257 57 let%span sresolve36 = "../../../../creusot-contracts/src/resolve.rs" 54 20 54 34 - let%span smodel37 = "../../../../creusot-contracts/src/model.rs" 110 8 110 22 + let%span smodel37 = "../../../../creusot-contracts/src/model.rs" 72 8 72 22 use prelude.prelude.UIntSize @@ -1107,7 +1107,7 @@ module M_06_knights_tour__qyi4580598960913230815__set [#"06_knights_tour.rs" 87 let%span svec8 = "../../../../creusot-contracts/src/std/vec.rs" 156 26 156 55 let%span s06_knights_tour9 = "06_knights_tour.rs" 32 12 34 93 let%span s06_knights_tour10 = "06_knights_tour.rs" 63 12 63 75 - let%span smodel11 = "../../../../creusot-contracts/src/model.rs" 110 8 110 22 + let%span smodel11 = "../../../../creusot-contracts/src/model.rs" 72 8 72 22 let%span sslice12 = "../../../../creusot-contracts/src/std/slice.rs" 122 20 122 37 let%span sslice13 = "../../../../creusot-contracts/src/std/slice.rs" 129 20 129 37 let%span svec14 = "../../../../creusot-contracts/src/std/vec.rs" 18 14 18 41 @@ -1338,7 +1338,7 @@ module M_06_knights_tour__min [#"06_knights_tour.rs" 110 0 110 58] let%span s06_knights_tour4 = "06_knights_tour.rs" 114 4 114 7 let%span s06_knights_tour5 = "06_knights_tour.rs" 108 10 109 60 let%span siter6 = "../../../../creusot-contracts/src/std/iter.rs" 97 0 205 1 - let%span smodel7 = "../../../../creusot-contracts/src/model.rs" 92 8 92 22 + let%span smodel7 = "../../../../creusot-contracts/src/model.rs" 54 8 54 22 let%span sindex8 = "../../../../creusot-contracts/src/logic/ops/index.rs" 27 8 27 31 let%span sslice9 = "../../../../creusot-contracts/src/std/slice.rs" 405 12 405 66 let%span siter10 = "../../../../creusot-contracts/src/std/iter.rs" 103 26 106 17 @@ -1356,7 +1356,7 @@ module M_06_knights_tour__min [#"06_knights_tour.rs" 110 0 110 58] let%span sslice22 = "../../../../creusot-contracts/src/std/slice.rs" 398 20 398 61 let%span sresolve23 = "../../../../creusot-contracts/src/resolve.rs" 54 20 54 34 let%span sindex24 = "../../../../creusot-contracts/src/logic/ops/index.rs" 49 8 49 31 - let%span smodel25 = "../../../../creusot-contracts/src/model.rs" 110 8 110 22 + let%span smodel25 = "../../../../creusot-contracts/src/model.rs" 72 8 72 22 let%span sslice26 = "../../../../creusot-contracts/src/std/slice.rs" 28 14 28 41 let%span sslice27 = "../../../../creusot-contracts/src/std/slice.rs" 29 14 29 42 @@ -1718,8 +1718,8 @@ module M_06_knights_tour__knights_tour [#"06_knights_tour.rs" 135 0 135 69] let%span svec69 = "../../../../creusot-contracts/src/std/vec.rs" 277 14 277 42 let%span svec70 = "../../../../creusot-contracts/src/std/vec.rs" 273 4 273 10 let%span svec71 = "../../../../creusot-contracts/src/std/vec.rs" 257 20 257 57 - let%span smodel72 = "../../../../creusot-contracts/src/model.rs" 110 8 110 22 - let%span smodel73 = "../../../../creusot-contracts/src/model.rs" 92 8 92 22 + let%span smodel72 = "../../../../creusot-contracts/src/model.rs" 72 8 72 22 + let%span smodel73 = "../../../../creusot-contracts/src/model.rs" 54 8 54 22 use prelude.prelude.UIntSize diff --git a/creusot/tests/should_succeed/vector/07_read_write.coma b/creusot/tests/should_succeed/vector/07_read_write.coma index 025e575c5..2e2bb0423 100644 --- a/creusot/tests/should_succeed/vector/07_read_write.coma +++ b/creusot/tests/should_succeed/vector/07_read_write.coma @@ -11,14 +11,14 @@ module M_07_read_write__read_write [#"07_read_write.rs" 6 0 6 75] let%span svec9 = "../../../../creusot-contracts/src/std/vec.rs" 162 27 162 46 let%span svec10 = "../../../../creusot-contracts/src/std/vec.rs" 163 26 163 54 let%span scmp11 = "../../../../creusot-contracts/src/std/cmp.rs" 11 26 11 75 - let%span smodel12 = "../../../../creusot-contracts/src/model.rs" 110 8 110 22 + let%span smodel12 = "../../../../creusot-contracts/src/model.rs" 72 8 72 22 let%span sslice13 = "../../../../creusot-contracts/src/std/slice.rs" 122 20 122 37 let%span sslice14 = "../../../../creusot-contracts/src/std/slice.rs" 129 20 129 37 let%span svec15 = "../../../../creusot-contracts/src/std/vec.rs" 18 14 18 41 let%span sslice16 = "../../../../creusot-contracts/src/std/slice.rs" 136 20 136 94 let%span sresolve17 = "../../../../creusot-contracts/src/resolve.rs" 54 20 54 34 - let%span smodel18 = "../../../../creusot-contracts/src/model.rs" 92 8 92 22 - let%span smodel19 = "../../../../creusot-contracts/src/model.rs" 83 8 83 28 + let%span smodel18 = "../../../../creusot-contracts/src/model.rs" 54 8 54 22 + let%span smodel19 = "../../../../creusot-contracts/src/model.rs" 45 8 45 28 let%span svec20 = "../../../../creusot-contracts/src/std/vec.rs" 65 20 65 41 let%span sinvariant21 = "../../../../creusot-contracts/src/invariant.rs" 34 20 34 44 let%span sinvariant22 = "../../../../creusot-contracts/src/invariant.rs" 24 8 24 18 diff --git a/creusot/tests/should_succeed/vector/08_haystack.coma b/creusot/tests/should_succeed/vector/08_haystack.coma index c7126fd7a..019de5227 100644 --- a/creusot/tests/should_succeed/vector/08_haystack.coma +++ b/creusot/tests/should_succeed/vector/08_haystack.coma @@ -20,7 +20,7 @@ module M_08_haystack__search [#"08_haystack.rs" 21 0 21 60] let%span sops18 = "../../../../creusot-contracts/src/std/ops.rs" 220 26 220 49 let%span sops19 = "../../../../creusot-contracts/src/std/ops.rs" 221 26 221 91 let%span siter20 = "../../../../creusot-contracts/src/std/iter.rs" 97 0 205 1 - let%span smodel21 = "../../../../creusot-contracts/src/model.rs" 92 8 92 22 + let%span smodel21 = "../../../../creusot-contracts/src/model.rs" 54 8 54 22 let%span s08_haystack22 = "08_haystack.rs" 8 16 11 62 let%span srange23 = "../../../../creusot-contracts/src/std/iter/range.rs" 66 12 70 76 let%span siter24 = "../../../../creusot-contracts/src/std/iter.rs" 103 26 106 17 diff --git a/creusot/tests/should_succeed/vector/09_capacity.coma b/creusot/tests/should_succeed/vector/09_capacity.coma index 33fb8df27..f6f29d70f 100644 --- a/creusot/tests/should_succeed/vector/09_capacity.coma +++ b/creusot/tests/should_succeed/vector/09_capacity.coma @@ -10,7 +10,7 @@ module M_09_capacity__change_capacity [#"09_capacity.rs" 6 0 6 41] let%span svec8 = "../../../../creusot-contracts/src/std/vec.rs" 126 26 126 43 let%span svec9 = "../../../../creusot-contracts/src/std/vec.rs" 130 26 130 43 let%span svec10 = "../../../../creusot-contracts/src/std/vec.rs" 18 14 18 41 - let%span smodel11 = "../../../../creusot-contracts/src/model.rs" 110 8 110 22 + let%span smodel11 = "../../../../creusot-contracts/src/model.rs" 72 8 72 22 let%span sindex12 = "../../../../creusot-contracts/src/logic/ops/index.rs" 27 8 27 31 let%span sresolve13 = "../../../../creusot-contracts/src/resolve.rs" 54 20 54 34 let%span svec14 = "../../../../creusot-contracts/src/std/vec.rs" 65 20 65 41