diff --git a/CHANGELOG.md b/CHANGELOG.md
index 75866d8b84af4a60a0bf93022d96163337ec1e70..835085e1cb9171f519531c144752ca385c889f1c 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -101,6 +101,8 @@ HeapLang, which is now in a separate package `coq-iris-heap-lang`.
 * Remove the laws `pure_forall_2 : (∀ a, ⌜ φ a ⌝) ⊢ ⌜ ∀ a, φ a ⌝` from the BI
   interface and factor it into a type class `BiPureForall`.
 * Add notation `¬ P` for `P → False` to `bi_scope`.
+* Add Coq side-condition `φ` to class `ElimAcc` (similar to what we already had
+  for `ElimInv` and `ElimModal`).
 
 **Changes in `base_logic`:**
 
@@ -176,6 +178,10 @@ HeapLang, which is now in a separate package `coq-iris-heap-lang`.
 * Generalize HeapLang's `mapsto` (`↦`), `array` (`↦∗`), and atomic heap
   connectives to discardable fractions. See the CHANGELOG entry in the category
   `base_logic` for more information.
+* Opening an invariant or eliminating a mask-changing update modality around a
+  non-atomic weakest precondition creates a side-condition `Atomic ...`.
+  Before, this would fail with the unspecific error "iMod: cannot eliminate
+  modality (|={E1,E2}=> ...) in (WP ...)".
 
 **Changes in `heap_lang`:**
 
diff --git a/iris/bi/lib/atomic.v b/iris/bi/lib/atomic.v
index 2658652ece2efd2c39d51badde8ee80bd5c57e0b..a7272ddc27a7dbda26ab4100260c57476cd2e966 100644
--- a/iris/bi/lib/atomic.v
+++ b/iris/bi/lib/atomic.v
@@ -319,17 +319,16 @@ Section lemmas.
 
   (* This lets you open invariants etc. when the goal is an atomic accessor. *)
   Global Instance elim_acc_aacc {X} E1 E2 Ei (α' β' : X → PROP) γ' α β Pas Φ :
-    ElimAcc (X:=X) (fupd E1 E2) (fupd E2 E1) α' β' γ'
+    ElimAcc (X:=X) True (fupd E1 E2) (fupd E2 E1) α' β' γ'
             (atomic_acc E1 Ei α Pas β Φ)
             (λ x', atomic_acc E2 Ei α (β' x' ∗ (γ' x' -∗? Pas))%I β
                 (λ.. x y, β' x' ∗ (γ' x' -∗? Φ x y))
             )%I.
   Proof.
-    rewrite /ElimAcc.
     (* FIXME: Is there any way to prevent maybe_wand from unfolding?
        It gets unfolded by env_cbv in the proofmode, ideally we'd like that
        to happen only if one argument is a constructor. *)
-    iIntros "Hinner >Hacc". iDestruct "Hacc" as (x') "[Hα' Hclose]".
+    iIntros (_) "Hinner >Hacc". iDestruct "Hacc" as (x') "[Hα' Hclose]".
     iMod ("Hinner" with "Hα'") as (x) "[Hα Hclose']".
     iMod (fupd_intro_mask') as "Hclose''"; last iModIntro; first done.
     iExists x. iFrame. iSplitWith "Hclose'".
diff --git a/iris/program_logic/total_weakestpre.v b/iris/program_logic/total_weakestpre.v
index 22c0331dbcdcb205cbf30d8f5f8b5e819b56e68a..469d8838734c2df03b52fe6389ac410dcd0ef577 100644
--- a/iris/program_logic/total_weakestpre.v
+++ b/iris/program_logic/total_weakestpre.v
@@ -292,11 +292,11 @@ Section proofmode_classes.
   Qed.
 
   Global Instance elim_modal_fupd_twp_atomic p s E1 E2 e P Φ :
-    Atomic (stuckness_to_atomicity s) e →
-    ElimModal True p false (|={E1,E2}=> P) P
-            (WP e @ s; E1 [{ Φ }]) (WP e @ s; E2 [{ v, |={E2,E1}=> Φ v }])%I.
+    ElimModal (Atomic (stuckness_to_atomicity s) e) p false
+            (|={E1,E2}=> P) P
+            (WP e @ s; E1 [{ Φ }]) (WP e @ s; E2 [{ v, |={E2,E1}=> Φ v }])%I | 100.
   Proof.
-    intros. by rewrite /ElimModal intuitionistically_if_elim
+    intros ?. by rewrite intuitionistically_if_elim
       fupd_frame_r wand_elim_r twp_atomic.
   Qed.
 
diff --git a/iris/program_logic/weakestpre.v b/iris/program_logic/weakestpre.v
index 6c510ba6d081890fc0f4d3996d5e875b7ddabbfd..1123c57fa5c5b1ddfe3414434b62083a25712e0c 100644
--- a/iris/program_logic/weakestpre.v
+++ b/iris/program_logic/weakestpre.v
@@ -288,11 +288,11 @@ Section proofmode_classes.
   Qed.
 
   Global Instance elim_modal_fupd_wp_atomic p s E1 E2 e P Φ :
-    Atomic (stuckness_to_atomicity s) e →
-    ElimModal True p false (|={E1,E2}=> P) P
-            (WP e @ s; E1 {{ Φ }}) (WP e @ s; E2 {{ v, |={E2,E1}=> Φ v }})%I.
+    ElimModal (Atomic (stuckness_to_atomicity s) e) p false
+            (|={E1,E2}=> P) P
+            (WP e @ s; E1 {{ Φ }}) (WP e @ s; E2 {{ v, |={E2,E1}=> Φ v }})%I | 100.
   Proof.
-    intros. by rewrite /ElimModal intuitionistically_if_elim
+    intros ?. by rewrite intuitionistically_if_elim
       fupd_frame_r wand_elim_r wp_atomic.
   Qed.
 
@@ -300,25 +300,23 @@ Section proofmode_classes.
     AddModal (|={E}=> P) P (WP e @ s; E {{ Φ }}).
   Proof. by rewrite /AddModal fupd_frame_r wand_elim_r fupd_wp. Qed.
 
-  Global Instance elim_acc_wp {X} E1 E2 α β γ e s Φ :
-    Atomic (stuckness_to_atomicity s) e →
-    ElimAcc (X:=X) (fupd E1 E2) (fupd E2 E1)
+  Global Instance elim_acc_wp_atomic {X} E1 E2 α β γ e s Φ :
+    ElimAcc (X:=X) (Atomic (stuckness_to_atomicity s) e)
+            (fupd E1 E2) (fupd E2 E1)
             α β γ (WP e @ s; E1 {{ Φ }})
-            (λ x, WP e @ s; E2 {{ v, |={E2}=> β x ∗ (γ x -∗? Φ v) }})%I.
+            (λ x, WP e @ s; E2 {{ v, |={E2}=> β x ∗ (γ x -∗? Φ v) }})%I | 100.
   Proof.
-    intros ?. rewrite /ElimAcc.
-    iIntros "Hinner >Hacc". iDestruct "Hacc" as (x) "[Hα Hclose]".
+    iIntros (?) "Hinner >Hacc". iDestruct "Hacc" as (x) "[Hα Hclose]".
     iApply (wp_wand with "(Hinner Hα)").
     iIntros (v) ">[Hβ HΦ]". iApply "HΦ". by iApply "Hclose".
   Qed.
 
   Global Instance elim_acc_wp_nonatomic {X} E α β γ e s Φ :
-    ElimAcc (X:=X) (fupd E E) (fupd E E)
+    ElimAcc (X:=X) True (fupd E E) (fupd E E)
             α β γ (WP e @ s; E {{ Φ }})
             (λ x, WP e @ s; E {{ v, |={E}=> β x ∗ (γ x -∗? Φ v) }})%I.
   Proof.
-    rewrite /ElimAcc.
-    iIntros "Hinner >Hacc". iDestruct "Hacc" as (x) "[Hα Hclose]".
+    iIntros (_) "Hinner >Hacc". iDestruct "Hacc" as (x) "[Hα Hclose]".
     iApply wp_fupd.
     iApply (wp_wand with "(Hinner Hα)").
     iIntros (v) ">[Hβ HΦ]". iApply "HΦ". by iApply "Hclose".
diff --git a/iris/proofmode/class_instances.v b/iris/proofmode/class_instances.v
index 6c2b00dcbc1fa9c232ffc5da3b289ca7cbf26454..64c39eb32874fb9a3c1b7fa12a140ae3b207682d 100644
--- a/iris/proofmode/class_instances.v
+++ b/iris/proofmode/class_instances.v
@@ -968,14 +968,14 @@ Proof. rewrite /AddModal bi_tforall_forall. apply add_modal_forall. Qed.
 
 (** ElimInv *)
 Global Instance elim_inv_acc_without_close {X : Type}
-     φ Pinv Pin (M1 M2 : PROP → PROP) α β mγ Q (Q' : X → PROP) :
-  IntoAcc (X:=X) Pinv φ Pin M1 M2 α β mγ →
-  ElimAcc (X:=X) M1 M2 α β mγ Q Q' →
-  ElimInv φ Pinv Pin α None Q Q'.
+     φ1 φ2 Pinv Pin (M1 M2 : PROP → PROP) α β mγ Q (Q' : X → PROP) :
+  IntoAcc (X:=X) Pinv φ1 Pin M1 M2 α β mγ →
+  ElimAcc (X:=X) φ2 M1 M2 α β mγ Q Q' →
+  ElimInv (φ1 ∧ φ2) Pinv Pin α None Q Q'.
 Proof.
   rewrite /ElimAcc /IntoAcc /ElimInv.
-  iIntros (Hacc Helim Hφ) "(Hinv & Hin & Hcont)".
-  iApply (Helim with "[Hcont]").
+  iIntros (Hacc Helim [??]) "(Hinv & Hin & Hcont)".
+  iApply (Helim with "[Hcont]"); first done.
   - iIntros (x) "Hα". iApply "Hcont". iSplitL; simpl; done.
   - iApply (Hacc with "Hinv Hin"). done.
 Qed.
diff --git a/iris/proofmode/class_instances_updates.v b/iris/proofmode/class_instances_updates.v
index 0e0a116d5fa08d7dad97919d44201df2dda12390..5fd7fea8bda20e776893c76b74852bc4a532b877 100644
--- a/iris/proofmode/class_instances_updates.v
+++ b/iris/proofmode/class_instances_updates.v
@@ -170,12 +170,11 @@ Global Instance add_modal_fupd `{!BiFUpd PROP} E1 E2 P Q :
 Proof. by rewrite /AddModal fupd_frame_r wand_elim_r fupd_trans. Qed.
 
 Global Instance elim_acc_fupd `{!BiFUpd PROP} {X} E1 E2 E α β mγ Q :
-  ElimAcc (X:=X) (fupd E1 E2) (fupd E2 E1) α β mγ
+  ElimAcc (X:=X) True (fupd E1 E2) (fupd E2 E1) α β mγ
           (|={E1,E}=> Q)
           (λ x, |={E2}=> β x ∗ (mγ x -∗? |={E1,E}=> Q))%I.
 Proof.
-  rewrite /ElimAcc.
-  iIntros "Hinner >Hacc". iDestruct "Hacc" as (x) "[Hα Hclose]".
+  iIntros (_) "Hinner >Hacc". iDestruct "Hacc" as (x) "[Hα Hclose]".
   iMod ("Hinner" with "Hα") as "[Hβ Hfin]".
   iMod ("Hclose" with "Hβ") as "Hγ". by iApply "Hfin".
 Qed.
diff --git a/iris/proofmode/classes.v b/iris/proofmode/classes.v
index f51b2162fdbea8cef752f603edc56f9104cbd67b..3848fce3f560adadf03c874df2de68698e53d1f1 100644
--- a/iris/proofmode/classes.v
+++ b/iris/proofmode/classes.v
@@ -523,17 +523,18 @@ Definition accessor {PROP : bi} {X : Type} (M1 M2 : PROP → PROP)
 
 (* Typeclass for assertions around which accessors can be eliminated.
    Inputs: [Q], [E1], [E2], [α], [β], [γ]
-   Outputs: [Q']
+   Outputs: [Q'], [φ]
 
    Elliminates an accessor [accessor E1 E2 α β γ] in goal [Q'], turning the goal
-   into [Q'] with a new assumption [α x]. *)
-Class ElimAcc {PROP : bi} {X : Type} (M1 M2 : PROP → PROP)
+   into [Q'] with a new assumption [α x], where [φ] is a side-condition at the
+   Cow level that needs to hold. *)
+Class ElimAcc {PROP : bi} {X : Type} (φ : Prop) (M1 M2 : PROP → PROP)
       (α β : X → PROP) (mγ : X → option PROP)
       (Q : PROP) (Q' : X → PROP) :=
-  elim_acc : ((∀ x, α x -∗ Q' x) -∗ accessor M1 M2 α β mγ -∗ Q).
-Arguments ElimAcc {_} {_} _%I _%I _%I _%I _%I _%I : simpl never.
-Arguments elim_acc {_} {_} _%I _%I _%I _%I _%I _%I {_}.
-Global Hint Mode ElimAcc + ! ! ! ! ! ! ! - : typeclass_instances.
+  elim_acc : φ → ((∀ x, α x -∗ Q' x) -∗ accessor M1 M2 α β mγ -∗ Q).
+Arguments ElimAcc {_} {_} _ _%I _%I _%I _%I _%I _%I : simpl never.
+Arguments elim_acc {_} {_} _ _%I _%I _%I _%I _%I _%I {_}.
+Global Hint Mode ElimAcc + ! - ! ! ! ! ! ! - : typeclass_instances.
 
 (* Turn [P] into an accessor.
    Inputs:
diff --git a/iris/proofmode/ltac_tactics.v b/iris/proofmode/ltac_tactics.v
index ea0886873334e7318a776f7e933da8795073ea44..a600e6e0b5259b4d0bb0301b44d80abfbc48ddda 100644
--- a/iris/proofmode/ltac_tactics.v
+++ b/iris/proofmode/ltac_tactics.v
@@ -24,10 +24,10 @@ performance and horrible error messages, so we wrap it in a [once]. *)
 Ltac iSolveTC :=
   solve [once (typeclasses eauto)].
 
-(** Tactic used for solving side-conditions arising from TC resolution in iMod
-and iInv. *)
+(** Tactic used for solving side-conditions arising from TC resolution in [iMod]
+and [iInv]. *)
 Ltac iSolveSideCondition :=
-  split_and?; try solve [ fast_done | solve_ndisj ].
+  split_and?; try solve [ fast_done | solve_ndisj | iSolveTC ].
 
 (** Used for printing [string]s and [ident]s. *)
 Ltac pretty_ident H :=
diff --git a/iris/proofmode/monpred.v b/iris/proofmode/monpred.v
index 0b6b1df2f4e1d1790d193043795e9854e46ce6c1..0cf886d51f817948ae4b208467a6755c0765efa9 100644
--- a/iris/proofmode/monpred.v
+++ b/iris/proofmode/monpred.v
@@ -569,26 +569,26 @@ Global Instance elim_modal_at_fupd_hyp `{BiFUpd PROP} φ p p' E1 E2 P 𝓟 𝓟'
   ElimModal φ p p' ((|={E1,E2}=> P) i) 𝓟' 𝓠 𝓠'.
 Proof. by rewrite /MakeMonPredAt /ElimModal monPred_at_fupd=><-. Qed.
 
-Global Instance elim_acc_at_None `{BiFUpd PROP} {X} E1 E2 E3 E4 α α' β β' P P'x i :
+Global Instance elim_acc_at_None `{BiFUpd PROP} {X} φ E1 E2 E3 E4 α α' β β' P P'x i :
   (∀ x, MakeEmbed (α x) (α' x)) → (∀ x, MakeEmbed (β x) (β' x)) →
-  ElimAcc (X:=X) (fupd E1 E2) (fupd E3 E4) α' β' (λ _, None) P P'x →
-  ElimAcc (X:=X) (fupd E1 E2) (fupd E3 E4) α β (λ _, None) (P i) (λ x, P'x x i).
+  ElimAcc (X:=X) φ (fupd E1 E2) (fupd E3 E4) α' β' (λ _, None) P P'x →
+  ElimAcc (X:=X) φ (fupd E1 E2) (fupd E3 E4) α β (λ _, None) (P i) (λ x, P'x x i).
 Proof.
-  rewrite /ElimAcc /MakeEmbed. iIntros (Hα Hβ HEA) "Hinner Hacc".
-  iApply (HEA with "[Hinner]").
+  rewrite /ElimAcc /MakeEmbed. iIntros (Hα Hβ HEA ?) "Hinner Hacc".
+  iApply (HEA with "[Hinner]"); first done.
   - iIntros (x).  iSpecialize ("Hinner" $! x). rewrite -Hα. by iIntros (? <-).
   - iMod "Hacc". iDestruct "Hacc" as (x) "[Hα Hclose]". iModIntro. iExists x.
     rewrite -Hα -Hβ. iFrame. iIntros (? _) "Hβ". by iApply "Hclose".
 Qed.
-Global Instance elim_acc_at_Some `{BiFUpd PROP} {X} E1 E2 E3 E4 α α' β β' γ γ' P P'x i :
+Global Instance elim_acc_at_Some `{BiFUpd PROP} {X} φ E1 E2 E3 E4 α α' β β' γ γ' P P'x i :
   (∀ x, MakeEmbed (α x) (α' x)) →
   (∀ x, MakeEmbed (β x) (β' x)) →
   (∀ x, MakeEmbed (γ x) (γ' x)) →
-  ElimAcc (X:=X) (fupd E1 E2) (fupd E3 E4) α' β' (λ x, Some (γ' x)) P P'x →
-  ElimAcc (X:=X) (fupd E1 E2) (fupd E3 E4) α β (λ x, Some (γ x)) (P i) (λ x, P'x x i).
+  ElimAcc (X:=X) φ (fupd E1 E2) (fupd E3 E4) α' β' (λ x, Some (γ' x)) P P'x →
+  ElimAcc (X:=X) φ (fupd E1 E2) (fupd E3 E4) α β (λ x, Some (γ x)) (P i) (λ x, P'x x i).
 Proof.
-  rewrite /ElimAcc /MakeEmbed. iIntros (Hα Hβ Hγ HEA) "Hinner Hacc".
-  iApply (HEA with "[Hinner]").
+  rewrite /ElimAcc /MakeEmbed. iIntros (Hα Hβ Hγ HEA ?) "Hinner Hacc".
+  iApply (HEA with "[Hinner]"); first done.
   - iIntros (x).  iSpecialize ("Hinner" $! x). rewrite -Hα. by iIntros (? <-).
   - iMod "Hacc". iDestruct "Hacc" as (x) "[Hα Hclose]". iModIntro. iExists x.
     rewrite -Hα -Hβ -Hγ. iFrame. iIntros (? _) "Hβ /=". by iApply "Hclose".
diff --git a/tests/heap_lang.ref b/tests/heap_lang.ref
index 0118b3b39b5ee0e3a75e6a0b4b7731637d279d46..b17918505b6f994a2fb86d16a8f92fcbb5eb98c3 100644
--- a/tests/heap_lang.ref
+++ b/tests/heap_lang.ref
@@ -188,6 +188,59 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
   Heq : ∀ v : val, I v ↔ I #true
   ============================
   ⊢ l ↦_(λ _ : val, I #true) □
+"wp_iMod_fupd_atomic"
+     : string
+2 subgoals
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  E1, E2 : coPset
+  P : iPropI Σ
+  ============================
+  Atomic (stuckness_to_atomicity NotStuck) (#() #())
+
+subgoal 2 is:
+ "H" : P
+--------------------------------------∗
+WP #() #() @ E2 {{ _, |={E2,E1}=> True }}
+
+"wp_iInv_atomic"
+     : string
+2 subgoals
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  N : namespace
+  E : coPset
+  P : iProp Σ
+  H : ↑N ⊆ E
+  ============================
+  Atomic (stuckness_to_atomicity NotStuck) (#() #())
+
+subgoal 2 is:
+ "H" : â–· P
+"Hclose" : ▷ P ={E ∖ ↑N,E}=∗ emp
+--------------------------------------∗
+WP #() #() @ E ∖ ↑N {{ _, |={E ∖ ↑N,E}=> True }}
+
+"wp_iInv_atomic_acc"
+     : string
+2 subgoals
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  N : namespace
+  E : coPset
+  P : iProp Σ
+  H : ↑N ⊆ E
+  ============================
+  Atomic (stuckness_to_atomicity NotStuck) (#() #())
+
+subgoal 2 is:
+ "H" : â–· P
+--------------------------------------∗
+WP #() #() @ E ∖ ↑N {{ _, |={E ∖ ↑N}=> ▷ P ∗ True }}
+
 1 subgoal
   
   Σ : gFunctors
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index 88c1030244cb0a45123c0ff51d6db82934970ba5..5196629e5acfa56375056b04dd34c9ac7bbdec0c 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -1,4 +1,4 @@
-From iris.base_logic.lib Require Import gen_inv_heap.
+From iris.base_logic.lib Require Import gen_inv_heap invariants.
 From iris.program_logic Require Export weakestpre total_weakestpre.
 From iris.heap_lang Require Import lang adequacy proofmode notation.
 (* Import lang *again*. This used to break notation. *)
@@ -323,6 +323,34 @@ Section inv_mapsto_tests.
   Abort.
 End inv_mapsto_tests.
 
+Section atomic.
+  Context `{!heapG Σ}.
+
+  (* These tests check if a side-condition for [Atomic] is generated *)
+  Check "wp_iMod_fupd_atomic".
+  Lemma wp_iMod_fupd_atomic E1 E2 P :
+    (|={E1,E2}=> P) -∗ WP #() #() @ E1 {{ _, True }}.
+  Proof.
+    iIntros "H". iMod "H". Show.
+  Abort.
+
+  Check "wp_iInv_atomic".
+  Lemma wp_iInv_atomic N E P :
+    ↑ N ⊆ E →
+    inv N P -∗ WP #() #() @ E {{ _, True }}.
+  Proof.
+    iIntros (?) "H". iInv "H" as "H" "Hclose". Show.
+  Abort.
+  Check "wp_iInv_atomic_acc".
+  Lemma wp_iInv_atomic_acc N E P :
+    ↑ N ⊆ E →
+    inv N P -∗ WP #() #() @ E {{ _, True }}.
+  Proof.
+    (* Test if a side-condition for [Atomic] is generated *)
+    iIntros (?) "H". iInv "H" as "H". Show.
+  Abort.
+End atomic.
+
 Section printing_tests.
   Context `{!heapG Σ}.