diff --git a/flake.lock b/flake.lock
index 0a2d4c2..2698269 100644
--- a/flake.lock
+++ b/flake.lock
@@ -11,11 +11,11 @@
         "rust-overlay": "rust-overlay"
       },
       "locked": {
-        "lastModified": 1724768110,
-        "narHash": "sha256-PPjuaIQa9srw64rDeaatDf3CHPNgLbqwfE0DSdEU37Q=",
-        "owner": "aeneasverif",
+        "lastModified": 1724945475,
+        "narHash": "sha256-Cb1/8daD2gkpHIbif8eXsSEYK1Es2aOgDIHoBHkTUCY=",
+        "owner": "AeneasVerif",
         "repo": "charon",
-        "rev": "13502d2f3bd477ee86acafe5974016dc7707db83",
+        "rev": "b351338f6a84c7a1afc27433eb0ffdc668b3581d",
         "type": "github"
       },
       "original": {
@@ -136,11 +136,11 @@
         "nixpkgs": "nixpkgs"
       },
       "locked": {
-        "lastModified": 1723651234,
-        "narHash": "sha256-u5zHiSygZhMqoc1Z5R2bP9nRwJx3JWq5xyOlcm765wE=",
+        "lastModified": 1724957201,
+        "narHash": "sha256-q8XaJiiErxDXFWhsOVN//WFSXPFmR3W8LvRL4Sov68c=",
         "owner": "FStarLang",
         "repo": "fstar",
-        "rev": "608c8c2cb41cc59f5a4d07fb70677c68aae8fa8a",
+        "rev": "d93417723d03781d0d3b4969eb7f0d6b9671ef6d",
         "type": "github"
       },
       "original": {
@@ -155,11 +155,11 @@
         "nixpkgs": "nixpkgs_2"
       },
       "locked": {
-        "lastModified": 1723651234,
-        "narHash": "sha256-u5zHiSygZhMqoc1Z5R2bP9nRwJx3JWq5xyOlcm765wE=",
+        "lastModified": 1724957201,
+        "narHash": "sha256-q8XaJiiErxDXFWhsOVN//WFSXPFmR3W8LvRL4Sov68c=",
         "owner": "fstarlang",
         "repo": "fstar",
-        "rev": "608c8c2cb41cc59f5a4d07fb70677c68aae8fa8a",
+        "rev": "d93417723d03781d0d3b4969eb7f0d6b9671ef6d",
         "type": "github"
       },
       "original": {
@@ -183,11 +183,11 @@
         ]
       },
       "locked": {
-        "lastModified": 1723656573,
-        "narHash": "sha256-sbNNlkqgBHJZwKLHbRKTKQf4tO/DhOAlC3KTzQrh92Y=",
+        "lastModified": 1724965512,
+        "narHash": "sha256-4QrNXTaIS3BxIB5XwkjC2SoOBfkqWZ66UkKPhasHIto=",
         "owner": "FStarLang",
         "repo": "karamel",
-        "rev": "7862fdc3899b718d39ec98568f78ec40592a622a",
+        "rev": "fa19d3771e6745dac67e834cd077438905ce7720",
         "type": "github"
       },
       "original": {
@@ -246,11 +246,11 @@
         ]
       },
       "locked": {
-        "lastModified": 1724725307,
-        "narHash": "sha256-gnu8JrUFQoy7b927EPuwmWpvk8MSroFl07pplmVueYA=",
+        "lastModified": 1723429325,
+        "narHash": "sha256-4x/32xTCd+xCwFoI/kKSiCr5LQA2ZlyTRYXKEni5HR8=",
         "owner": "oxalica",
         "repo": "rust-overlay",
-        "rev": "f56076b216c266cd855b0811ceb86802e834cdb9",
+        "rev": "65e3dc0fe079fe8df087cd38f1fe6836a0373aad",
         "type": "github"
       },
       "original": {
diff --git a/include/eurydice_glue.h b/include/eurydice_glue.h
index 0451efd..01c3541 100644
--- a/include/eurydice_glue.h
+++ b/include/eurydice_glue.h
@@ -95,6 +95,9 @@ typedef struct {
 #define core_array_equality___core__cmp__PartialEq__Array_U__N___for__Array_T__N____eq( \
     sz, a1, a2, t, _, _ret_t)                                                           \
   Eurydice_array_eq(sz, a1, a2, t, _)
+#define core_array_equality___core__cmp__PartialEq__0___Slice_U____for__Array_T__N___3__eq( \
+    sz, a1, a2, t, _, _ret_t)                                                               \
+  Eurydice_array_eq(sz, a1, ((a2)->ptr), t, _)
 
 #define Eurydice_slice_split_at(slice, mid, element_type, ret_t)               \
   (CLITERAL(ret_t){                                                            \
diff --git a/lib/AstOfLlbc.ml b/lib/AstOfLlbc.ml
index 9adb859..ed68438 100644
--- a/lib/AstOfLlbc.ml
+++ b/lib/AstOfLlbc.ml
@@ -1264,7 +1264,11 @@ let expression_of_rvalue (env : env) (p : C.rvalue) : K.expr =
   | Global { global_id; global_generics = _ } ->
       let global = env.get_nth_global global_id in
       K.with_type (typ_of_ty env global.ty) (K.EQualified (lid_of_name env global.item_meta.name))
-  | Len _ -> failwith "unsupported: Len"
+  | rvalue ->
+      failwith
+        ("unsupported rvalue: `"
+        ^ Charon.PrintExpressions.rvalue_to_string env.format_env rvalue
+        ^ "`")
 
 let expression_of_assertion (env : env) ({ cond; expected } : C.assertion) : K.expr =
   let cond =
@@ -1350,7 +1354,7 @@ let rec expression_of_raw_statement (env : env) (ret_var : C.var_id) (s : C.raw_
         func =
           FnOpRegular
             {
-              func = FunId (FAssumed (ArrayIndexShared | ArrayIndexMut));
+              func = FunId (FAssumed (Index { is_array = true; mutability = _; is_range = false }));
               generics = { types = [ ty ]; _ };
               _;
             };
@@ -1433,15 +1437,16 @@ let rec expression_of_raw_statement (env : env) (ret_var : C.var_id) (s : C.raw_
           | _ -> []
         in
         match fn_ptr.func, fn_ptr.generics.types @ extra_types with
-        | ( FunId (FAssumed (SliceIndexShared | SliceIndexMut)),
+        | ( FunId (FAssumed (Index { is_array = false; mutability = _; is_range = false })),
             [ TAdt (TAssumed (TArray | TSlice), _) ] ) ->
             (* Will decay. See comment above maybe_addrof *)
             rhs
-        | FunId (FAssumed (SliceIndexShared | SliceIndexMut)), [ TAdt (id, generics) ]
+        | ( FunId (FAssumed (Index { is_array = false; mutability = _; is_range = false })),
+            [ TAdt (id, generics) ] )
           when RustNames.is_vec env id generics ->
             (* Will decay. See comment above maybe_addrof *)
             rhs
-        | FunId (FAssumed (SliceIndexShared | SliceIndexMut)), _ ->
+        | FunId (FAssumed (Index { is_array = false; mutability = _; is_range = false })), _ ->
             K.(with_type (TBuf (rhs.typ, false)) (EAddrOf rhs))
         | _ -> rhs
       in
@@ -1577,7 +1582,7 @@ let decl_of_id (env : env) (id : C.any_decl_id) : K.decl option =
       let env = push_type_binders env type_params in
 
       match kind with
-      | Opaque | Error _ -> None
+      | Union _ | Opaque | Error _ -> None
       | Struct fields ->
           let fields =
             List.map
diff --git a/lib/Cleanup1.ml b/lib/Cleanup1.ml
index 935f0dd..5d218bd 100644
--- a/lib/Cleanup1.ml
+++ b/lib/Cleanup1.ml
@@ -56,7 +56,18 @@ let remove_assignments =
           List.map
             (fun atom ->
               let name, typ = AtomMap.find atom not_yet_closed in
-              ( { node = { atom; name; mut = true; mark = ref Krml.Mark.default; meta = None }; typ },
+              ( {
+                  node =
+                    {
+                      atom;
+                      name;
+                      mut = true;
+                      mark = ref Krml.Mark.default;
+                      meta = None;
+                      attempt_inline = false;
+                    };
+                  typ;
+                },
                 if typ = TUnit then
                   Krml.Helpers.eunit
                 else
@@ -153,7 +164,15 @@ let remove_assignments =
               let name, typ = AtomMap.find atom not_yet_closed in
               let b =
                 {
-                  node = { atom; name; mut = true; mark = ref Krml.Mark.default; meta = None };
+                  node =
+                    {
+                      atom;
+                      name;
+                      mut = true;
+                      mark = ref Krml.Mark.default;
+                      meta = None;
+                      attempt_inline = false;
+                    };
                   typ;
                 }
               in