diff --git a/charon-pin b/charon-pin
index 6e543363e..0ba22660e 100644
--- a/charon-pin
+++ b/charon-pin
@@ -1,2 +1,2 @@
 # This is the commit from https://github.com/AeneasVerif/charon that should be used with this version of aeneas.
-6c6b93beebaf143d9a6d3ffd0f7fc0ffbf57efe4
+051a0322504d97dea97f013be0c70a6b48811bf0
diff --git a/flake.lock b/flake.lock
index b2277989b..7c86c5881 100644
--- a/flake.lock
+++ b/flake.lock
@@ -9,11 +9,11 @@
         "rust-overlay": "rust-overlay"
       },
       "locked": {
-        "lastModified": 1768082582,
-        "narHash": "sha256-9H8ggZm5I+A4anR8jQiomkDWCo3WTqIex6ylKNhyvnw=",
+        "lastModified": 1768319516,
+        "narHash": "sha256-IXeYc6gPHx2rmtitF00ZLVsMtlNpiufr4Ts6xua2QfI=",
         "owner": "aeneasverif",
         "repo": "charon",
-        "rev": "6c6b93beebaf143d9a6d3ffd0f7fc0ffbf57efe4",
+        "rev": "051a0322504d97dea97f013be0c70a6b48811bf0",
         "type": "github"
       },
       "original": {
diff --git a/tests/lean/Loops.lean b/tests/lean/Loops.lean
index 593d6380d..814ef2860 100644
--- a/tests/lean/Loops.lean
+++ b/tests/lean/Loops.lean
@@ -299,7 +299,7 @@ def list_nth_shared_with_id
   list_nth_shared_with_id_loop i ls1
 
 /- [loops::list_nth_mut_pair]: loop 0:
-   Source: 'tests/src/loops.rs', lines 199:8-199:24 -/
+   Source: 'tests/src/loops.rs', lines 198:4-214:1 -/
 def list_nth_mut_pair_loop
   {T : Type} (ls0 : List T) (ls1 : List T) (i : Std.U32) :
   Result (T × T × (T → List T) × (T → List T))
@@ -332,7 +332,7 @@ def list_nth_mut_pair
   ok ((t, t1), back, back1)
 
 /- [loops::list_nth_shared_pair]: loop 0:
-   Source: 'tests/src/loops.rs', lines 223:8-223:24 -/
+   Source: 'tests/src/loops.rs', lines 222:4-238:1 -/
 def list_nth_shared_pair_loop
   {T : Type} (ls0 : List T) (ls1 : List T) (i : Std.U32) :
   Result (T × T)