diff --git a/flake.lock b/flake.lock
index 827ac174..e77d6de5 100644
--- a/flake.lock
+++ b/flake.lock
@@ -26,11 +26,11 @@
         "rust-overlay": "rust-overlay"
       },
       "locked": {
-        "lastModified": 1780248582,
-        "narHash": "sha256-zzh6JL6Boun4OFBSndfSM+5aZJUXfVNaYgePxIszBOA=",
+        "lastModified": 1780311953,
+        "narHash": "sha256-YEbUYbgdW1BddC9xxqOF0W2kaWLRrA/5IjxUn0sVJ04=",
         "owner": "aeneasverif",
         "repo": "charon",
-        "rev": "42836b36b666a980cbc9d438a8aed340ad3b848b",
+        "rev": "65dcdb566e05472a6bca8074318c05f729e30177",
         "type": "github"
       },
       "original": {
@@ -698,17 +698,17 @@
         ]
       },
       "locked": {
-        "lastModified": 1780024773,
-        "narHash": "sha256-aU9nlrS9S+IJ2EiCzsaxzOXUhggogqTrJojBicE6Oeg=",
+        "lastModified": 1780284119,
+        "narHash": "sha256-y2wR4Mk6D/N1ID4FZa2oUMStCUxyIoRzmgOOpLzoWmo=",
         "owner": "oxalica",
         "repo": "rust-overlay",
-        "rev": "40b0a3a193e0840c76174b4a322874c8f6dd0a63",
+        "rev": "51390d0bfca0a68a8c337d215a4bbeddc2ca616e",
         "type": "github"
       },
       "original": {
         "owner": "oxalica",
         "repo": "rust-overlay",
-        "rev": "40b0a3a193e0840c76174b4a322874c8f6dd0a63",
+        "rev": "51390d0bfca0a68a8c337d215a4bbeddc2ca616e",
         "type": "github"
       }
     },
diff --git a/lib/AstOfLlbc.ml b/lib/AstOfLlbc.ml
index 112b070d..b4eebd65 100644
--- a/lib/AstOfLlbc.ml
+++ b/lib/AstOfLlbc.ml
@@ -1886,7 +1886,7 @@ let maybe_reborrow_slice t_dst e_src =
 
 let expression_of_rvalue (env : env) (p : C.rvalue) expected_ty : K.expr =
   match p with
-  | Use op -> expression_of_operand env op
+  | Use (op, _) -> expression_of_operand env op
   (* Generally, MIR / current LLBC is guaranteed to apply [Deref] only to places that are
      references or raw pointers, in these cases [&*p] == [p].
      The [Deref] traits types are desugared to function calls to [deref].