diff --git a/src/phl/ecPhlWhile.ml b/src/phl/ecPhlWhile.ml
index e43f633a8..7d6d5d7e9 100644
--- a/src/phl/ecPhlWhile.ml
+++ b/src/phl/ecPhlWhile.ml
@@ -201,7 +201,7 @@ let t_bdhoare_while_rev_r inv tc =
 (* -------------------------------------------------------------------- *)
 (* Rule for = or >= *)
 
-let t_bdhoare_while_rev_geq_r inv vrnt k (eps: ss_inv) tc =
+let t_bdhoare_while_rev_geq_r inv vrnt (k: ss_inv) (eps: ss_inv) tc =
   let env, hyps, _ = FApi.tc1_eflat tc in
 
   let bhs = tc1_as_bdhoareS tc in
@@ -221,6 +221,11 @@ let t_bdhoare_while_rev_geq_r inv vrnt k (eps: ss_inv) tc =
       "The variant decreasing rate lower-bound cannot "
       "depend on variables written by the loop body";
 
+  if not (PV.indep env (s_write env lp_body) (PV.fv env (EcMemory.memory mem) k.inv)) then
+    tc_error !!tc
+      "The variant upper bound cannot depend on "
+      "variables written by the loop body";
+
   check_single_stmt tc rem_s;
 
   let lp_guard = ss_inv_of_expr m lp_guard_exp in