diff --git a/theories/heap_lang/lang.v b/theories/heap_lang/lang.v
index 45a3fde8c6f2f52cffff1817deac976c038b090c..2471844ed467152f8ac4c1059045fcfd0fcf69de 100644
--- a/theories/heap_lang/lang.v
+++ b/theories/heap_lang/lang.v
@@ -523,6 +523,12 @@ Definition bin_op_eval_bool (op : bin_op) (b1 b2 : bool) : option base_lit :=
   | OffsetOp => None (* Pointer arithmetic *)
   end.
 
+Definition bin_op_eval_loc (op : bin_op) (l1 : loc) (v2 : base_lit) : option base_lit :=
+  match op, v2 with
+  | OffsetOp, (LitInt off) => Some $ LitLoc (l1 +â‚— off)
+  | _, _ => None
+  end.
+
 Definition bin_op_eval (op : bin_op) (v1 v2 : val) : option val :=
   if decide (op = EqOp) then
     (* Crucially, this compares the same way as [CmpXchg]! *)
@@ -534,7 +540,7 @@ Definition bin_op_eval (op : bin_op) (v1 v2 : val) : option val :=
     match v1, v2 with
     | LitV (LitInt n1), LitV (LitInt n2) => LitV <$> bin_op_eval_int op n1 n2
     | LitV (LitBool b1), LitV (LitBool b2) => LitV <$> bin_op_eval_bool op b1 b2
-    | LitV (LitLoc l), LitV (LitInt off) => Some $ LitV $ LitLoc (l +â‚— off)
+    | LitV (LitLoc l1), LitV v2 => LitV <$> bin_op_eval_loc op l1 v2
     | _, _ => None
     end.
 
diff --git a/theories/heap_lang/metatheory.v b/theories/heap_lang/metatheory.v
index 49629d63e946fb8a4d23eabc33131e4df1755dfb..090b2260154862ae4e55017af3982a63d114a004 100644
--- a/theories/heap_lang/metatheory.v
+++ b/theories/heap_lang/metatheory.v
@@ -88,7 +88,7 @@ Lemma  bin_op_eval_closed op v1 v2 v':
   is_closed_val v1 → is_closed_val v2 → bin_op_eval op v1 v2 = Some v' →
   is_closed_val v'.
 Proof.
-  rewrite /bin_op_eval /bin_op_eval_bool /bin_op_eval_int;
+  rewrite /bin_op_eval /bin_op_eval_bool /bin_op_eval_int /bin_op_eval_loc;
     repeat case_match; by naive_solver.
 Qed.
 
diff --git a/theories/heap_lang/proph_erasure.v b/theories/heap_lang/proph_erasure.v
index f12382ee310169572417ed71c50352de0db58cfd..5f18f766728976749ee257187be39997de10b3d1 100644
--- a/theories/heap_lang/proph_erasure.v
+++ b/theories/heap_lang/proph_erasure.v
@@ -174,7 +174,7 @@ Lemma bin_op_eval_erase op v1 v2 v' :
   bin_op_eval op (erase_val v1) (erase_val v2) = Some v' ↔
   ∃ w, bin_op_eval op v1 v2 = Some w ∧ erase_val w = v'.
 Proof.
-  rewrite /bin_op_eval /bin_op_eval_int /bin_op_eval_bool;
+  rewrite /bin_op_eval /bin_op_eval_int /bin_op_eval_bool /bin_op_eval_loc;
     split; [intros ?|intros (?&?&?)];
       repeat (case_match; simplify_eq/=); eauto.
   - eexists _; split; eauto; simpl.