Merge pull request #251 from Nadrieril/bump-charon2

4 files changed, 15 insertions, 15 deletions

diff --git a/tests/lean/Arrays.lean b/tests/lean/Arrays.lean
index bb97d5c4..bdaa7380 100644
--- a/tests/lean/Arrays.lean
+++ b/tests/lean/Arrays.lean
@@ -349,7 +349,7 @@ def non_copyable_array : Result Unit :=
   take_array_t (Array.make AB 2#usize [ AB.A, AB.B ])
 
 /- [arrays::sum]: loop 0:
-   Source: 'tests/src/arrays.rs', lines 245:0-253:1 -/
+   Source: 'tests/src/arrays.rs', lines 247:4-253:1 -/
 divergent def sum_loop (s : Slice U32) (sum1 : U32) (i : Usize) : Result U32 :=
   let i1 := Slice.len U32 s
   if i < i1
@@ -367,7 +367,7 @@ def sum (s : Slice U32) : Result U32 :=
   sum_loop s 0#u32 0#usize
 
 /- [arrays::sum2]: loop 0:
-   Source: 'tests/src/arrays.rs', lines 255:0-264:1 -/
+   Source: 'tests/src/arrays.rs', lines 258:4-264:1 -/
 divergent def sum2_loop
   (s : Slice U32) (s2 : Slice U32) (sum1 : U32) (i : Usize) : Result U32 :=
   let i1 := Slice.len U32 s
@@ -464,7 +464,7 @@ def ite : Result Unit :=
   Result.ok ()
 
 /- [arrays::zero_slice]: loop 0:
-   Source: 'tests/src/arrays.rs', lines 306:0-313:1 -/
+   Source: 'tests/src/arrays.rs', lines 308:4-313:1 -/
 divergent def zero_slice_loop
   (a : Slice U8) (i : Usize) (len : Usize) : Result (Slice U8) :=
   if i < len
@@ -483,7 +483,7 @@ def zero_slice (a : Slice U8) : Result (Slice U8) :=
   zero_slice_loop a 0#usize len
 
 /- [arrays::iter_mut_slice]: loop 0:
-   Source: 'tests/src/arrays.rs', lines 315:0-321:1 -/
+   Source: 'tests/src/arrays.rs', lines 317:4-321:1 -/
 divergent def iter_mut_slice_loop (len : Usize) (i : Usize) : Result Unit :=
   if i < len
   then do
@@ -500,7 +500,7 @@ def iter_mut_slice (a : Slice U8) : Result (Slice U8) :=
   Result.ok a
 
 /- [arrays::sum_mut_slice]: loop 0:
-   Source: 'tests/src/arrays.rs', lines 323:0-331:1 -/
+   Source: 'tests/src/arrays.rs', lines 325:4-331:1 -/
 divergent def sum_mut_slice_loop
   (a : Slice U32) (i : Usize) (s : U32) : Result U32 :=
   let i1 := Slice.len U32 a
diff --git a/tests/lean/Betree/Funs.lean b/tests/lean/Betree/Funs.lean
index 4592e91c..dd8dfb05 100644
--- a/tests/lean/Betree/Funs.lean
+++ b/tests/lean/Betree/Funs.lean
@@ -83,7 +83,7 @@ def betree.upsert_update
       else Result.ok 0#u64
 
 /- [betree::betree::{betree::betree::List<T>#1}::len]: loop 0:
-   Source: 'src/betree.rs', lines 276:4-284:5 -/
+   Source: 'src/betree.rs', lines 278:8-284:5 -/
 divergent def betree.List.len_loop
   (T : Type) (self : betree.List T) (len : U64) : Result U64 :=
   match self with
@@ -99,7 +99,7 @@ def betree.List.len (T : Type) (self : betree.List T) : Result U64 :=
   betree.List.len_loop T self 0#u64
 
 /- [betree::betree::{betree::betree::List<T>#1}::reverse]: loop 0:
-   Source: 'src/betree.rs', lines 304:4-312:5 -/
+   Source: 'src/betree.rs', lines 305:8-312:5 -/
 divergent def betree.List.reverse_loop
   (T : Type) (self : betree.List T) (out : betree.List T) :
   Result (betree.List T)
@@ -116,7 +116,7 @@ def betree.List.reverse
   betree.List.reverse_loop T self betree.List.Nil
 
 /- [betree::betree::{betree::betree::List<T>#1}::split_at]: loop 0:
-   Source: 'src/betree.rs', lines 287:4-302:5 -/
+   Source: 'src/betree.rs', lines 289:8-302:5 -/
 divergent def betree.List.split_at_loop
   (T : Type) (n : U64) (beg : betree.List T) (self : betree.List T) :
   Result ((betree.List T) × (betree.List T))
@@ -174,7 +174,7 @@ def betree.ListPairU64T.head_has_key
   | betree.List.Nil => Result.ok false
 
 /- [betree::betree::{betree::betree::List<(u64, T)>#2}::partition_at_pivot]: loop 0:
-   Source: 'src/betree.rs', lines 355:4-370:5 -/
+   Source: 'src/betree.rs', lines 358:8-370:5 -/
 divergent def betree.ListPairU64T.partition_at_pivot_loop
   (T : Type) (pivot : U64) (beg : betree.List (U64 × T))
   (end1 : betree.List (U64 × T)) (self : betree.List (U64 × T)) :
diff --git a/tests/lean/Hashmap/Funs.lean b/tests/lean/Hashmap/Funs.lean
index 7972b715..76ec5041 100644
--- a/tests/lean/Hashmap/Funs.lean
+++ b/tests/lean/Hashmap/Funs.lean
@@ -63,7 +63,7 @@ def HashMap.new (T : Type) : Result (HashMap T) :=
   HashMap.new_with_capacity T 32#usize 4#usize 5#usize
 
 /- [hashmap::{hashmap::HashMap<T>}::clear]: loop 0:
-   Source: 'tests/src/hashmap.rs', lines 91:4-99:5 -/
+   Source: 'tests/src/hashmap.rs', lines 94:8-99:5 -/
 divergent def HashMap.clear_loop
   (T : Type) (slots : alloc.vec.Vec (AList T)) (i : Usize) :
   Result (alloc.vec.Vec (AList T))
diff --git a/tests/lean/Loops.lean b/tests/lean/Loops.lean
index e676336e..6435cabb 100644
--- a/tests/lean/Loops.lean
+++ b/tests/lean/Loops.lean
@@ -9,7 +9,7 @@ set_option linter.unusedVariables false
 namespace loops
 
 /- [loops::sum]: loop 0:
-   Source: 'tests/src/loops.rs', lines 8:0-18:1 -/
+   Source: 'tests/src/loops.rs', lines 10:4-18:1 -/
 divergent def sum_loop (max : U32) (i : U32) (s : U32) : Result U32 :=
   if i < max
   then do
@@ -24,7 +24,7 @@ def sum (max : U32) : Result U32 :=
   sum_loop max 0#u32 0#u32
 
 /- [loops::sum_with_mut_borrows]: loop 0:
-   Source: 'tests/src/loops.rs', lines 23:0-35:1 -/
+   Source: 'tests/src/loops.rs', lines 25:4-35:1 -/
 divergent def sum_with_mut_borrows_loop
   (max : U32) (i : U32) (s : U32) : Result U32 :=
   if i < max
@@ -41,7 +41,7 @@ def sum_with_mut_borrows (max : U32) : Result U32 :=
   sum_with_mut_borrows_loop max 0#u32 0#u32
 
 /- [loops::sum_with_shared_borrows]: loop 0:
-   Source: 'tests/src/loops.rs', lines 38:0-52:1 -/
+   Source: 'tests/src/loops.rs', lines 40:4-52:1 -/
 divergent def sum_with_shared_borrows_loop
   (max : U32) (i : U32) (s : U32) : Result U32 :=
   if i < max
@@ -58,7 +58,7 @@ def sum_with_shared_borrows (max : U32) : Result U32 :=
   sum_with_shared_borrows_loop max 0#u32 0#u32
 
 /- [loops::sum_array]: loop 0:
-   Source: 'tests/src/loops.rs', lines 54:0-62:1 -/
+   Source: 'tests/src/loops.rs', lines 56:4-62:1 -/
 divergent def sum_array_loop
   (N : Usize) (a : Array U32 N) (i : Usize) (s : U32) : Result U32 :=
   if i < N
@@ -76,7 +76,7 @@ def sum_array (N : Usize) (a : Array U32 N) : Result U32 :=
   sum_array_loop N a 0#usize 0#u32
 
 /- [loops::clear]: loop 0:
-   Source: 'tests/src/loops.rs', lines 66:0-72:1 -/
+   Source: 'tests/src/loops.rs', lines 67:4-72:1 -/
 divergent def clear_loop
   (v : alloc.vec.Vec U32) (i : Usize) : Result (alloc.vec.Vec U32) :=
   let i1 := alloc.vec.Vec.len U32 v