SpanNotQuery with a negative post (or dist) drops every include span after the one that uses up a document's exclude spans, because NO_MORE_POSITIONS - post overflows int

SpanNotQuery(include, exclude, pre, post) keeps the include spans that no exclude span overlaps within pre tokens before or post tokens after, and its javadoc says negative values "allow a certain amount of overlap to occur". Read as a window, a negative post can only keep more spans than post = 0. In fact it keeps fewer: once checking one include span has moved the exclude cursor past the document's last exclude span, the cursor reads NO_MORE_POSITIONS (Integer.MAX_VALUE), and for every later include span SpanNotQuery.java:210 computes excludeSpans.startPosition() - post, which wraps to a negative int for any post < 0. On "b a a c", spanNot(a, b, 0, -1) returns [1,2) instead of [1,2), [2,3), and spanNear([spanNot(a, b, 0, -1), c], 0, true) no longer matches. With ordinary negative values a top-level SpanNotQuery keeps its document set but loses spans and score; nested in a positional query it loses documents. The line came from LUCENE-8034 (7.2.0), which fixed the opposite overflow for a huge positive post; every release from 7.2.0 to 10.6.0 (10.6.0 by reading) and main is affected. Lucene's query parsers always pass 0 and cannot reach it.

• Span: a match of a span query inside one document, written [start,end) in token positions. In "b a a c" the term "a" has the spans [1,2) and [2,3).
• SpanNotQuery(include, exclude, pre, post): keeps the include spans that no exclude span overlaps within pre tokens before or post tokens after. A negative post (or dist, which sets both) allows that much overlap (SpanNotQuery.java:51-66), so, read as a window, it can only keep more.
• NO_MORE_POSITIONS: Integer.MAX_VALUE (Spans.java:32). After the last span of the current document, a Spans iterator's startPosition() and endPosition() return it (Spans.java:34-51).

SpanNotWeight#getSpans wraps the include spans in a FilterSpans whose accept(candidate) runs once per include span, in position order (SpanNotQuery.java:166-216 on main a9779ef3c193):

1. It catches the exclude cursor up to the candidate's document and, if the cursor has not yet started in this document, moves it to its first span (:175-200).
2. It skips exclude spans that end before the candidate starts (:202-207). If that runs out of exclude spans, it accepts the candidate: return AcceptStatus.YES; // no more exclude at current doc. (:205). The cursor stays on the document, now reading NO_MORE_POSITIONS.
3. Otherwise it checks the next exclude span's start: if (excludeSpans.startPosition() - post >= candidate.endPosition()) return YES; else return NO; (:210-214).
4. For the next include span of the same document, step 2 does nothing (2147483647 <= candidate.startPosition() - pre is false for any ordinary pre) and step 3 computes 2147483647 - post. With post = 0 that is 2147483647 and the span is kept; with post = -1 it is 2^31, which wraps to -2147483648, and -2147483648 >= 3 is false: rejected. Every negative post wraps, because indexed positions are at most Integer.MAX_VALUE - 128 (IndexWriter.java:211).
5. FilterSpans then asks for the next include span (FilterSpans.java:83-96), which is rejected the same way: every later include span of the document is gone. The next document starts fresh.

The wrap can only reject, never accept, and the include span that used up the exclude spans is itself accepted, so with ordinary negative values a top-level SpanNotQuery keeps its document set. The trigger is a negative post: in a bounded enumeration with pre and post in -2..2, a negative pre with post >= 0 gave 0 mismatches. Windows of about 2^31 tokens hit related corners: post = Integer.MAX_VALUE compares against the sentinel without wrapping and drops the same span, and post = Integer.MIN_VALUE also wraps on real positions, where even a top-level document is lost.

On "b a a c": spanNot(a, b, 0, 0) gives [1,2), [2,3); spanNot(a, b, 0, -1) and new SpanNotQuery(a, b, -1) give [1,2); spanNear([spanNot(a, b, 0, -1), c], 0, true) counts 0 instead of 1. On "b a a c b" the same query gives both spans. On "x y y y y y", spanNot(y, x, 0, post) keeps 1 of 5 "y" for post -1, -2 and -3 and all 5 for 0 and 1. A two-phase exclude (spanNear([b, x], 0, true)) is affected too. Every document over {a, b} of 1 to 5 tokens, pre and post in -2..2: 260 mismatches in 6,450 include-span checks, all with post < 0 after the exclude spans were used up.

• Who. Java code that calls the 4-argument constructor with post < 0 or the 3-argument constructor with dist < 0, both documented as allowed overlap (SpanNotQuery.java:51-66); rewrite keeps the values (:230). Default codec, IndexWriterConfig and searcher (the executed main() port) and randomized test codecs (the JUnits), assertions on or off, any index size.
• When. A document has an exclude match before two or more include matches and no exclude match after the include match that uses them up. Ordinary text does this.
• Top-level query (ordinary negative values). The same documents match, but spans, Matches positions, span frequency and scores are wrong: in one probe 11 of 57 documents score lower with 57 = 57 hits; in another "b a a c" scores 0.053059246 instead of 0.070576414 with 4 = 4 hits; Matches reports 1 position instead of 2.
• Nested query. In spanNear or spanPositionRange, whole documents stop matching (executed).
• Under a negation. A MUST_NOT over spanNear([spanNot(a, b, 0, -1), c], 0, true) keeps "b a a c" ([0, 1] instead of [1]); the same with dist = -1; spanNot(a, spanNot(a, b, 0, -1)) returns [0] instead of [] (executed on main, 10.5.2 and 9.12.3; all pass with the fix).
• Highlighting. WeightedSpanTermExtractor iterates the same spans, so the span highlighter would mark fewer occurrences (read, not executed).
• Not reachable through Lucene's query parsers: the XML SpanNotBuilder and ComplexPhraseQueryParser use the 2-argument constructor (SpanNotBuilder.java:45, ComplexPhraseQueryParser.java:359, 417).
• Cost. Deterministic, per document; no hang or resource blow-up was observed: the filter stays linear and emits fewer spans (one "b" then 50,000 "a": 1 span, milliseconds).
• Why the tests miss it. No deterministic upstream negative-window test has an include span after the exclude spans are used up (the randomized TestSpanSearchEquivalence uses the 2-argument constructor).

# Lucene main 645d4fe14a20, assertions on (-ea), seed DEADBEEF: 1 test(s) run, 1 failed
    => java.lang.AssertionError: expected:<[[1,2), [2,3)]> but was:<[[1,2)]>
       org.junit.Assert.fail(Assert.java:89)
       org.junit.Assert.failNotEquals(Assert.java:835)
       org.junit.Assert.assertEquals(Assert.java:120)
       org.junit.Assert.assertEquals(Assert.java:146)
       org.apache.lucene.queries.spans.TestSpanNotNegativePost.testNegativePostKeepsSpansAfterLastExclude(TestSpanNotNegativePost.java:56)

• The contract. SpanNotQuery.java:51-56 (3-argument): "matching spans from include which have no overlap with spans from exclude within dist tokens of include. Inversely, a negative dist value may be used to specify a certain amount of allowable overlap." :61-66 (4-argument): "... within pre tokens before or post tokens of include. Inversely, negative values for pre and/or post allow a certain amount of overlap to occur."
• A deliberate feature. lucene/CHANGES.txt:8710-8712 (6.4.0): "LUCENE-7431: Allow a certain amount of overlap to be specified between the include and exclude arguments of SpanNotQuery via negative pre and/or post arguments." That change removed the earlier clamping of negative values to 0.
• Lucene's own tests use it. TestBasics#testSpanNotWindowNegPost (TestBasics.java:331-352) asserts that post = -1 keeps the 16 hits that testSpanWithMultipleNotSingle (:244) asserts for post = 0, and that post = -2 adds two more; testSpanNotWindowNegPre (:354-375) does the same for pre (-2 keeps the 16, -3 adds the two).
• History. Until 7.1.0 the check was candidate.endPosition() + post <= excludeSpans.startPosition(), correct for any post <= 0; 7.1.0 returns both spans (executed). LUCENE-8034 (#9082) turned it into the subtraction only to fix an overflow for a huge positive post; its discussion never mentions negative post, and its test uses pre = post = Integer.MAX_VALUE (TestBasics.java:232).
• Order dependence. The same include span is kept or dropped depending on whether an earlier include span used up the exclude spans, and an extra exclude match after it restores it.

The strongest works-as-designed case, from the intended-behaviour verifier, a reviewer from another model family (OpenAI GPT-5.6) and the adjudication: testSpanNotWindowNegPost carries the comment "test handling of invalid window < 0" (TestBasics.java:332), so negative windows might be invalid input; SpanNotWeight is @lucene.internal (SpanNotQuery.java:125); no javadoc says what happens after the exclude spans run out; and no bundled parser can produce the trigger.

Why it fails: the comment predates LUCENE-7431, when the test was testSpanNotWindowNeg and the constructor clamped negative values to 0; LUCENE-7431 renamed the test and made it assert that negative windows widen the hits, but kept the comment. The constructors are public and documented; only the weight is internal. Under the window reading that LUCENE-7431's tests assert, the javadoc is monotone (a more negative post never removes spans), and Spans documents the sentinel that accept itself reads. A documented input that only Java callers can pass is still a legitimate trigger. Every verifier and the adjudication rejected the intended argument; the cross-model reviews rated it weak. Open issue #16820 proposes deprecating span queries, which could argue for won't-fix but not for intended behaviour.

Two options were applied in a scratch worktree at a9779ef3c193 and run through gradle (seed DEADBEEF), with the compact repro and a 24-case window probe that compares spanNot(a, b, pre, post) with the javadoc rule on "b a a c", "a b" and "b a a c b" (stock main: 7 mismatches); the third option was not run. A diff with the recommended fix and the repro as a new test is attached (fix-with-test.diff).

In accept, right after the exclude cursor is initialised (SpanNotQuery.java:198-200), return YES when excludeSpans.startPosition() == NO_MORE_POSITIONS: an earlier candidate used up the exclude spans of this document, so nothing can exclude this one. Also make line 210 overflow-safe with a long subtraction. +5/-1 lines.

           if (excludeSpans.startPosition() == -1) { // init exclude start position if needed
             excludeSpans.nextStartPosition();
           }
 
+          if (excludeSpans.startPosition() == NO_MORE_POSITIONS) {
+            return AcceptStatus.YES; // an earlier candidate used up the exclude spans of this doc
+          }
+
           while (excludeSpans.endPosition() <= candidate.startPosition() - pre) {
@@
-          if (excludeSpans.startPosition() - post >= candidate.endPosition()) {
+          if ((long) excludeSpans.startPosition() - post >= candidate.endPosition()) {

Trade-offs

• One int comparison for each include candidate that gets past the document check at :194-196, whether it is then accepted or rejected; no benchmark run.
• The check makes the result independent of post once the exclude spans of the document are used up, including post = Integer.MAX_VALUE; the long comparison keeps LUCENE-8034's protection for a huge positive post and also covers a huge negative post on real positions.
• Not covered and not examined: the loop condition at :202 still computes candidate.startPosition() - pre in int, so an extreme negative pre (about -2^31) is not made safe.

What the checks validated

• Stock main a9779ef3c193: the repro fails through gradle with assertions on and off.
• With the fix: the repro and the window probe pass with assertions on and off (24 of 24 cases).
• With the fix, all of lucene/queries passes (53 classes, 514 tests, 5 skipped), including the 22 upstream span classes (232 tests; TestBasics 29 of 29 with testSpanNotNoOverflowOnLargeSpans and testSpanNotWindowNegPost), and all of lucene/highlighter (34 classes, 722 tests); ecjLint and checkGoogleJavaFormat pass for queries.
• Through the classpath runner the repro passes with the fix shadowed, and the probe passes 24 of 24 with -ea and -da.
• Not run: the full Lucene test suite; no benchmark.

if ((long) excludeSpans.startPosition() - post >= candidate.endPosition()) at SpanNotQuery.java:210.

-          if (excludeSpans.startPosition() - post >= candidate.endPosition()) {
+          if ((long) excludeSpans.startPosition() - post >= candidate.endPosition()) {

Trade-offs

It still compares against the sentinel as if it were a real position, so post = Integer.MAX_VALUE with pre = 0 still drops the later span once the exclude spans are used up (1 of the probe's 24 cases). That needs a window of 2^31 - 1 tokens.

What the checks validated

• This doc, gradle at a9779ef3c193: the repro passes; the window probe fails 1 of 24 cases (post = Integer.MAX_VALUE, pre = 0 on "b a a c": [1,2) instead of both).
• The hunt (classpath runner, main ea57360912ed): the finder's, the independent reproducer's (0 of 6,450 enumeration mismatches) and the intended-lens reviewer's tests and the negated-shape probe pass, as do 156 upstream span tests in 9 classes, including testSpanNotNoOverflowOnLargeSpans and testSpanNotWindowNegPost (that run also shadowed six interval fixes from the same hunt unit; its one failure in 273 tests is the interval test TestDisjunctionRewrites#testNotContainedBy, which asserts a rewrite form one of those fixes changes).

(long) candidate.endPosition() + post <= excludeSpans.startPosition().

Trade-offs

Equivalent to the one-line long option, with the same sentinel corner.

Method: bounded-exhaustive translation validation on the stock jar (semi-formal tier), in a hunt unit on span and interval queries.

• The harness evaluates the span filters of the real main jars on every document of up to 3 positions over {a, b, c}, with SpanNotQuery pre and post in -1..1 over 30 child queries, and compares each result with an exact reference built from the children's actual Lucene spans and the javadoc semantics.
• The SpanNot relation failed in 636 of 510,300 checks, all with post = -1, and in 0 of 12,425,400 checks with the unit's fix sketches shadowed onto the jar (larger scopes, run on separate build machines).
• The root cause was then read from SpanNotQuery.java:210 and reduced to a public-API JUnit. No model checker, SMT solver or prover was involved.
• Found 2026-10-26 on main ea57360912ed; then checked by an independent reproducer, reviews by a model from another family (OpenAI GPT-5.6), an intended-behaviour devil's advocate, an adjudication, a history and prior-report follow-up, and a credibility audit.