diff --git a/src/Karamel.ml b/src/Karamel.ml
index 6d8d67c9c..634ce5588 100644
--- a/src/Karamel.ml
+++ b/src/Karamel.ml
@@ -627,6 +627,9 @@ Supported options:|}
   let files = Simplify.remove_unused files in
   let files = if !Options.tail_calls then Simplify.tail_calls files else files in
   let files = Simplify.simplify2 files in
+  (* TODO: Inlining.drop_unused here, since this creates more opportunities for
+     elimination (see comment in functional_updates; also true for
+     Simplify.remove_unused). *)
   let files = if Options.(!merge_variables <> No) then SimplifyMerge.simplify files else files in
   if !arg_print_structs then
     print PrintAst.print_files files;
diff --git a/src/Simplify.ml b/src/Simplify.ml
index 1301f7003..eb330e2b8 100644
--- a/src/Simplify.ml
+++ b/src/Simplify.ml
@@ -561,6 +561,10 @@ let functional_updates = object (self)
 
   val mutable make_mut = []
 
+  (* The general case with >= 3 fields reveals a let-binding. This assumes we
+     run after `hoist` to avoid nested let-bindings. This has the disadvantage
+     that for the version with operators, we leave superfluous monomorphized
+     instances of the operators in the file without eliminating them. *)
   method! visit_ELet env b e1 e2 =
     let b = self#visit_binder env b in
     let e1 = self#visit_expr env e1 in
@@ -573,9 +577,16 @@ let functional_updates = object (self)
               true
         ) fields in
       if List.length the_field = 1 then
+        let e1 = match e1.node with
+          | EApp ({ node = EQualified (["LowStar"; "BufferOps"], op2); _ }, [ e2 ])
+            when KString.starts_with op2 "op_Bang_Star" ->
+              with_type e1.typ (EBufRead (e2, Helpers.zerou32))
+          | _ -> e1
+        in
         let the_field, the_expr = List.hd the_field in
         let the_field = Option.must the_field in
-        let the_expr = self#visit_expr env (snd (open_binder b the_expr)) in
+        let the_expr = DeBruijn.subst e1 0 the_expr in
+        let the_expr = self#visit_expr env the_expr in
         make_mut <- (assert_tlid e1.typ, the_field) :: make_mut;
         k (EAssign (with_type the_expr.typ (EField (e1, the_field)), the_expr))
       else
@@ -583,23 +594,25 @@ let functional_updates = object (self)
     in
 
     match e1.node, e2.node with
-    | EBufRead ({ node = EBound i; _ }, j),
-      EBufWrite ({ node = EBound iplusone; _ }, j', { node = EFlat fields; _ })
-      when j = j' && iplusone = i + 1 ->
+    (* Not in terminal position, no shorthand operators. *)
+    | EBufRead (e1, j),
+      EBufWrite (e1', j', { node = EFlat fields; _ })
+      when j = j' && e1' = DeBruijn.lift 1 e1 ->
         (* let uu = (Bound i)[j];
-         * (Bound (i + 1))[j] <- { fi = ei } with ei = e if i = k, (Bound 0).fi otherwise
+         * (Bound (i + 1))[j] <- { f0 = (Bound 0).f0; ... except fk = e }
          * -->
          * (Bound i)[j].fk <- (unlift 1 e)
          *)
         make_assignment fields (fun x -> x)
 
-    | EBufRead ({ node = EBound i; _ }, j),
+    (* In terminal position, no shorthand operators. *)
+    | EBufRead (e1, j),
       ELet (b,
-        { node = EBufWrite ({ node = EBound iplusone; _ }, j', { node = EFlat fields; _ }); _ },
+        { node = EBufWrite (e1', j', { node = EFlat fields; _ }); _ },
         e3)
-      when j = j' && iplusone = i + 1 ->
+      when j = j' && e1' = DeBruijn.lift 1 e1 ->
         (* let uu = (Bound i)[j];
-         * let _ = (Bound (i + 1))[j] <- { fi = ei } with ei = e if i = k, * (Bound 0).fi otherwise in
+         * let _ = (Bound (i + 1))[j] <- { fi = (Bound 0).fi, except fk = e } in
          * e3
          * -->
          * let _ = (Bound i)[j].fk <- (unlift 1 e) in
@@ -609,9 +622,102 @@ let functional_updates = object (self)
           let e3 = self#visit_expr env (snd (open_binder b e3)) in
           ELet (b, with_unit x, e3))
 
+    (* Not in terminal position, both shorthand operators. *)
+    | EApp ({ node = EQualified (["LowStar"; "BufferOps"], op2); _ }, [ e1 ]),
+        EApp ({ node = EQualified (["LowStar"; "BufferOps"], op1); _ },
+          [ e1'; { node = EFlat fields; _ } ])
+      when
+        KString.starts_with op1 "op_Star_Equals" &&
+        KString.starts_with op2 "op_Bang_Star" &&
+          e1' = DeBruijn.lift 1 e1
+      ->
+        (* let uu = !* e1 in
+         * e1 *= { fi = uu.fi except fk = e2 } *)
+        make_assignment fields (fun x -> x)
+
+    (* In terminal position, both shorthand operators. *)
+    | EApp ({ node = EQualified (["LowStar"; "BufferOps"], op2); _ }, [ e1 ]),
+      ELet (b,
+        { node = EApp ({ node = EQualified (["LowStar"; "BufferOps"], op1); _ },
+          [ e1'; { node = EFlat fields; _ } ]); _ },
+        e3)
+      when
+          KString.starts_with op1 "op_Star_Equals" &&
+          KString.starts_with op2 "op_Bang_Star" &&
+          e1' = DeBruijn.lift 1 e1
+      ->
+        make_assignment fields (fun x ->
+          let e3 = self#visit_expr env (snd (open_binder b e3)) in
+          ELet (b, with_unit x, e3))
+
     | _ ->
         ELet (b, e1, self#visit_expr env e2)
 
+  (* The two cases below cover the case where there are only two fields in the
+     record, meaning that there is no intermediate variable (of the form uu_...)
+     being introduced for the dereference expression. *)
+  method! visit_EApp env e es =
+    let e = self#visit_expr env e in
+    let es = List.map (self#visit_expr env) es in
+    match e.node, es with
+    | EQualified (["LowStar"; "BufferOps"], op1),
+      [ e1; { node = EFlat fields; _ } ]
+      when KString.starts_with op1 "op_Star_Equals" ->
+        (* e1: (buf t) *= { fi =  (!* e1).fi except fk = e } *)
+        let f, _ = List.partition (function
+          | Some f, { node =
+              EField ({ node =
+                EApp ( { node =
+                  EQualified (["LowStar"; "BufferOps"], op2); _ },
+                  [ e1' ]); _ }, f'); _ }
+            when f = f' && e1 = e1' && KString.starts_with op2 "op_Bang_Star" ->
+              false
+          | _ ->
+              true
+        ) fields in
+        begin match f with
+        | [ Some f, e ] ->
+            let t = assert_tbuf e1.typ in
+            make_mut <- (assert_tlid t, f) :: make_mut;
+            EAssign (with_type e.typ (
+              EField (
+                with_type t (EBufRead (e1, Helpers.zerou32)),
+                f)),
+              e)
+        | _ ->
+            EApp (e, es)
+        end
+    | _ ->
+        EApp (e, es)
+
+  method! visit_EBufWrite env e1 e2 e3 =
+    let e1 = self#visit_expr env e1 in
+    let e2 = self#visit_expr env e2 in
+    let e3 = self#visit_expr env e3 in
+    (* bufwrite (e1, e2, { fi = bufread (e1, e2).fi except fk = e }) *)
+    match e3.node with
+    | EFlat fields ->
+        let f, _ = List.partition (function
+          | Some f, { node = EField ({ node = EBufRead (e1', e2'); _ }, f'); _ }
+            when f = f' && e1 = e1' && e2 = e2' ->
+              false
+          | _ ->
+              true
+        ) fields in
+        begin match f with
+        | [ Some f, e ] ->
+            make_mut <- (assert_tlid e3.typ, f) :: make_mut;
+            EAssign (with_type e.typ (
+              EField (
+                with_type e3.typ (EBufRead (e1, e2)),
+                f)),
+              e)
+        | _ ->
+            EBufWrite (e1, e2, e3)
+        end
+    | _ ->
+        EBufWrite (e1, e2, e3)
+
   (* The same object is called a second time with the mark_mut flag set to true
    * to mark those fields that now ought to be mutable *)
   method! visit_DType mark_mut name flags n def =
@@ -663,7 +769,7 @@ let misc_cosmetic = object (self)
     | _ ->
         EIfThenElse (e1, e2, e3)
 
-  (* &x[0] --> x *)
+  (* &(x[0]) --> x *)
   method! visit_EAddrOf env e =
     let e = self#visit_expr env e in
     match e.node with
@@ -672,6 +778,7 @@ let misc_cosmetic = object (self)
     | _ ->
         EAddrOf e
 
+  (* (&x)[0] --> x *)
   method! visit_EBufRead env e1 e2 =
     let e1 = self#visit_expr env e1 in
     let e2 = self#visit_expr env e2 in
@@ -681,6 +788,18 @@ let misc_cosmetic = object (self)
     | _ ->
         EBufRead (e1, e2)
 
+  (* *(&x) --> x *)
+  method! visit_EApp env e es =
+    let e = self#visit_expr env e in
+    let es = List.map (self#visit_expr env) es in
+    match e.node, es with
+    | EQualified (["LowStar"; "BufferOps"], op2),
+      [ { node = EAddrOf e2; _ } ]
+      when KString.starts_with op2 "op_Bang_Star" ->
+        e2.node
+    | _ ->
+        EApp (e, es)
+
   method! visit_EBufWrite env e1 e2 e3 =
     let e1 = self#visit_expr env e1 in
     let e2 = self#visit_expr env e2 in
@@ -1689,6 +1808,7 @@ end
 let simplify0 (files: file list): file list =
   let files = remove_local_function_bindings#visit_files () files in
   let files = count_and_remove_locals#visit_files [] files in
+  let files = misc_cosmetic#visit_files () files in
   let files = remove_uu#visit_files () files in
   let files = remove_proj_is#visit_files () files in
   let files = combinators#visit_files () files in
diff --git a/test/FunctionalUpdate.fst b/test/FunctionalUpdate.fst
new file mode 100644
index 000000000..b19cd6d59
--- /dev/null
+++ b/test/FunctionalUpdate.fst
@@ -0,0 +1,64 @@
+module FunctionalUpdate
+
+module B = LowStar.Buffer
+open LowStar.BufferOps
+open FStar.HyperStack.ST
+
+type point = {
+  x: (x:Int32.t { 0 <= Int32.v x && Int32.v x <= 2 });
+  y: (y:Int32.t { 0 <= Int32.v y && Int32.v y <= 2 });
+}
+
+type point3d = {
+  x: (x:Int32.t { 0 <= Int32.v x && Int32.v x <= 2 });
+  y: (y:Int32.t { 0 <= Int32.v y && Int32.v y <= 2 });
+  z: (z:Int32.t { 0 <= Int32.v z && Int32.v z <= 2 });
+}
+
+noeq type point_indir = { point_ref : B.pointer point3d; other : Int32.t }
+
+let f1 (p: B.buffer point): Stack unit
+  (requires (fun h -> B.live h p /\ B.length p = 1))
+  (ensures (fun _ _ _ -> True))
+=
+  let open LowStar.BufferOps in
+  p.(0ul) <- ({ p.(0ul) with x = 0l })
+
+let g1 (p: B.buffer point): Stack unit
+  (requires (fun h -> B.live h p /\ B.length p = 1))
+  (ensures (fun _ _ _ -> True))
+=
+  let open LowStar.BufferOps in
+  p *= ({ !*p with y = 0l })
+
+let f2 (p: B.buffer point3d): Stack unit
+  (requires (fun h -> B.live h p /\ B.length p = 1))
+  (ensures (fun _ _ _ -> True))
+=
+  let open LowStar.BufferOps in
+  p.(0ul) <- ({ p.(0ul) with x = 0l })
+
+let g2 (p: B.buffer point3d): Stack unit
+  (requires (fun h -> B.live h p /\ B.length p = 1))
+  (ensures (fun _ _ _ -> True))
+=
+  let open LowStar.BufferOps in
+  p *= ({ !*p with y = 0l })
+
+let test_set_field2 (r: point_indir)
+  : Stack unit (requires fun h -> B.live h r.point_ref) (ensures fun _ _ _ -> True)
+  =
+    r.point_ref.(0ul) <- { r.point_ref.(0ul) with z = 0l }
+
+let main (): St Int32.t =
+  push_frame ();
+  let r1 = B.alloca (({ x = 1l; y = 2l } <: point)) 1ul in
+  f1 r1;
+  g1 r1;
+  let r2: B.buffer point3d = B.alloca ({ x = 1l; y = 2l; z = 2l }) 1ul in
+  f2 r2;
+  g2 r2;
+  test_set_field2 ({ point_ref = r2; other = 0l });
+  let ret = (!*r1).x `Int32.add` (!*r1).y `Int32.add` (!*r2).x `Int32.add` (!*r2).y `Int32.add` (!*r2).z in
+  pop_frame ();
+  ret
diff --git a/test/Makefile b/test/Makefile
index fe84768c5..3af0dd58e 100644
--- a/test/Makefile
+++ b/test/Makefile
@@ -25,7 +25,7 @@ ifneq ($(RECENT_GCC),"yes")
   FILES 	:= $(filter-out Debug.test,$(FILES))
 endif
 
-CUSTOM		= count-eq count-uu check-unused check-no-constructor check-no-erased
+CUSTOM		= count-pointer count-eq count-uu check-unused check-no-constructor check-no-erased
 WASM_FILES	= \
   WasmTrap.wasm-test Wasm1.wasm-test Wasm2.wasm-test Wasm3.wasm-test \
   Wasm4.wasm-test Wasm5.wasm-test Wasm6.wasm-test Wasm7.wasm-test \
@@ -184,7 +184,6 @@ count-point: $(OUTPUT_DIR)/FunctionalUpdate.exe
 	[ `grep point $(OUTPUT_DIR)/FunctionalUpdate.out/FunctionalUpdate.c | wc -l` = 9 ]
 	[ `grep uu___ $(OUTPUT_DIR)/FunctionalUpdate.out/FunctionalUpdate.c | wc -l` = 0 ]
 
-
 check-unused: $(OUTPUT_DIR)/Unused_B.exe
 	egrep -q 'gets_eliminated.*foobar\)' $(OUTPUT_DIR)/Unused_B.out/Unused_A.c