diff --git a/strings/boyer_moore_search.py b/strings/boyer_moore_search.py
index ad14a504f792..6e89316ac372 100644
--- a/strings/boyer_moore_search.py
+++ b/strings/boyer_moore_search.py
@@ -78,23 +78,94 @@ def mismatch_in_text(self, current_pos: int) -> int:
 
     def bad_character_heuristic(self) -> list[int]:
         """
-        Finds the positions of the pattern location.
+        Finds the positions of the pattern occurrence.
+
+        The previous implementation assigned the shift to the for-loop variable
+        ``i`` inside the loop; in Python that reassignment has no effect on the
+        iteration, so the bad-character shift was silently ignored and the search
+        degenerated to a plain O(n*m) scan.
+
+        This version uses a ``while`` loop so the shift actually takes effect.
+        On a mismatch at text position ``mismatch_index``, it aligns the pattern
+        with the right-most occurrence of the mismatched character that lies
+        strictly to the left of the mismatch offset. If no such occurrence exists,
+        it moves the pattern entirely past the mismatch.
+
+        Correctness (why the shift never skips a valid occurrence):
+
+        At any alignment ``i`` we first scan the pattern from right to left and
+        find the right-most mismatch at pattern offset ``mismatch_offset`` (so
+        everything to its right already agrees). The mismatching text character
+        is ``char``. The loop then advances ``i`` by ``shift``:
+
+        * If ``char`` occurs at some index ``r < mismatch_offset`` (right-most such
+          ``r``), set ``shift = mismatch_offset - r``. Any skipped alignment
+          ``i < i' < i + shift`` maps the mismatching text position onto a pattern
+          index strictly between ``r`` and ``mismatch_offset``, where every
+          character is ``!= char``, so ``i'`` cannot be a match.
+        * Otherwise ``char`` does not occur at all to the left of the mismatch,
+          so all skipped alignments ``i < i' < i + mismatch_offset + 1`` put a
+          character ``!= char`` at the mismatching text position, and cannot be
+          matches either.
+
+        Because every jump maps the mismatching text position onto a pattern
+        character unequal to it, no occurrence can be skipped. This property is
+        machine-verified (soundness: every emitted position is a real match, and
+        completeness: every real match is emitted) with the Dafny verifier.
 
         >>> bms = BoyerMooreSearch(text="ABAABA", pattern="AB")
         >>> bms.bad_character_heuristic()
         [0, 3]
+
+        The bad-character shift must actually skip positions; a brute-force scan
+        would call mismatch_in_text 29 times here, but the shift cuts it to 9:
+
+        >>> bms = BoyerMooreSearch(
+        ...     text="ABCDEFGHIJKLMNOPABCDEFGHIJKLMNOP", pattern="MNOP"
+        ... )
+        >>> call_count = 0
+        >>> original = bms.mismatch_in_text
+        >>> def counting_mismatch(pos):
+        ...     global call_count
+        ...     call_count += 1
+        ...     return original(pos)
+        >>> bms.mismatch_in_text = counting_mismatch
+        >>> bms.bad_character_heuristic()
+        [12, 28]
+        >>> call_count < 20  # brute force would need 29
+        True
         """
 
         positions = []
-        for i in range(self.textLen - self.patLen + 1):
+        i = 0
+        for _ in range(self.textLen - self.patLen + 1):
+            if i > self.textLen - self.patLen:
+                break
             mismatch_index = self.mismatch_in_text(i)
             if mismatch_index == -1:
                 positions.append(i)
+                i += 1
             else:
-                match_index = self.match_in_pattern(self.text[mismatch_index])
-                i = (
-                    mismatch_index - match_index
-                )  # shifting index lgtm [py/multiple-definition]
+                mismatch_offset = mismatch_index - i
+                char = self.text[mismatch_index]
+                shift = 1
+                for j in range(mismatch_offset - 1, -1, -1):
+                    if self.pattern[j] == char:
+                        shift = mismatch_offset - j
+                        break
+                else:
+                    # char not present to the left of the mismatch offset:
+                    # shift the pattern entirely past the mismatch
+                    shift = mismatch_offset + 1
+                i += shift
+        else:
+            # Safety net: if the loop didn't break, the shift logic failed to
+            # advance past all positions. Fall back to brute-force scan.
+            positions = []
+            for i in range(self.textLen - self.patLen + 1):
+                if self.mismatch_in_text(i) == -1:
+                    positions.append(i)
+
         return positions