Formal models and scripts: spellchecker-candidate-budget-int-overflow

Tools: Python

These are the working models and scripts this part of the hunt used. Some encode the code as it is (a counterexample is the expected result), others a fixed or correct variant; read the header comment of each file. Paths inside them were replaced by placeholders such as $LUCENE (a Lucene checkout) and $WORK.

Findings

• DirectSpellChecker.suggestSimilar computes its candidate budget numSug * maxInspections in int: with setMaxInspections(Integer.MAX_VALUE) ('inspect everything') and any even numSug the budget wraps to -numSug, so the call throws NullPointerException or silently returns no suggestions (finding LFV-986; repro · finding page)
• SpellChecker.suggestSimilar computes its hit budget 10 * numSug in int, so numSug = Integer.MAX_VALUE ('all suggestions'), 214748365 and every other count whose product wraps to <= 0 throw IllegalArgumentException 'numHits must be > 0' instead of returning the suggestions, and counts whose product wraps to a small positive value silently return fewer suggestions (finding LFV-996; repro · finding page)

Files

• directspellchecker-inspection-budget-int-overflow/model/budget_smt.py (used for LFV-986)
• spellchecker-maxhits-int-overflow-and-queue-presize/model/budget_smt.py (used for LFV-996)
• spellchecker-maxhits-int-overflow-and-queue-presize/model/wrap_intervals.py (used for LFV-996)

How to run

• Python: python3 <file>.py; scripts that import z3 need the z3-solver package.

Snapshot of 2026-11-03. AI-assisted; not yet triaged by a human Lucene committer. Feedback: open an issue in lucene-ai-bug-hunt.