diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index 5d5e8dff1af72b48d7f508f323d061625b4ab9e4..45c124d9840d912e4f36d0d754cf4afb2206d8a0 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -408,4 +408,12 @@ Proof.
   eexists. split. iIntros "#? ? ? ?". iAccu. done.
 Qed.
 
+Lemma test_iAssumption_evar P : ∃ R, (R ⊢ P) /\ R = P.
+Proof.
+  eexists. split.
+  - iIntros "H". iAssumption.
+  (* Now verify that the evar was chosen as desired (i.e., it should not pick False). *)
+  - reflexivity.
+Qed.
+
 End tests.