From 082661f0d9d1bb1196ef8e1d57b3f2b4922b3d8e Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Tue, 18 Jun 2024 12:12:05 +0200
Subject: Bump charon

---
 tests/lean/Arrays.lean | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'tests/lean/Arrays.lean')

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
-- 
cgit v1.2.3

