diff --git a/packages/compiler/src/ir/integer-loop-facts.ts b/packages/compiler/src/ir/integer-loop-facts.ts
index d18f42297..0017a152c 100644
--- a/packages/compiler/src/ir/integer-loop-facts.ts
+++ b/packages/compiler/src/ir/integer-loop-facts.ts
@@ -154,6 +154,112 @@ export function boundedIntegerLoopFacts(
   return result;
 }
 
+/** Bound counters of a while loop by its condition. A counter qualifies when
+ * the loop (condition and body) changes it only by increments of positive
+ * integer literals outside nested loops, switch and exception regions, and a
+ * conjunct of the condition compares it below a literal or a binding the loop
+ * never writes (`while (x * x + y * y <= 4 && it < MAX) it++`). The body runs
+ * only after that conjunct held, and the condition never writes the counter,
+ * so every pass starts at most at the conjunct's bound and climbs by at most
+ * the sum of the body's increments. The counter starts at its entry fact and
+ * only grows, so the range holds at every read inside and after the loop. */
+export function guardedLoopCounterFacts(
+  loop: IrStmt & { kind: "while" },
+  locals: ReadonlyMap<string, IrLocal>,
+  initial: ReadonlyMap<string, IntegerRange>,
+): ReadonlyMap<string, IntegerRange> {
+  const result = new Map<string, IntegerRange>();
+  const budget = new Map<string, number>(),
+    refused = new Set<string>();
+  let opaque = 0;
+  const write = (id: string, delta: number | null): void => {
+    if (opaque || delta === null || delta <= 0 || delta > 2147483647) refused.add(id);
+    else budget.set(id, (budget.get(id) ?? 0) + delta);
+  };
+  const expr = (e: IrExpr): boolean => {
+    if (e.kind === "assignExpr") write(e.localId, increment(e.localId, e.value));
+    if (e.kind === "incDec") write(e.localId, e.op === "+" ? 1 : null);
+    return everyExprChild(e, expr, stmt);
+  };
+  const stmt = (s: IrStmt): boolean => {
+    const region =
+      s.kind === "for" ||
+      s.kind === "while" ||
+      s.kind === "doWhile" ||
+      s.kind === "forOf" ||
+      s.kind === "tryCatch" ||
+      s.kind === "switch";
+    if (region) opaque++;
+    if (s.kind === "assign") write(s.localId, increment(s.localId, s.value));
+    if (s.kind === "varDecl" || s.kind === "forOf") write(s.localId, null);
+    if (s.kind === "tryCatch" && s.catchLocalId) write(s.catchLocalId, null);
+    const completed = everyStmtChild(s, expr, stmt);
+    if (region) opaque--;
+    return completed;
+  };
+  // The condition is evaluated before every pass; a write there would
+  // separate the compared value from the one the body sees.
+  const condition = new Set<string>();
+  const conditionWrites = (e: IrExpr): boolean => {
+    if (e.kind === "assignExpr" || e.kind === "incDec") condition.add(e.localId);
+    return everyExprChild(e, conditionWrites, (s) => {
+      opaque++;
+      stmt(s);
+      opaque--;
+      return true;
+    });
+  };
+  conditionWrites(loop.cond);
+  for (const id of condition) refused.add(id);
+  loop.body.every(stmt);
+  const stable = (id: string): boolean => {
+    const local = locals.get(id);
+    return local !== undefined && !local.boxed && !local.tdz && !budget.has(id) && !refused.has(id);
+  };
+  const limit = (e: IrExpr): IntegerRange | null => {
+    if (e.kind === "numLit" && Number.isSafeInteger(e.value) && !Object.is(e.value, -0))
+      return { min: e.value, max: e.value };
+    if (e.kind === "varRef" && stable(e.localId)) return initial.get(e.localId) ?? null;
+    return null;
+  };
+  // Conjuncts that hold whenever the body runs.
+  const conjuncts: IrExpr[] = [];
+  const collect = (e: IrExpr): void => {
+    if (e.kind === "toBool") collect(e.operand);
+    else if (e.kind === "logical" && e.op === "&&") {
+      collect(e.left);
+      collect(e.right);
+    } else conjuncts.push(e);
+  };
+  collect(loop.cond);
+  const ceiling = new Map<string, number>();
+  for (const c of conjuncts) {
+    if (c.kind !== "bin") continue;
+    // `counter < bound` or `bound > counter` (and the inclusive forms).
+    const below = c.op === "<" || c.op === "<=",
+      above = c.op === ">" || c.op === ">=";
+    const counter = below ? c.left : above ? c.right : null,
+      other = below ? c.right : c.left;
+    if (counter?.kind !== "varRef") continue;
+    const bound = limit(other);
+    if (!bound) continue;
+    const hi = c.op === "<" || c.op === ">" ? bound.max - 1 : bound.max;
+    const previous = ceiling.get(counter.localId);
+    ceiling.set(counter.localId, previous === undefined ? hi : Math.min(previous, hi));
+  }
+  for (const [id, step] of budget) {
+    const local = locals.get(id),
+      start = initial.get(id),
+      hi = ceiling.get(id);
+    if (refused.has(id) || !local || local.boxed || local.tdz || !start || hi === undefined)
+      continue;
+    const max = Math.max(start.max, hi + step);
+    if (Number.isSafeInteger(start.min) && Number.isSafeInteger(max))
+      result.set(id, { min: start.min, max });
+  }
+  return result;
+}
+
 /** Recognize only exits whose target cannot be inside this statement list.
  * Labeled blocks, loops, switch and exception regions retain the join. */
 export function integerPathFallsThrough(body: readonly IrStmt[]): boolean {
diff --git a/packages/compiler/src/ir/integer-ranges.test.ts b/packages/compiler/src/ir/integer-ranges.test.ts
index 9ee1d55ff..ac9e4a98a 100644
--- a/packages/compiler/src/ir/integer-ranges.test.ts
+++ b/packages/compiler/src/ir/integer-ranges.test.ts
@@ -611,6 +611,101 @@ test("a loop-invariant positive step bounds the counter of a limited loop", () =
     expect(loop(step, update, body).inside, label).toBeNull();
 });
 
+test("a while condition bounds a counter the loop only increments", () => {
+  // it = start; while (unknown <= 4 && it < MAX) { observe(it); it++ } observe(it)
+  const set = (localId: string, value: IrExpr): IrStmt => ({ loc, kind: "assign", localId, value });
+  const bump = (op: "+" | "-" = "+"): IrStmt => ({
+    loc,
+    kind: "exprStmt",
+    expr: { loc, kind: "incDec", op, prefix: false, localId: "it", type: F64 },
+  });
+  const and = (left: IrExpr, right: IrExpr): IrExpr => ({
+    loc,
+    kind: "logical",
+    op: "&&",
+    left,
+    right,
+    type: BOOL,
+  });
+  const run = (
+    options: {
+      start?: IrExpr;
+      cond?: IrExpr;
+      body?: IrStmt[];
+      before?: IrStmt[];
+    } = {},
+  ) => {
+    const inside = ref("it"),
+      after = ref("it");
+    const f = fn([
+      set("max", num(300)),
+      set("it", options.start ?? num(0)),
+      ...(options.before ?? []),
+      {
+        loc,
+        kind: "while",
+        cond:
+          options.cond ??
+          and(condition("<=", ref("unknown"), num(4)), condition("<", ref("it"), ref("max"))),
+        body: options.body ?? [observe(inside), bump()],
+      },
+      observe(after),
+    ]);
+    for (const id of ["it", "max"]) f.locals.push({ id, name: id, type: F64, mutable: true });
+    const ranges = analyzeIntegerRanges(f);
+    return { inside: ranges.get(inside), after: ranges.get(after) };
+  };
+  expect(run()).toEqual({ inside: { min: 0, max: 299 }, after: { min: 0, max: 300 } });
+  // `MAX > it`, an inclusive bound, two increments per pass and an early exit.
+  expect(run({ cond: condition(">", ref("max"), ref("it")) }).after).toEqual({ min: 0, max: 300 });
+  expect(run({ cond: condition("<=", ref("it"), num(10)) }).after).toEqual({ min: 0, max: 11 });
+  const twice = [observe(ref("it")), bump(), set("it", bin("+", ref("it"), num(2)))];
+  expect(run({ body: twice }).after).toEqual({ min: 0, max: 302 });
+  const exit: IrStmt = {
+    loc,
+    kind: "if",
+    cond: condition("===", ref("unknown"), num(0)),
+    then: [{ loc, kind: "break" }],
+    else_: null,
+  };
+  expect(run({ body: [exit, bump()] }).after).toEqual({ min: 0, max: 300 });
+  // A start above the bound stays the entry value.
+  expect(run({ start: num(500) }).after).toEqual({ min: 500, max: 500 });
+  // Decrements, fractional or variable steps, increments in a nested loop,
+  // writes in the condition, a bound the loop writes, a disjunction, and an
+  // unknown start prove nothing.
+  const nested: IrStmt = {
+    loc,
+    kind: "while",
+    cond: condition("<", ref("unknown"), num(3)),
+    body: [bump()],
+  };
+  const counted: IrExpr = { loc, kind: "incDec", op: "+", prefix: false, localId: "it", type: F64 };
+  const open: [string, Parameters<typeof run>[0]][] = [
+    ["decrement", { body: [bump("-")] }],
+    ["fraction step", { body: [set("it", bin("+", ref("it"), num(0.5)))] }],
+    ["variable step", { body: [set("it", bin("+", ref("it"), ref("unknown")))] }],
+    ["nested increment", { body: [nested] }],
+    ["condition write", { cond: condition("<", counted, ref("max")), body: [] }],
+    ["written bound", { body: [bump(), set("max", num(1e12))] }],
+    [
+      "disjunction",
+      {
+        cond: {
+          loc,
+          kind: "logical",
+          op: "||",
+          left: condition("<=", ref("unknown"), num(4)),
+          right: condition("<", ref("it"), ref("max")),
+          type: BOOL,
+        },
+      },
+    ],
+    ["unknown start", { start: ref("unknown") }],
+  ];
+  for (const [label, options] of open) expect(run(options).after, label).toBeNull();
+});
+
 test("whole-program slot facts seed parameters, field reads and call results", () => {
   const field: IrExpr = {
     loc,
diff --git a/packages/compiler/src/ir/integer-ranges.ts b/packages/compiler/src/ir/integer-ranges.ts
index 25afcdfee..2277b632c 100644
--- a/packages/compiler/src/ir/integer-ranges.ts
+++ b/packages/compiler/src/ir/integer-ranges.ts
@@ -1,7 +1,11 @@
 import type { IrExpr, IrFunction, IrStmt } from "./ir.js";
 import { everyExprChild, everyStmtChild, everyStmtList } from "./traverse.js";
 import { byteNumberAccess, byteNumberRange } from "./byte-numbers.js";
-import { boundedIntegerLoopFacts, integerPathFallsThrough } from "./integer-loop-facts.js";
+import {
+  boundedIntegerLoopFacts,
+  guardedLoopCounterFacts,
+  integerPathFallsThrough,
+} from "./integer-loop-facts.js";
 
 /** Exactly representable integers, excluding negative zero. Facts describe
  * the evaluated value, never a later read of the same local binding. */
@@ -846,15 +850,21 @@ export function analyzeIntegerRanges(fn: IrFunction, slots: IntegerSlotFacts = {
         }
         case "while":
         case "doWhile": {
+          // Counters the condition bounds keep their range at every read
+          // inside and after the loop.
+          const guarded =
+            s.kind === "while" ? guardedLoopCounterFacts(s, loopLocals, facts) : noInvariants;
           const loop = new Map(facts);
-          havoc(loop, [s], loop);
+          havocWith(loop, [s], loop, guarded);
+          for (const [id, range] of guarded) set(loop, id, range);
           const header = new Map(loop);
           expr(s.cond, header);
           if (s.kind === "while") {
             refine(s.cond, true, header);
             body(s.body, header);
           } else body(s.body, new Map(loop));
-          havoc(facts, [s], facts);
+          havocWith(facts, [s], facts, guarded);
+          for (const [id, range] of guarded) set(facts, id, range);
           break;
         }
         case "forOf": {
diff --git a/packages/compiler/test/ts7/baselines/order-parity/tests/corpus/5333-integer-guarded-while-counters.ts.json b/packages/compiler/test/ts7/baselines/order-parity/tests/corpus/5333-integer-guarded-while-counters.ts.json
new file mode 100644
index 000000000..113a84867
--- /dev/null
+++ b/packages/compiler/test/ts7/baselines/order-parity/tests/corpus/5333-integer-guarded-while-counters.ts.json
@@ -0,0 +1,6 @@
+{
+ "order": [
+  "<repo>/tests/corpus/5333-integer-guarded-while-counters.ts"
+ ],
+ "diags": []
+}
diff --git a/tests/corpus/5333-integer-guarded-while-counters.ts b/tests/corpus/5333-integer-guarded-while-counters.ts
new file mode 100644
index 000000000..cd43cc5dc
--- /dev/null
+++ b/tests/corpus/5333-integer-guarded-while-counters.ts
@@ -0,0 +1,122 @@
+// While-loop counters that the loop only increments by integer literals and
+// that a conjunct of the condition bounds (`it < MAX` in an escape-time
+// loop) stay exact integers. Counters written in the condition, decremented,
+// stepped by fractions or unknown values, or incremented inside nested
+// loops, bounds the loop writes, disjunctions, and limits near 2^31, 2^32
+// and 2^53 keep ordinary double behavior.
+
+const MAX: number = 300;
+
+function escape(cx: number, cy: number): number {
+  let x: number = 0;
+  let y: number = 0;
+  let it: number = 0;
+  while (x * x + y * y <= 4 && it < MAX) {
+    const xt: number = x * x - y * y + cx;
+    y = 2 * x * y + cy;
+    x = xt;
+    it++;
+  }
+  return it;
+}
+let inside: number = 0;
+let total: number = 0;
+for (let py: number = 0; py < 24; py++) {
+  for (let px: number = 0; px < 32; px++) {
+    const it: number = escape((px / 32) * 3 - 2, (py / 24) * 2 - 1);
+    total += it;
+    if (it === MAX) inside++;
+  }
+}
+console.log("escape", inside, total, escape(0, 0), escape(2, 2));
+
+// Reversed and inclusive bounds, two increments per pass, early exits and
+// continue, a counter used as an index and a remainder operand.
+function shapes(limit: number): string {
+  const table: Int32Array = new Int32Array(64);
+  let a: number = 0;
+  while (limit > a) a += 3;
+  let b: number = 1;
+  while (b <= 40) {
+    b++;
+    if (b % 7 === 0) continue;
+    b += 2;
+  }
+  let c: number = 0;
+  while (c < 63) {
+    table[c] = c % 5;
+    if (table[c] === 4 && c > 50) break;
+    c++;
+  }
+  let sum: number = 0;
+  for (let i: number = 0; i < 64; i++) sum += table[i];
+  return `${a} ${b} ${c} ${sum}`;
+}
+console.log("shapes", shapes(10), shapes(0), shapes(-5), shapes(64));
+
+// A module-level counter in the initializer.
+let steps: number = 0;
+while (steps < 1000 && (steps * 7) % 11 !== 10) steps++;
+console.log("module", steps);
+
+// Entries outside the proof: fractions, -0, NaN and Infinity starts.
+function starts(start: number): string {
+  let i: number = start;
+  while (i < 5) i++;
+  return `${i} ${Object.is(i, -0)}`;
+}
+console.log("starts", starts(0.5), starts(-0), starts(NaN), starts(Infinity), starts(-2), starts(9));
+
+// Counters that cross 2^31, 2^32 and 2^53 under their bound.
+function wide(): string {
+  let i: number = 0;
+  while (i < 3000000000) i += 1000000000;
+  let j: number = 2147483600;
+  while (j < 2147483647) j += 13;
+  let k: number = 9007199254740980;
+  while (k < 9007199254740991) k += 4;
+  let u: number = 4294967290;
+  while (u <= 4294967295) u++;
+  return `${i} ${j} ${k} ${u} ${j | 0} ${u >>> 0}`;
+}
+console.log("wide", wide());
+
+// Forms the proof refuses: a counter written by its condition, decrements,
+// unknown and fractional steps, nested increments, written bounds and
+// disjunctions. (The first counter stays bounded: its condition writes only
+// `budget`, which is not the counter.)
+function refused(n: number): string {
+  let a: number = 0;
+  let budget: number = n;
+  while (budget-- > 0 && a < 10) a++;
+  let b: number = 0;
+  while (b++ < 5) b += 0;
+  let c: number = 10;
+  while (c < 20) {
+    c++;
+    c--;
+    c += 2;
+  }
+  let d: number = 0;
+  while (d < 3) d += 0.75;
+  let e: number = 0;
+  while (e < 20) e += n;
+  let f: number = 0;
+  while (f < 6) {
+    let g: number = 0;
+    while (g < 3) {
+      f++;
+      g++;
+    }
+  }
+  let h: number = 0;
+  let cap: number = 4;
+  while (h < cap) {
+    h++;
+    if (h === 3) cap = 4.5;
+  }
+  let k: number = 0;
+  while (k < 3 || k === 3) k++;
+  return `${a} ${budget} ${b} ${c} ${d} ${e} ${f} ${h} ${cap} ${k}`;
+}
+console.log("refused", refused(3), refused(25));