WANDScorer prunes documents that score +Infinity once the minimum competitive score is +Infinity

A top-k search tells the scorer the score to beat through Scorable#setMinCompetitiveScore, and the scorer may skip only documents whose score is less than that bound. When finite clause scores add up past Float.MAX_VALUE (about 3.4e38), a document scores +Infinity, which Lucene treats as a valid score. Once the k-th best score is +Infinity, Lucene's own collectors pass +Infinity as the bound: TopFieldCollector for a sort by score and then another field (ties can still win on the second field), and TopScoreDocCollector, which passes Math.nextUp of the k-th score (also +Infinity when that score is exactly Float.MAX_VALUE) and shares the bound across the slices of a concurrent search.

WANDScorer.scaleMinScore asserts that the bound is finite, so with assertions on the search throws AssertionError. With assertions off, (long) Math.floor(+Infinity) is Long.MAX_VALUE, far above every scaled maximum score (each at most 2^24 - 1) and any sum of a few of them, so WANDScorer skips every remaining document, including those that also score +Infinity and should still win. In the repro, 10 documents score +Infinity and the top 3 by (score, rank) should be docs 9, 8, 7; Lucene returns 3, 2, 1. The plain IndexSearcher.search(query, n, sort) call does the same once more than 1,000 documents match, and a concurrent search by score returns the wrong +Infinity ties too. When the k-th score is exactly Float.MAX_VALUE, even a single-threaded search by score alone returns those hits instead of later +Infinity ones. Finite-scored hits are never lost: the documents wrongly skipped all score +Infinity. The trigger is rare: scores must overflow, through huge FeatureField values or huge boosts. By source inspection every release from 8.0.0 to 10.6.0 and main is affected; representative releases were run. Clamping the bound to Float.MAX_VALUE in scaleMinScore fixes it and passes the closest test suites.

1. The route. minShouldMatch > 1 builds a WANDScorer (BooleanScorerSupplier.java:589-590); the comment above it says "WANDScorer should be able to handle ... Any minCompetitiveScore ( >= 0 )" (:582-585). With a MUST_NOT clause, a top-level disjunction reaches it as ReqExclScorer(WANDScorer) when the SHOULD clauses match at most 0.3% of the documents: cost() <= 3L * maxDoc / 1000, with the cost taken from the positive clauses only (:82-101, :203-207); the MUST_NOT clause itself may be dense. ReqExclScorer forwards the bound (ReqExclScorer.java:89-92). Denser SHOULD clauses with minimumNumberShouldMatch <= 1 take ReqExclBulkScorer over MaxScoreBulkScorer instead (:265, :308-328).
2. The score. WANDScorer.score() sums the clause scores as a double and returns (float) leadScore (WANDScorer.java:553-564): each clause scores 1.993842E38 (FeatureField keeps only the top bits of 2e38), and the double sum, about 5.98e38, becomes +Infinity in the cast. FeatureField accepts any positive finite normal value (FeatureField.java:152-171) and linear weights in (0, 64] (:593-596).
3. The bound. A sort whose first field is the score makes TopFieldCollector TOP_SCORES with canSetMinScore (TopFieldCollector.java:342-346). With the queue full and totalHits > totalHitsThreshold it passes the bottom's score itself, +Infinity, not nextUp (:380-386), because a tie on score can still win on rank. The call comes while the 4th hit, doc 3, is collected; the bottom is then doc 1. TopScoreDocCollector passes Math.nextUp(topScore) (TopScoreDocCollector.java:160), which is +Infinity when the k-th score is +Infinity or exactly Float.MAX_VALUE, and in a concurrent search the raw global bound to leaves with smaller doc ids (:141-148).
4. The defect. setMinCompetitiveScore calls scaleMinScore (WANDScorer.java:258-266), which does assert Float.isFinite(minScore); (:112) and then return (long) Math.floor(Math.scalb((double) minScore, scalingFactor)); with the comment "cast might lower the value again if scaled > Long.MAX_VALUE, which is fine" (:116-119). With assertions on, AssertionError; with assertions off, Long.MAX_VALUE.
5. Every document goes. Each clause's scaled max score is capped at MAX_SCALED_SCORE = (1L << 24) - 1 (:58, :98-101); in the repro each clause's max score scales to 8,388,608 and the three sum to 25,165,824, far below Long.MAX_VALUE. WANDScorer keeps a clause in its tail, not advanced, while the tail's summed max scores stay below the bound (insertTailWithOverFlow, :600-601; updateMaxScores, :481). With the bound at Long.MAX_VALUE, all three clauses go to the tail after doc 3 (pushBackLeads, :391-393), none is left to propose a candidate, and the iterator returns NO_MORE_DOCS (:309-315). Docs 4 to 9 are never visited, although each scores +Infinity, which is not less than +Infinity. The same inequality rejects a candidate in matches() (:340-344).

The saturating cast is right for a large finite bound above every reachable score; it is wrong for +Infinity, because a document can score exactly +Infinity.

All returned documents score +Infinity, except in the last row: there they score Float.MAX_VALUE, and docs 4 to 9, which score +Infinity, are skipped. In that row the bound is Math.nextUp(Float.MAX_VALUE), which is +Infinity; with the clamp fix the search returns 4, 5, 6.

• Who is hit. Top-k disjunctions that run on WANDScorer (minimumNumberShouldMatch > 1, or SHOULD clauses that match at most 0.3% of the documents next to a MUST_NOT clause) over documents that score +Infinity: FeatureField linear clauses over very large values (for example sentinels near Float.MAX_VALUE) whose sum overflows, or very large finite boosts. BoostQuery rejects only non-finite or negative boosts, and the classic QueryParser parses a boost with Float.parseFloat: the query string x^B y^B z^B -w with a 38-digit finite boost over ordinary BM25 text reached it in the study.
• Assertions off (production). Silently the wrong top k: hits that score +Infinity are dropped. With a sort by score and then another field (single-threaded, including the plain searcher.search(query, n, sort) once more than 1,000 documents match) or with a concurrent search by score (an executor and more than one slice), the wrong +Infinity ties come back. A single-threaded search by score alone is correct when the k-th score is +Infinity (later ties lose to lower doc ids anyway), but not when it is exactly Float.MAX_VALUE: TopScoreDocCollector's nextUp makes the bound +Infinity, and later +Infinity hits lose to the Float.MAX_VALUE ones (fact-check probe: 0, 1, 2 instead of 4, 5, 6).
• Assertions on (test suites, Lucene's own included). AssertionError for that search, single-threaded or not, through the stock collectors.
• Never. No finite-scored hit is lost: the bound becomes +Infinity only once the k-th score is +Infinity (or exactly Float.MAX_VALUE for TopScoreDocCollector), and then no later finite-scored document could enter the top k, so the documents wrongly skipped all score +Infinity. No extra or excluded document is returned, and the work is bounded and smaller.
• Default vs opt-in, scale. No setting is needed; scores must overflow, and the wrong results also need a score-then-field sort, a concurrent search, or a k-th score of exactly Float.MAX_VALUE. Deterministic, any index size. A rare, low-severity correctness defect.

It fixes the codec to the default because LuceneTestCase randomises it. The total-hits threshold 3 keeps the index at 10 documents; with the default threshold of 1000 (searcher.search(query, 3, sort)) the same failure needs more than 1,000 matching documents. The test passes with the recommended fix and fails on stock, with assertions on and off.

# assertions on (gradle, main 645d4fe14a20)
TestWANDInfiniteMinCompetitiveScore > testInfiniteScoresSortedByScoreThenField FAILED
    java.lang.AssertionError
        at __randomizedtesting.SeedInfo.seed([DEADBEEF:192FFA96F9D0EF7B]:0)
        at org.apache.lucene.search.WANDScorer.scaleMinScore(WANDScorer.java:112)
        at org.apache.lucene.search.WANDScorer.setMinCompetitiveScore(WANDScorer.java:264)
        at org.apache.lucene.search.ScoreCachingWrappingScorer.setMinCompetitiveScore(ScoreCachingWrappingScorer.java:95)
        at org.apache.lucene.search.TopFieldCollector.updateMinCompetitiveScore(TopFieldCollector.java:385)
        ...

# -Ptests.asserts=false
TestWANDInfiniteMinCompetitiveScore > testInfiniteScoresSortedByScoreThenField FAILED
    org.junit.ComparisonFailure: expected:<[[9, 8, 7]]> but was:<[[3, 2, 1]]>

# the same on the 10.6.0, 10.5.2 and 9.12.3 release jars (9.12.3: WANDScorer.java:111),
# and 10 of 10 iterations in each mode on main

• The contract. Scorable#setMinCompetitiveScore: the scorer "may safely ignore all documents whose score is less than the given minScore" (Scorable.java:45-51).
• Valid scores. "The values Float#NaN and Float#NEGATIVE_INFINITY are not valid scores" (TopScoreDocCollector.java:30-31). LUCENE-2271 (7b9c0f79695, 2010) took POSITIVE_INFINITY off that list on purpose.
• Lucene's own checks allow it. The BooleanScorerSupplier comment says WANDScorer should handle "Any minCompetitiveScore ( >= 0 )" (:584); the test framework's AssertingScorer.setMinCompetitiveScore requires a scorer that may score and a non-NaN bound that never decreases, but not a finite one (AssertingScorer.java:89-95).
• History. The cast comment dates from LUCENE-4100 (2017), when the assertion was only not-NaN; #794 (2022, an accuracy change with no review comments) narrowed it to isFinite without a documented caller rule. LUCENE-10553 (#860) fixed +Infinity max scores; its tests keep actual scores finite. We found no javadoc, test, CHANGES entry or recorded discussion that restricts +Infinity scores or bounds (source, history, CHANGES and the prior-art searches).

The strongest case (an intended-behaviour verifier and a cross-model reviewer built it): the isFinite assertion is an author-written precondition; upstream fixes infinite scores where they are produced (LUCENE-3357, LUCENE-3215), AssertingSimilarity requires finite scores, and LUCENE-8016 (#9064, open) calls infinite scores from huge boosts trappy. Scores of 3.4e38 are garbage in.

Why it fails: the precondition is private and undocumented, and Lucene's own collectors break it; the documented rules allow +Infinity; the finite-score checks cover Similarity implementations only, while here every clause score is finite and only WANDScorer's own sum overflows; LUCENE-8016 was never implemented and would not cover feature values or sum overflow. The cross-model reviews rated the case weak and the adjudication found it weak; the intended-behaviour check, which built it, was "medium-high" confident that the behaviour is not intended. A later fact-check reviewer (OpenAI GPT-5.6) rated it moderate: a maintainer could reasonably call the input pathological or prefer a fix where scores are produced. It is a fair reason for low priority and for asking where to fix it, not for the current result.

The recommended fix was written by an independent verifier and run in a scratch worktree of 645d4fe14a20 (OpenJDK 25.0.3, seed DEADBEEF), removed afterwards. Maintainers may prefer to fix it where infinite scores are produced; the options below say what each costs. The sibling bug in ScorerUtil.minRequiredScore (same trigger, block-max conjunctions and MaxScoreBulkScorer) needs its own fix; neither fix covers the other.

Keep only the not-NaN assertion and clamp minScore to Float.MAX_VALUE before scaling (+4/-1 in WANDScorer.java). A document scores +Infinity only if the exact sum of its clause scores exceeds Float.MAX_VALUE; the clause max scores bound those scores and are rounded up when scaled, so such a document still passes. Finite bounds are unchanged. The soundness is argued, not proved. The code comment in the verifier's diff is loose: a double sum slightly above Float.MAX_VALUE still rounds to MAX_VALUE in the cast, so exceeding MAX_VALUE does not always give +Infinity. The fix needs only the other direction (a +Infinity score means the exact sum is above MAX_VALUE); a tighter comment would read, for example, "A document scores +Infinity only if the sum of its clause scores exceeds Float.MAX_VALUE, so a bound of Float.MAX_VALUE keeps it competitive."

   private static long scaleMinScore(float minScore, int scalingFactor) {
-    assert Float.isFinite(minScore);
+    assert Float.isNaN(minScore) == false;
     assert minScore >= 0;
+    // A float sum becomes +Infinity once its exact value exceeds Float.MAX_VALUE, so a document
+    // scoring +Infinity only guarantees that the sum of its clause scores is above MAX_VALUE.
+    minScore = Math.min(minScore, Float.MAX_VALUE);

Trade-offs

Once the bound is +Infinity, WAND keeps candidates whose max scores reach Float.MAX_VALUE instead of none, and the collector discards the finite ones; only such rare searches pay for that.

What the checks validated

• Stock 645d4fe14a20: the repro fails with assertions on and off.
• With the fix: the repro passes with assertions on and off; TestWANDScorer with nightly tests passes (the gradle log shows 15 tests; its saved summary lists all 15, 0 skipped, including testRandomWithInfiniteMaxScore and testRandomWithMaxScoreOverflow); the core org.apache.lucene.search.* tests plus TestFeatureField and TestFeatureSort pass (the gradle log shows 2,360 tests, 49 skipped; the saved summary adds 217 classes and 0 failures; the summaries were written from the scratch worktree's JUnit reports before it was removed); :lucene:core:check -x test (google-java-format, ecj lint, forbidden APIs, license checks) passes with the repro test in place.
• With the fix shadowed in the standalone runner: the plain-search probe (1,010 documents) and the concurrent test pass with assertions off; in the study the fix also passed the MUST_NOT-route test, a scorer-level probe, the first repro, and, as a one-line clamp in the release sources, the 8.0.0 and 8.4.0 ports.
• Not run: the full core test suite; x86.

return Math.min((long) Math.floor(scaled), MAX_SCALED_SCORE); was the first idea. When the clause max scores sum past Float.MAX_VALUE, the scaling factor makes MAX_SCALED_SCORE stand for about 2 x Float.MAX_VALUE, so a document with two clauses of 2e38 is still pruned.

Trade-offs

It is incomplete: a MUST_NOT-route test and a scorer-level probe still fail with it.

What the checks validated

Run in the study: the concurrent repro passes; the MUST_NOT test and the scorer probe fail.

TopFieldCollector and TopScoreDocCollector would skip setMinCompetitiveScore when the bound is infinite.

Trade-offs

Four call sites; custom collectors stay exposed, since the Scorable contract allows any non-NaN bound; an all-+Infinity top k loses pruning.

Clamp scores where they are produced (for example in WANDScorer.score()), or document +Infinity as invalid.

Trade-offs

Changes ranking semantics (+Infinity hits would tie with Float.MAX_VALUE hits); a javadoc change alone leaves the AssertionError reachable through the stock collectors.

Method: semi-formal (the finder's label): a hypothesis formed while modelling, then witnessed by a tool.

• The hunt unit modelled the WAND scaled-integer rejection test with a Z3 lemma split and found no counterexample for a finite minimum competitive score under its stated preconditions: the lemmas are UNSAT for 13 sampled scaling factors of the reachable -105 to 173, the two edge factors are argued by hand, two rounding facts are assumed, and the end-to-end queries did not finish. The split needs "minScore finite", which scaleMinScore asserts.
• Reading the callers showed that TopScoreDocCollector passes nextUp(+Infinity) and the raw cross-slice bound; the signal came from code reading while modelling, not from the solver.
• An executable probe, then a deterministic JUnit test on the stock jar, witnessed it. Independent verifiers, cross-model reviewers (OpenAI GPT-5.6) and an adjudication then reproduced it with their own tests; the history step found the single-threaded sort route used by the minimal repro.