diff --git a/iris/proofmode/class_instances_frame.v b/iris/proofmode/class_instances_frame.v
index e3c78d51eb4e9a5c49f7c7cfc3e908d52a2d014a..0af320b676116158e34d75a6e80f25fbf3d2239b 100644
--- a/iris/proofmode/class_instances_frame.v
+++ b/iris/proofmode/class_instances_frame.v
@@ -14,10 +14,14 @@ Implicit Types P Q R : PROP.
 goal. Otherwise we leave [emp] via [frame_here].
 Only if all those options fail, we start decomposing [R], via instances like
 [frame_exist]. To ensure that, all other instances must have cost > 1. *)
-Global Instance frame_here_absorbing p R : Absorbing R → Frame p R R True | 0.
+Lemma frame_here_absorbing p R : Absorbing R → Frame p R R True.
 Proof. intros. by rewrite /Frame intuitionistically_if_elim sep_elim_l. Qed.
-Global Instance frame_here p R : Frame p R R emp | 1.
+Lemma frame_here p R : Frame p R R emp.
 Proof. intros. by rewrite /Frame intuitionistically_if_elim sep_elim_l. Qed.
+Global Instance frame_here_maybe_absorbing p R O :
+  TCIf (Absorbing R) (TCEq O True)%I (TCEq O emp)%I →
+  Frame p R R O | 0.
+Proof. case => [+->|->]; [apply frame_here_absorbing | apply frame_here]. Qed.
 Global Instance frame_affinely_here_absorbing p R :
   Absorbing R → Frame p (<affine> R) R True | 0.
 Proof.
@@ -59,20 +63,20 @@ Global Instance frame_pure_embed `{!BiEmbed PROP PROP'} p P Q (Q' : PROP') φ :
 Proof. rewrite /Frame /MakeEmbed -embed_pure. apply (frame_embed p P Q). Qed.
 
 Global Instance frame_sep_persistent_l progress R P1 P2 Q1 Q2 Q' :
-  Frame true R P1 Q1 → MaybeFrame true R P2 Q2 progress → MakeSep Q1 Q2 Q' →
+  Frame true R P1 Q1 → MaybeFrame true R P2 Q2 progress → TCNoBackTrack (MakeSep Q1 Q2 Q') →
   Frame true R (P1 ∗ P2) Q' | 9.
 Proof.
-  rewrite /Frame /MaybeFrame /MakeSep /= => <- <- <-.
+  rewrite /Frame /MaybeFrame /MakeSep /= => <- <- [<-].
   rewrite {1}(intuitionistically_sep_dup R).
   by rewrite !assoc -(assoc _ _ _ Q1) -(comm _ Q1) assoc -(comm _ Q1).
 Qed.
 Global Instance frame_sep_l R P1 P2 Q Q' :
-  Frame false R P1 Q → MakeSep Q P2 Q' → Frame false R (P1 ∗ P2) Q' | 9.
-Proof. rewrite /Frame /MakeSep => <- <-. by rewrite assoc. Qed.
+  Frame false R P1 Q → TCNoBackTrack (MakeSep Q P2 Q') → Frame false R (P1 ∗ P2) Q' | 9.
+Proof. rewrite /Frame /MakeSep => <- [<-]. by rewrite assoc. Qed.
 Global Instance frame_sep_r p R P1 P2 Q Q' :
-  Frame p R P2 Q → MakeSep P1 Q Q' → Frame p R (P1 ∗ P2) Q' | 10.
+  Frame p R P2 Q → TCNoBackTrack (MakeSep P1 Q Q') → Frame p R (P1 ∗ P2) Q' | 10.
 Proof.
-  rewrite /Frame /MakeSep => <- <-. by rewrite assoc -(comm _ P1) assoc.
+  rewrite /Frame /MakeSep => <- [<-]. by rewrite assoc -(comm _ P1) assoc.
 Qed.
 
 Global Instance frame_big_sepL_cons {A} p (Φ : nat → A → PROP) R Q l x l' :
diff --git a/iris/proofmode/classes.v b/iris/proofmode/classes.v
index 94558ae4ba5fdd0b3cecc1663a689c1f8297de01..92b9b13a15ebd887fe6e6085e97e22defa3a6d74 100644
--- a/iris/proofmode/classes.v
+++ b/iris/proofmode/classes.v
@@ -386,8 +386,8 @@ Global Instance maybe_frame_default_persistent {PROP : bi} (R P : PROP) :
   MaybeFrame true R P P false | 100.
 Proof. intros. rewrite /MaybeFrame /=. by rewrite sep_elim_r. Qed.
 Global Instance maybe_frame_default {PROP : bi} (R P : PROP) :
-  TCOr (Affine R) (Absorbing P) → MaybeFrame false R P P false | 100.
-Proof. intros. rewrite /MaybeFrame /=. apply: sep_elim_r. Qed.
+  TCNoBackTrack (TCOr (Affine R) (Absorbing P)) → MaybeFrame false R P P false | 100.
+Proof. intros [?]. rewrite /MaybeFrame /=. apply: sep_elim_r. Qed.
 
 Class IntoExcept0 {PROP : bi} (P Q : PROP) := into_except_0 : P ⊢ ◇ Q.
 Global Arguments IntoExcept0 {_} _%I _%I : simpl never.
diff --git a/tests/proofmode.v b/tests/proofmode.v
index e9f7005e0db6e44cce68360668dd5f0532003135..05bb0d23aecd731866af765d9ec8494906b784ce 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -651,6 +651,21 @@ Lemma test_iFrame_disjunction_1 P1 P2 Q1 Q2 :
 Proof. intros ?. iIntros "#HP1 HQ2 HP2". iFrame "HP1 HQ2 HP2". Qed.
 Lemma test_iFrame_disjunction_2 P : P -∗ (True ∨ True) ∗ P.
 Proof. iIntros "HP". iFrame "HP". auto. Qed.
+Lemma test_iFrame_disjunction_3_evars `(Φ : nat → PROP) P1 P2 P3 P4 :
+  BiAffine PROP →
+  let n := 5 in
+  let R := fun a => Nat.iter n (fun P => (P1 ∗ P2 ∗ P3 ∗ P4 ∗ Φ a) ∨ P)%I (Φ a) in
+  P1 ⊢ ∃ a, R a.
+Proof.
+  intros ?. cbn. iIntros "HP1". iExists _.
+  Timeout 2 iFrame.
+Abort.
+Lemma test_iFrame_disjunction_4_evars `(Φ : nat → nat → PROP) P :
+  Φ 0 1 ∗ Φ 1 0 ⊢ ∃ n m, (Φ n m ∗ Φ 0 1) ∨ (P ∗ Φ m n).
+Proof.
+  iIntros "(HΦ1 & HΦ2)". iExists _, _.
+  iFrame "HΦ1". by iLeft.
+Qed.
 
 Lemma test_iFrame_conjunction_1 P Q :
   P -∗ Q -∗ (P ∗ Q) ∧ (P ∗ Q).
@@ -667,6 +682,15 @@ Proof.
   (* [iFrame] should simplify [False ∧ Q] to just [False]. *)
   Show.
 Abort.
+Lemma test_iFrame_conjunction_4_evars `(Φ : nat → PROP) P1 P2 P3 P4 P5 :
+  BiAffine PROP →
+  let n := 5 in
+  let R := fun a => Nat.iter n (fun P => (P1 ∗ P2 ∗ P3 ∗ P4 ∗ Φ a) ∧ P)%I (P1 ∗ P2 ∗ P3 ∗ P4 ∗ Φ a)%I in
+  P5 ⊢ ∃ a, R a.
+Proof.
+  intros ?. cbn. iIntros "HP1". iExists _.
+  Timeout 1 iFrame.
+Abort.
 
 Lemma test_iFrame_later `{!BiAffine PROP} P Q : P -∗ Q -∗ ▷ P ∗ Q.
 Proof. iIntros "H1 H2". by iFrame "H1". Qed.