diff --git a/charon-pin b/charon-pin
index 2621304ec..237559d97 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.
-5c2ae3744ce702d07920d0f536a272aadd396ed9
+944e91f5fcbed9e6b923c26b12580bf5522f7aee
diff --git a/flake.lock b/flake.lock
index 73bd300d4..90e87cd27 100644
--- a/flake.lock
+++ b/flake.lock
@@ -9,11 +9,11 @@
         "rust-overlay": "rust-overlay"
       },
       "locked": {
-        "lastModified": 1719229989,
-        "narHash": "sha256-/Eb1xd65HQeZtO7R/XMXA0ibzig7mffOLNGITuG6rVQ=",
+        "lastModified": 1719241017,
+        "narHash": "sha256-D8l2NO6/2FPhBYDJ4I9v62lC79vWKv/MTrHKrHr41cE=",
         "owner": "aeneasverif",
         "repo": "charon",
-        "rev": "5c2ae3744ce702d07920d0f536a272aadd396ed9",
+        "rev": "944e91f5fcbed9e6b923c26b12580bf5522f7aee",
         "type": "github"
       },
       "original": {
@@ -266,21 +266,17 @@
     },
     "rust-overlay": {
       "inputs": {
-        "flake-utils": [
-          "charon",
-          "flake-utils"
-        ],
         "nixpkgs": [
           "charon",
           "nixpkgs"
         ]
       },
       "locked": {
-        "lastModified": 1701656211,
-        "narHash": "sha256-lfFXsLWH4hVbEKR6K+UcDiKxeS6Lz4FkC1DZ9LHqf9Y=",
+        "lastModified": 1719195554,
+        "narHash": "sha256-bFXHMjpYlEERexzXa1gLGJO/1l8dxaAtSNE56YALuTg=",
         "owner": "oxalica",
         "repo": "rust-overlay",
-        "rev": "47a276e820ae4ae1b8d98a503bf09d2ceb52dfd8",
+        "rev": "577ee84c69ba89894ac622d71a678a14d746b2f7",
         "type": "github"
       },
       "original": {
diff --git a/tests/coq/arrays/Arrays.v b/tests/coq/arrays/Arrays.v
index cd6a4b878..bdf8c168f 100644
--- a/tests/coq/arrays/Arrays.v
+++ b/tests/coq/arrays/Arrays.v
@@ -36,19 +36,19 @@ Definition array_to_mut_slice_
 (** [arrays::array_len]:
     Source: 'tests/src/arrays.rs', lines 28:0-28:40 *)
 Definition array_len (T : Type) (s : array T 32%usize) : result usize :=
-  s1 <- array_to_slice T 32%usize s; Ok (slice_len T s1)
+  s1 <- array_to_slice T 32%usize s; Ok (slice_len T true s1)
 .
 
 (** [arrays::shared_array_len]:
     Source: 'tests/src/arrays.rs', lines 32:0-32:48 *)
 Definition shared_array_len (T : Type) (s : array T 32%usize) : result usize :=
-  s1 <- array_to_slice T 32%usize s; Ok (slice_len T s1)
+  s1 <- array_to_slice T 32%usize s; Ok (slice_len T true s1)
 .
 
 (** [arrays::shared_slice_len]:
     Source: 'tests/src/arrays.rs', lines 36:0-36:44 *)
 Definition shared_slice_len (T : Type) (s : slice T) : result usize :=
-  Ok (slice_len T s)
+  Ok (slice_len T true s)
 .
 
 (** [arrays::index_array_shared]:
@@ -382,7 +382,7 @@ Fixpoint sum_loop
   match n with
   | O => Fail_ OutOfFuel
   | S n1 =>
-    let i1 := slice_len u32 s in
+    let i1 := slice_len u32 true s in
     if i s< i1
     then (
       i2 <- slice_index_usize u32 s i;
@@ -408,7 +408,7 @@ Fixpoint sum2_loop
   match n with
   | O => Fail_ OutOfFuel
   | S n1 =>
-    let i1 := slice_len u32 s in
+    let i1 := slice_len u32 true s in
     if i s< i1
     then (
       i2 <- slice_index_usize u32 s i;
@@ -424,8 +424,8 @@ Fixpoint sum2_loop
 (** [arrays::sum2]:
     Source: 'tests/src/arrays.rs', lines 255:0-255:41 *)
 Definition sum2 (n : nat) (s : slice u32) (s2 : slice u32) : result u32 :=
-  let i := slice_len u32 s in
-  let i1 := slice_len u32 s2 in
+  let i := slice_len u32 true s in
+  let i1 := slice_len u32 true s2 in
   if i s= i1 then sum2_loop n s s2 0%u32 0%usize else Fail_ Failure
 .
 
@@ -528,7 +528,7 @@ Fixpoint zero_slice_loop
 (** [arrays::zero_slice]:
     Source: 'tests/src/arrays.rs', lines 306:0-306:31 *)
 Definition zero_slice (n : nat) (a : slice u8) : result (slice u8) :=
-  let len := slice_len u8 a in zero_slice_loop n a 0%usize len
+  let len := slice_len u8 true a in zero_slice_loop n a 0%usize len
 .
 
 (** [arrays::iter_mut_slice]: loop 0:
@@ -547,7 +547,9 @@ Fixpoint iter_mut_slice_loop
 (** [arrays::iter_mut_slice]:
     Source: 'tests/src/arrays.rs', lines 315:0-315:35 *)
 Definition iter_mut_slice (n : nat) (a : slice u8) : result (slice u8) :=
-  let len := slice_len u8 a in _ <- iter_mut_slice_loop n len 0%usize; Ok a
+  let len := slice_len u8 true a in
+  _ <- iter_mut_slice_loop n len 0%usize;
+  Ok a
 .
 
 (** [arrays::sum_mut_slice]: loop 0:
@@ -557,7 +559,7 @@ Fixpoint sum_mut_slice_loop
   match n with
   | O => Fail_ OutOfFuel
   | S n1 =>
-    let i1 := slice_len u32 a in
+    let i1 := slice_len u32 true a in
     if i s< i1
     then (
       i2 <- slice_index_usize u32 a i;
diff --git a/tests/coq/betree/Betree_Funs.v b/tests/coq/betree/Betree_Funs.v
index bb9fe90e8..c4685cb0f 100644
--- a/tests/coq/betree/Betree_Funs.v
+++ b/tests/coq/betree/Betree_Funs.v
@@ -169,7 +169,8 @@ Definition betree_List_split_at
     Source: 'src/betree.rs', lines 315:4-315:34 *)
 Definition betree_List_push_front
   (T : Type) (self : betree_List_t T) (x : T) : result (betree_List_t T) :=
-  let (tl, _) := core_mem_replace (betree_List_t T) self Betree_List_Nil in
+  let (tl, _) := core_mem_replace (betree_List_t T) true self Betree_List_Nil
+    in
   Ok (Betree_List_Cons x tl)
 .
 
@@ -177,7 +178,8 @@ Definition betree_List_push_front
     Source: 'src/betree.rs', lines 322:4-322:32 *)
 Definition betree_List_pop_front
   (T : Type) (self : betree_List_t T) : result (T * (betree_List_t T)) :=
-  let (ls, _) := core_mem_replace (betree_List_t T) self Betree_List_Nil in
+  let (ls, _) := core_mem_replace (betree_List_t T) true self Betree_List_Nil
+    in
   match ls with
   | Betree_List_Cons x tl => Ok (x, tl)
   | Betree_List_Nil => Fail_ Failure
@@ -370,7 +372,7 @@ Fixpoint betree_Node_apply_upserts_loop
         betree_Node_apply_upserts_loop n1 msgs1 (Some v) key
       end)
     else (
-      v <- core_option_Option_unwrap u64 prev;
+      v <- core_option_Option_unwrap u64 true prev;
       msgs1 <-
         betree_List_push_front (u64 * betree_Message_t) msgs (key,
           Betree_Message_Insert v);
diff --git a/tests/coq/hashmap/Hashmap_Funs.v b/tests/coq/hashmap/Hashmap_Funs.v
index bd3b57ccf..69add481e 100644
--- a/tests/coq/hashmap/Hashmap_Funs.v
+++ b/tests/coq/hashmap/Hashmap_Funs.v
@@ -229,7 +229,7 @@ Fixpoint hashMap_move_elements_loop
         alloc_vec_Vec_index_mut (AList_t T) usize
           (core_slice_index_SliceIndexUsizeSliceTInst (AList_t T)) slots i;
       let (a, index_mut_back) := p in
-      let (ls, a1) := core_mem_replace (AList_t T) a AList_Nil in
+      let (ls, a1) := core_mem_replace (AList_t T) true a AList_Nil in
       ntable1 <- hashMap_move_elements_from_list T n1 ntable ls;
       i2 <- usize_add i 1%usize;
       slots1 <- index_mut_back a1;
@@ -467,7 +467,7 @@ Fixpoint hashMap_remove_from_list_loop
       if ckey s= key
       then
         let (mv_ls, _) :=
-          core_mem_replace (AList_t T) (AList_Cons ckey t tl) AList_Nil in
+          core_mem_replace (AList_t T) true (AList_Cons ckey t tl) AList_Nil in
         match mv_ls with
         | AList_Cons _ cvalue tl1 => Ok (Some cvalue, tl1)
         | AList_Nil => Fail_ Failure
diff --git a/tests/coq/misc/External_FunsExternal_Template.v b/tests/coq/misc/External_FunsExternal_Template.v
index 03df26563..2f144f475 100644
--- a/tests/coq/misc/External_FunsExternal_Template.v
+++ b/tests/coq/misc/External_FunsExternal_Template.v
@@ -12,7 +12,7 @@ Include External_Types.
 Module External_FunsExternal_Template.
 
 (** [core::cell::{core::cell::Cell<T>#10}::get]:
-    Source: '/rustc/library/core/src/cell.rs', lines 510:4-510:26
+    Source: '/rustc/library/core/src/cell.rs', lines 509:4-509:26
     Name pattern: core::cell::{core::cell::Cell<@T>}::get *)
 Axiom core_cell_Cell_get :
   forall(T : Type) (markerCopyInst : core_marker_Copy_t T),
@@ -20,7 +20,7 @@ Axiom core_cell_Cell_get :
 .
 
 (** [core::cell::{core::cell::Cell<T>#11}::get_mut]:
-    Source: '/rustc/library/core/src/cell.rs', lines 588:4-588:39
+    Source: '/rustc/library/core/src/cell.rs', lines 587:4-587:39
     Name pattern: core::cell::{core::cell::Cell<@T>}::get_mut *)
 Axiom core_cell_Cell_get_mut :
   forall(T : Type),
diff --git a/tests/coq/misc/NoNestedBorrows.v b/tests/coq/misc/NoNestedBorrows.v
index 923609c50..05235bbcd 100644
--- a/tests/coq/misc/NoNestedBorrows.v
+++ b/tests/coq/misc/NoNestedBorrows.v
@@ -322,7 +322,7 @@ Fixpoint list_rev_aux
 (** [no_nested_borrows::list_rev]:
     Source: 'tests/src/no_nested_borrows.rs', lines 319:0-319:42 *)
 Definition list_rev (T : Type) (l : List_t T) : result (List_t T) :=
-  let (li, _) := core_mem_replace (List_t T) l List_Nil in
+  let (li, _) := core_mem_replace (List_t T) true l List_Nil in
   list_rev_aux T li List_Nil
 .
 
@@ -485,7 +485,7 @@ Check (test_weird_borrows1 )%return.
 (** [no_nested_borrows::test_mem_replace]:
     Source: 'tests/src/no_nested_borrows.rs', lines 407:0-407:37 *)
 Definition test_mem_replace (px : u32) : result u32 :=
-  let (y, _) := core_mem_replace u32 px 1%u32 in
+  let (y, _) := core_mem_replace u32 true px 1%u32 in
   if y s= 0%u32 then Ok 2%u32 else Fail_ Failure
 .
 
diff --git a/tests/fstar/arrays/Arrays.Funs.fst b/tests/fstar/arrays/Arrays.Funs.fst
index 5aad99e03..16bcc9b12 100644
--- a/tests/fstar/arrays/Arrays.Funs.fst
+++ b/tests/fstar/arrays/Arrays.Funs.fst
@@ -28,17 +28,17 @@ let array_to_mut_slice_
 (** [arrays::array_len]:
     Source: 'tests/src/arrays.rs', lines 28:0-28:40 *)
 let array_len (t : Type0) (s : array t 32) : result usize =
-  let* s1 = array_to_slice t 32 s in Ok (slice_len t s1)
+  let* s1 = array_to_slice t 32 s in Ok (slice_len t true s1)
 
 (** [arrays::shared_array_len]:
     Source: 'tests/src/arrays.rs', lines 32:0-32:48 *)
 let shared_array_len (t : Type0) (s : array t 32) : result usize =
-  let* s1 = array_to_slice t 32 s in Ok (slice_len t s1)
+  let* s1 = array_to_slice t 32 s in Ok (slice_len t true s1)
 
 (** [arrays::shared_slice_len]:
     Source: 'tests/src/arrays.rs', lines 36:0-36:44 *)
 let shared_slice_len (t : Type0) (s : slice t) : result usize =
-  Ok (slice_len t s)
+  Ok (slice_len t true s)
 
 (** [arrays::index_array_shared]:
     Source: 'tests/src/arrays.rs', lines 40:0-40:57 *)
@@ -312,7 +312,7 @@ let rec sum_loop
   (s : slice u32) (sum1 : u32) (i : usize) :
   Tot (result u32) (decreases (sum_loop_decreases s sum1 i))
   =
-  let i1 = slice_len u32 s in
+  let i1 = slice_len u32 true s in
   if i < i1
   then
     let* i2 = slice_index_usize u32 s i in
@@ -332,7 +332,7 @@ let rec sum2_loop
   (s : slice u32) (s2 : slice u32) (sum1 : u32) (i : usize) :
   Tot (result u32) (decreases (sum2_loop_decreases s s2 sum1 i))
   =
-  let i1 = slice_len u32 s in
+  let i1 = slice_len u32 true s in
   if i < i1
   then
     let* i2 = slice_index_usize u32 s i in
@@ -346,8 +346,8 @@ let rec sum2_loop
 (** [arrays::sum2]:
     Source: 'tests/src/arrays.rs', lines 255:0-255:41 *)
 let sum2 (s : slice u32) (s2 : slice u32) : result u32 =
-  let i = slice_len u32 s in
-  let i1 = slice_len u32 s2 in
+  let i = slice_len u32 true s in
+  let i1 = slice_len u32 true s2 in
   if i = i1 then sum2_loop s s2 0 0 else Fail Failure
 
 (** [arrays::f0]:
@@ -431,7 +431,7 @@ let rec zero_slice_loop
 (** [arrays::zero_slice]:
     Source: 'tests/src/arrays.rs', lines 306:0-306:31 *)
 let zero_slice (a : slice u8) : result (slice u8) =
-  let len = slice_len u8 a in zero_slice_loop a 0 len
+  let len = slice_len u8 true a in zero_slice_loop a 0 len
 
 (** [arrays::iter_mut_slice]: loop 0:
     Source: 'tests/src/arrays.rs', lines 317:4-321:1 *)
@@ -446,7 +446,7 @@ let rec iter_mut_slice_loop
 (** [arrays::iter_mut_slice]:
     Source: 'tests/src/arrays.rs', lines 315:0-315:35 *)
 let iter_mut_slice (a : slice u8) : result (slice u8) =
-  let len = slice_len u8 a in let* _ = iter_mut_slice_loop len 0 in Ok a
+  let len = slice_len u8 true a in let* _ = iter_mut_slice_loop len 0 in Ok a
 
 (** [arrays::sum_mut_slice]: loop 0:
     Source: 'tests/src/arrays.rs', lines 325:4-331:1 *)
@@ -454,7 +454,7 @@ let rec sum_mut_slice_loop
   (a : slice u32) (i : usize) (s : u32) :
   Tot (result u32) (decreases (sum_mut_slice_loop_decreases a i s))
   =
-  let i1 = slice_len u32 a in
+  let i1 = slice_len u32 true a in
   if i < i1
   then
     let* i2 = slice_index_usize u32 a i in
diff --git a/tests/fstar/betree/Betree.Funs.fst b/tests/fstar/betree/Betree.Funs.fst
index 53356bdb6..a63844625 100644
--- a/tests/fstar/betree/Betree.Funs.fst
+++ b/tests/fstar/betree/Betree.Funs.fst
@@ -140,14 +140,14 @@ let betree_List_split_at
     Source: 'src/betree.rs', lines 315:4-315:34 *)
 let betree_List_push_front
   (t : Type0) (self : betree_List_t t) (x : t) : result (betree_List_t t) =
-  let (tl, _) = core_mem_replace (betree_List_t t) self Betree_List_Nil in
+  let (tl, _) = core_mem_replace (betree_List_t t) true self Betree_List_Nil in
   Ok (Betree_List_Cons x tl)
 
 (** [betree::betree::{betree::betree::List<T>#1}::pop_front]:
     Source: 'src/betree.rs', lines 322:4-322:32 *)
 let betree_List_pop_front
   (t : Type0) (self : betree_List_t t) : result (t & (betree_List_t t)) =
-  let (ls, _) = core_mem_replace (betree_List_t t) self Betree_List_Nil in
+  let (ls, _) = core_mem_replace (betree_List_t t) true self Betree_List_Nil in
   begin match ls with
   | Betree_List_Cons x tl -> Ok (x, tl)
   | Betree_List_Nil -> Fail Failure
@@ -304,7 +304,7 @@ let rec betree_Node_apply_upserts_loop
       betree_Node_apply_upserts_loop msgs1 (Some v) key
     end
   else
-    let* v = core_option_Option_unwrap u64 prev in
+    let* v = core_option_Option_unwrap u64 true prev in
     let* msgs1 =
       betree_List_push_front (u64 & betree_Message_t) msgs (key,
         Betree_Message_Insert v) in
diff --git a/tests/fstar/hashmap/Hashmap.Funs.fst b/tests/fstar/hashmap/Hashmap.Funs.fst
index 223bde572..6ce7dccf3 100644
--- a/tests/fstar/hashmap/Hashmap.Funs.fst
+++ b/tests/fstar/hashmap/Hashmap.Funs.fst
@@ -169,7 +169,7 @@ let rec hashMap_move_elements_loop
     let* (a, index_mut_back) =
       alloc_vec_Vec_index_mut (aList_t t) usize
         (core_slice_index_SliceIndexUsizeSliceTInst (aList_t t)) slots i in
-    let (ls, a1) = core_mem_replace (aList_t t) a AList_Nil in
+    let (ls, a1) = core_mem_replace (aList_t t) true a AList_Nil in
     let* ntable1 = hashMap_move_elements_from_list t ntable ls in
     let* i2 = usize_add i 1 in
     let* slots1 = index_mut_back a1 in
@@ -344,7 +344,7 @@ let rec hashMap_remove_from_list_loop
     if ckey = key
     then
       let (mv_ls, _) =
-        core_mem_replace (aList_t t) (AList_Cons ckey x tl) AList_Nil in
+        core_mem_replace (aList_t t) true (AList_Cons ckey x tl) AList_Nil in
       begin match mv_ls with
       | AList_Cons _ cvalue tl1 -> Ok (Some cvalue, tl1)
       | AList_Nil -> Fail Failure
diff --git a/tests/fstar/misc/External.FunsExternal.fsti b/tests/fstar/misc/External.FunsExternal.fsti
index fa9d5d70d..99ae86760 100644
--- a/tests/fstar/misc/External.FunsExternal.fsti
+++ b/tests/fstar/misc/External.FunsExternal.fsti
@@ -7,14 +7,14 @@ include External.Types
 #set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
 
 (** [core::cell::{core::cell::Cell<T>#10}::get]:
-    Source: '/rustc/library/core/src/cell.rs', lines 510:4-510:26
+    Source: '/rustc/library/core/src/cell.rs', lines 509:4-509:26
     Name pattern: core::cell::{core::cell::Cell<@T>}::get *)
 val core_cell_Cell_get
   (t : Type0) (markerCopyInst : core_marker_Copy_t t) :
   core_cell_Cell_t t -> state -> result (state & t)
 
 (** [core::cell::{core::cell::Cell<T>#11}::get_mut]:
-    Source: '/rustc/library/core/src/cell.rs', lines 588:4-588:39
+    Source: '/rustc/library/core/src/cell.rs', lines 587:4-587:39
     Name pattern: core::cell::{core::cell::Cell<@T>}::get_mut *)
 val core_cell_Cell_get_mut
   (t : Type0) :
diff --git a/tests/fstar/misc/NoNestedBorrows.fst b/tests/fstar/misc/NoNestedBorrows.fst
index f45d7f23b..8ef0387bd 100644
--- a/tests/fstar/misc/NoNestedBorrows.fst
+++ b/tests/fstar/misc/NoNestedBorrows.fst
@@ -271,7 +271,7 @@ let rec list_rev_aux
 (** [no_nested_borrows::list_rev]:
     Source: 'tests/src/no_nested_borrows.rs', lines 319:0-319:42 *)
 let list_rev (t : Type0) (l : list_t t) : result (list_t t) =
-  let (li, _) = core_mem_replace (list_t t) l List_Nil in
+  let (li, _) = core_mem_replace (list_t t) true l List_Nil in
   list_rev_aux t li List_Nil
 
 (** [no_nested_borrows::test_list_functions]:
@@ -404,7 +404,7 @@ let _ = assert_norm (test_weird_borrows1 = Ok ())
 (** [no_nested_borrows::test_mem_replace]:
     Source: 'tests/src/no_nested_borrows.rs', lines 407:0-407:37 *)
 let test_mem_replace (px : u32) : result u32 =
-  let (y, _) = core_mem_replace u32 px 1 in
+  let (y, _) = core_mem_replace u32 true px 1 in
   if y = 0 then Ok 2 else Fail Failure
 
 (** [no_nested_borrows::test_shared_borrow_bool1]:
diff --git a/tests/lean/Arrays.lean b/tests/lean/Arrays.lean
index bdaa7380e..3cb685544 100644
--- a/tests/lean/Arrays.lean
+++ b/tests/lean/Arrays.lean
@@ -38,19 +38,19 @@ def array_to_mut_slice_
 def array_len (T : Type) (s : Array T 32#usize) : Result Usize :=
   do
   let s1 ← Array.to_slice T 32#usize s
-  Result.ok (Slice.len T s1)
+  Result.ok (Slice.len T true s1)
 
 /- [arrays::shared_array_len]:
    Source: 'tests/src/arrays.rs', lines 32:0-32:48 -/
 def shared_array_len (T : Type) (s : Array T 32#usize) : Result Usize :=
   do
   let s1 ← Array.to_slice T 32#usize s
-  Result.ok (Slice.len T s1)
+  Result.ok (Slice.len T true s1)
 
 /- [arrays::shared_slice_len]:
    Source: 'tests/src/arrays.rs', lines 36:0-36:44 -/
 def shared_slice_len (T : Type) (s : Slice T) : Result Usize :=
-  Result.ok (Slice.len T s)
+  Result.ok (Slice.len T true s)
 
 /- [arrays::index_array_shared]:
    Source: 'tests/src/arrays.rs', lines 40:0-40:57 -/
@@ -351,7 +351,7 @@ def non_copyable_array : Result Unit :=
 /- [arrays::sum]: loop 0:
    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
+  let i1 := Slice.len U32 true s
   if i < i1
   then
     do
@@ -370,7 +370,7 @@ def sum (s : Slice U32) : Result U32 :=
    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
+  let i1 := Slice.len U32 true s
   if i < i1
   then
     do
@@ -385,8 +385,8 @@ divergent def sum2_loop
 /- [arrays::sum2]:
    Source: 'tests/src/arrays.rs', lines 255:0-255:41 -/
 def sum2 (s : Slice U32) (s2 : Slice U32) : Result U32 :=
-  let i := Slice.len U32 s
-  let i1 := Slice.len U32 s2
+  let i := Slice.len U32 true s
+  let i1 := Slice.len U32 true s2
   if i = i1
   then sum2_loop s s2 0#u32 0#usize
   else Result.fail .panic
@@ -479,7 +479,7 @@ divergent def zero_slice_loop
 /- [arrays::zero_slice]:
    Source: 'tests/src/arrays.rs', lines 306:0-306:31 -/
 def zero_slice (a : Slice U8) : Result (Slice U8) :=
-  let len := Slice.len U8 a
+  let len := Slice.len U8 true a
   zero_slice_loop a 0#usize len
 
 /- [arrays::iter_mut_slice]: loop 0:
@@ -495,7 +495,7 @@ divergent def iter_mut_slice_loop (len : Usize) (i : Usize) : Result Unit :=
    Source: 'tests/src/arrays.rs', lines 315:0-315:35 -/
 def iter_mut_slice (a : Slice U8) : Result (Slice U8) :=
   do
-  let len := Slice.len U8 a
+  let len := Slice.len U8 true a
   let _ ← iter_mut_slice_loop len 0#usize
   Result.ok a
 
@@ -503,7 +503,7 @@ def iter_mut_slice (a : Slice U8) : Result (Slice U8) :=
    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
+  let i1 := Slice.len U32 true a
   if i < i1
   then
     do
diff --git a/tests/lean/Betree/Funs.lean b/tests/lean/Betree/Funs.lean
index dd8dfb054..b476f2e91 100644
--- a/tests/lean/Betree/Funs.lean
+++ b/tests/lean/Betree/Funs.lean
@@ -145,14 +145,14 @@ def betree.List.split_at
    Source: 'src/betree.rs', lines 315:4-315:34 -/
 def betree.List.push_front
   (T : Type) (self : betree.List T) (x : T) : Result (betree.List T) :=
-  let (tl, _) := core.mem.replace (betree.List T) self betree.List.Nil
+  let (tl, _) := core.mem.replace (betree.List T) true self betree.List.Nil
   Result.ok (betree.List.Cons x tl)
 
 /- [betree::betree::{betree::betree::List<T>#1}::pop_front]:
    Source: 'src/betree.rs', lines 322:4-322:32 -/
 def betree.List.pop_front
   (T : Type) (self : betree.List T) : Result (T × (betree.List T)) :=
-  let (ls, _) := core.mem.replace (betree.List T) self betree.List.Nil
+  let (ls, _) := core.mem.replace (betree.List T) true self betree.List.Nil
   match ls with
   | betree.List.Cons x tl => Result.ok (x, tl)
   | betree.List.Nil => Result.fail .panic
@@ -304,7 +304,7 @@ divergent def betree.Node.apply_upserts_loop
       betree.Node.apply_upserts_loop msgs1 (some v) key
   else
     do
-    let v ← core.option.Option.unwrap U64 prev
+    let v ← core.option.Option.unwrap U64 true prev
     let msgs1 ←
       betree.List.push_front (U64 × betree.Message) msgs (key,
         betree.Message.Insert v)
diff --git a/tests/lean/External/FunsExternal_Template.lean b/tests/lean/External/FunsExternal_Template.lean
index ce2cfe47c..a94890c46 100644
--- a/tests/lean/External/FunsExternal_Template.lean
+++ b/tests/lean/External/FunsExternal_Template.lean
@@ -10,14 +10,14 @@ set_option linter.unusedVariables false
 open external
 
 /- [core::cell::{core::cell::Cell<T>#10}::get]:
-   Source: '/rustc/library/core/src/cell.rs', lines 510:4-510:26
+   Source: '/rustc/library/core/src/cell.rs', lines 509:4-509:26
    Name pattern: core::cell::{core::cell::Cell<@T>}::get -/
 axiom core.cell.Cell.get
   (T : Type) (markerCopyInst : core.marker.Copy T) :
   core.cell.Cell T → State → Result (State × T)
 
 /- [core::cell::{core::cell::Cell<T>#11}::get_mut]:
-   Source: '/rustc/library/core/src/cell.rs', lines 588:4-588:39
+   Source: '/rustc/library/core/src/cell.rs', lines 587:4-587:39
    Name pattern: core::cell::{core::cell::Cell<@T>}::get_mut -/
 axiom core.cell.Cell.get_mut
   (T : Type) :
diff --git a/tests/lean/Hashmap/Funs.lean b/tests/lean/Hashmap/Funs.lean
index f01f1c4f0..1f261f8fa 100644
--- a/tests/lean/Hashmap/Funs.lean
+++ b/tests/lean/Hashmap/Funs.lean
@@ -175,7 +175,7 @@ divergent def HashMap.move_elements_loop
     let (a, index_mut_back) ←
       alloc.vec.Vec.index_mut (AList T) Usize
         (core.slice.index.SliceIndexUsizeSliceTInst (AList T)) slots i
-    let (ls, a1) := core.mem.replace (AList T) a AList.Nil
+    let (ls, a1) := core.mem.replace (AList T) true a AList.Nil
     let ntable1 ← HashMap.move_elements_from_list T ntable ls
     let i2 ← i + 1#usize
     let slots1 ← index_mut_back a1
@@ -357,7 +357,7 @@ divergent def HashMap.remove_from_list_loop
     if ckey = key
     then
       let (mv_ls, _) :=
-        core.mem.replace (AList T) (AList.Cons ckey t tl) AList.Nil
+        core.mem.replace (AList T) true (AList.Cons ckey t tl) AList.Nil
       match mv_ls with
       | AList.Cons _ cvalue tl1 => Result.ok (some cvalue, tl1)
       | AList.Nil => Result.fail .panic
diff --git a/tests/lean/NoNestedBorrows.lean b/tests/lean/NoNestedBorrows.lean
index 090ca2b22..91b07fb58 100644
--- a/tests/lean/NoNestedBorrows.lean
+++ b/tests/lean/NoNestedBorrows.lean
@@ -336,7 +336,7 @@ divergent def list_rev_aux
 /- [no_nested_borrows::list_rev]:
    Source: 'tests/src/no_nested_borrows.rs', lines 319:0-319:42 -/
 def list_rev (T : Type) (l : List T) : Result (List T) :=
-  let (li, _) := core.mem.replace (List T) l List.Nil
+  let (li, _) := core.mem.replace (List T) true l List.Nil
   list_rev_aux T li List.Nil
 
 /- [no_nested_borrows::test_list_functions]:
@@ -491,7 +491,7 @@ def test_weird_borrows1 : Result Unit :=
 /- [no_nested_borrows::test_mem_replace]:
    Source: 'tests/src/no_nested_borrows.rs', lines 407:0-407:37 -/
 def test_mem_replace (px : U32) : Result U32 :=
-  let (y, _) := core.mem.replace U32 px 1#u32
+  let (y, _) := core.mem.replace U32 true px 1#u32
   if y = 0#u32
   then Result.ok 2#u32
   else Result.fail .panic