Formal models and scripts: study-simd-equivalence
Tools: SMT-LIB (Z3/cvc5), 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
- Doc-values range queries with a skip index return wrong hits when a segment's values span more than Long.MAX_VALUE (finding LFV-044; repro · finding page)
- Panama minMaxScalarQuantize rounds differently from the default implementation at one boundary value (finding LFV-071; repro · finding page)
Files
smt/byte_kernels.pysmt/byte_kernels_comp.pysmt/dv_fix_check.pysmt/dv_gcd1_classify.pysmt/dv_gcd_transform.pysmt/dv_gcd_transform_int.pysmt/int4_kernels.pysmt/int4bit_abstract.pysmt/misc_kernels.pysmt/mutation_checks.pysmt/quantize_round_fp.pysmt/vecsem.pysmt/obligations/mut_int4DotProductBothPacked_VB128_n32.smt2smt/obligations/mut_int4DotProductBothPacked_VB128_n33.smt2smt/obligations/mut_int4DotProductBothPacked_VB256_n32.smt2smt/obligations/mut_int4DotProductBothPacked_VB256_n33.smt2smt/obligations/mut_int4DotProductBothPacked_VB256_n64.smt2smt/obligations/mut_int4DotProductBothPacked_VB512_n32.smt2smt/obligations/mut_int4DotProductBothPacked_VB512_n33.smt2smt/obligations/mut_int4DotProductBothPacked_VB512_n64.smt2smt/obligations/mut_int4DotProductSinglePacked_VB128_n32.smt2smt/obligations/mut_int4DotProductSinglePacked_VB128_n33.smt2smt/obligations/mut_int4DotProductSinglePacked_VB256_n32.smt2smt/obligations/mut_int4DotProductSinglePacked_VB256_n33.smt2smt/obligations/mut_int4DotProductSinglePacked_VB256_n64.smt2smt/obligations/mut_int4DotProductSinglePacked_VB512_n32.smt2smt/obligations/mut_int4DotProductSinglePacked_VB512_n33.smt2smt/obligations/mut_int4DotProductSinglePacked_VB512_n64.smt2smt/obligations/mut_int4DotProduct_VB128_n32.smt2smt/obligations/mut_int4DotProduct_VB128_n33.smt2smt/obligations/mut_int4DotProduct_VB256_n32.smt2smt/obligations/mut_int4DotProduct_VB256_n33.smt2smt/obligations/mut_int4DotProduct_VB256_n64.smt2smt/obligations/mut_int4DotProduct_VB512_n32.smt2smt/obligations/mut_int4DotProduct_VB512_n33.smt2smt/obligations/mut_int4DotProduct_VB512_n64.smt2smt/obligations/mut_int4SquareDistanceBothPacked_VB128_n32.smt2smt/obligations/mut_int4SquareDistanceBothPacked_VB128_n33.smt2smt/obligations/mut_int4SquareDistanceBothPacked_VB256_n32.smt2smt/obligations/mut_int4SquareDistanceBothPacked_VB256_n33.smt2smt/obligations/mut_int4SquareDistanceBothPacked_VB256_n64.smt2smt/obligations/mut_int4SquareDistanceBothPacked_VB512_n32.smt2smt/obligations/mut_int4SquareDistanceBothPacked_VB512_n33.smt2smt/obligations/mut_int4SquareDistanceBothPacked_VB512_n64.smt2smt/obligations/mut_int4SquareDistanceSinglePacked_VB128_n32.smt2smt/obligations/mut_int4SquareDistanceSinglePacked_VB128_n33.smt2smt/obligations/mut_int4SquareDistanceSinglePacked_VB256_n32.smt2smt/obligations/mut_int4SquareDistanceSinglePacked_VB256_n33.smt2smt/obligations/mut_int4SquareDistanceSinglePacked_VB256_n64.smt2smt/obligations/mut_int4SquareDistanceSinglePacked_VB512_n32.smt2smt/obligations/mut_int4SquareDistanceSinglePacked_VB512_n33.smt2smt/obligations/mut_int4SquareDistanceSinglePacked_VB512_n64.smt2smt/obligations/mut_int4SquareDistance_VB128_n32.smt2smt/obligations/mut_int4SquareDistance_VB128_n33.smt2smt/obligations/mut_int4SquareDistance_VB256_n32.smt2smt/obligations/mut_int4SquareDistance_VB256_n33.smt2smt/obligations/mut_int4SquareDistance_VB256_n64.smt2smt/obligations/mut_int4SquareDistance_VB512_n32.smt2smt/obligations/mut_int4SquareDistance_VB512_n33.smt2smt/obligations/mut_int4SquareDistance_VB512_n64.smt2
How to run
- SMT-LIB:
z3 <file>.smt2orcvc5 <file>.smt2(satwith a model is a counterexample where the query asks for one). - Python:
python3 <file>.py; scripts that importz3need thez3-solverpackage.
Snapshot of 2026-11-03. AI-assisted; not yet triaged by a human Lucene committer. Feedback: open an issue in lucene-ai-bug-hunt.