Commits

Commit history

1. Commits on Nov 10, 2026

   • Remove timing-out arithmetic alias SAT control

     Show description for 145c0c5
     

     NikolajBjorner

     and

     Copilot

     committed
     145c0c5View commit details

     Copy full SHA for 145c0c5

     Browse repository at this point

   • Handle canceled model searches in Spacer global subsumption (#11635)

     Show description for 4903f69
     

     Copilot

     and

     NikolajBjorner

     authored
     4903f69View commit details

     Copy full SHA for 4903f69

     Browse repository at this point

   • Handle dual polarity for generated universal quantifiers (#11644)

     Show description for 1449270
     

     NikolajBjorner

     and

     github-actions[bot]

     authored
     1449270View commit details

     Copy full SHA for 1449270

     Browse repository at this point

   • Fix NFV admission scope and expose API-denial diagnostics (#11642)

     Show description for 18bce2b
     

     shuvendu-lahiri

     and

     Copilot

     authored
     18bce2bView commit details

     Copy full SHA for 18bce2b

     Browse repository at this point

   • Revert "Handle quantifier polarity during SMT internalization (#11562)" (#11638)

     Show description for 1e136dc
     

     NikolajBjorner

     and

     github-actions[bot]

     authored
     1e136dcView commit details

     Copy full SHA for 1e136dc

     Browse repository at this point

   • Merge branch 'master' of https://github.com/z3prover/z3

     NikolajBjorner

     committed
     8927ff9View commit details

     Copy full SHA for 8927ff9

     Browse repository at this point

   • updated version

     Show description for 3660f20
     NikolajBjorner

     committed
     3660f20View commit details

     Copy full SHA for 3660f20

     Browse repository at this point

   • Make native checker regressions independent of proof search and Skolem numbering

     Show description for 16291f1
     

     NikolajBjorner

     and

     Copilot

     committed
     16291f1View commit details

     Copy full SHA for 16291f1

     Browse repository at this point

   • F*: replay guarded integer and real product equality clauses (#11629)

     Show description for cb384b2
     

     3 peopleauthored
     cb384b2View commit details

     Copy full SHA for cb384b2

     Browse repository at this point

   • Upgrade NFV: one advisory audit per ready PR (#11630)

     Show description for 0dc62b0
     shuvendu-lahiri

     authored
     0dc62b0View commit details

     Copy full SHA for 0dc62b0

     Browse repository at this point

   • Update 5.4.0 release notes for recent fixes and proof checking

     Show description for d6c9b4f
     

     NikolajBjorner

     and

     Copilot

     committed
     d6c9b4fView commit details

     Copy full SHA for d6c9b4f

     Browse repository at this point

   • F*: extend verified arithmetic proof replay (#11618)

     Show description for 5db0b4c
     

     3 peopleauthored
     5db0b4cView commit details

     Copy full SHA for 5db0b4c

     Browse repository at this point

   • Prevent model evaluator loops when merging division guards (#11620)

     Show description for 0973684
     

     4 peopleauthored
     0973684View commit details

     Copy full SHA for 0973684

     Browse repository at this point
2. Commits on Nov 9, 2026

   • Certify scripts with print-only and optimization commands, more distincts, and deep ite chains in Lean (#11623)

     Show description for 13423e3
     levnach

     authored
     13423e3View commit details

     Copy full SHA for 13423e3

     Browse repository at this point

   • Make unsupported and unsafe proof tactics no-ops (#11547)

     Show description for 8100da1
     

     3 peopleauthored
     8100da1View commit details

     Copy full SHA for 8100da1

     Browse repository at this point

   • Handle empty inputs in Z3Py pseudo-Boolean constraints (#11621)

     Show description for 7e6d08e
     

     Copilot

     and

     NikolajBjorner

     authored
     7e6d08eView commit details

     Copy full SHA for 7e6d08e

     Browse repository at this point

   • Disable eq2bv when recursive definitions exist (#11622)

     Show description for 7c24939
     

     Copilot

     and

     NikolajBjorner

     authored
     7c24939View commit details

     Copy full SHA for 7c24939

     Browse repository at this point

   • docs: record shared-step NNF proof checking design

     Show description for 3aead9c
     NikolajBjorner

     committed
     3aead9cView commit details

     Copy full SHA for 3aead9c

     Browse repository at this point

   • Fix datatype occurs checks through nested containers (#11597)

     Show description for 532cbc4
     

     4 peopleauthored
     532cbc4View commit details

     Copy full SHA for 532cbc4

     Browse repository at this point

   • Preserve maximal lower bounds in arithmetic conjunction rewriting (#11604)

     Show description for 89520c1
     

     3 peopleauthored
     89520c1View commit details

     Copy full SHA for 89520c1

     Browse repository at this point

   • Fix Spacer root lifetime across repeated fixedpoint queries (#11605)

     Show description for b2daca7
     

     Copilot

     and

     NikolajBjorner

     authored
     b2daca7View commit details

     Copy full SHA for b2daca7

     Browse repository at this point

   • Fix comparisons of overlapping algebraic roots (#11599)

     Show description for f16c6ce
     

     3 peopleauthored
     f16c6ceView commit details

     Copy full SHA for f16c6ce

     Browse repository at this point
3. Commits on Nov 8, 2026

   • F*: stabilize Pulse verification under the current solver and preserve alias regression checks (#11612)

     Show description for 8573212
     

     NikolajBjorner

     and

     github-actions[bot]

     authored
     8573212View commit details

     Copy full SHA for 8573212

     Browse repository at this point

   • F*: certify Real order and guarded Int division; make LP decoding stack-safe (#11606)

     Show description for ff86ba7
     NikolajBjorner

     authored
     ff86ba7View commit details

     Copy full SHA for ff86ba7

     Browse repository at this point
4. Commits on Nov 7, 2026

   • Certify arrays of enumerations, constant-array rewrites, and distincts of more than 32 terms in Lean (#11602)

     Show description for aa82260
     

     levnach

     and

     claude

     authored
     aa82260View commit details

     Copy full SHA for aa82260

     Browse repository at this point

   • Guard sequence nth equation decomposition by index bounds (#11549)

     Show description for a0d488d
     

     3 peopleauthored
     a0d488dView commit details

     Copy full SHA for a0d488d

     Browse repository at this point

   • Fix iterator invalidation in datatype subterm merges (#11598)

     Show description for effa86a
     

     3 peopleauthored
     effa86aView commit details

     Copy full SHA for effa86a

     Browse repository at this point

   • Handle quantifier polarity during SMT internalization (#11562)

     Show description for 6df87c1
     

     4 peopleauthored
     6df87c1View commit details

     Copy full SHA for 6df87c1

     Browse repository at this point

   • Update README to require fixes and tests for fuzz bugs

     Show description for 840eedc
     NikolajBjorner

     authored
     840eedcView commit details

     Copy full SHA for 840eedc

     Browse repository at this point

   • Fix length-constrained models for nested sequence elements (#11550)

     Show description for d86b80e
     

     3 peopleauthored
     d86b80eView commit details

     Copy full SHA for d86b80e

     Browse repository at this point

   • Fix incorrect ITE-sum optimization bounds and model reconstruction (#11585)

     Show description for f706941
     

     3 peopleauthored
     f706941View commit details

     Copy full SHA for f706941

     Browse repository at this point

   • Upgrade NFV reviewer for bounded report publication (#11596)

     Show description for afdede3
     

     shuvendu-lahiri

     and

     Copilot

     authored
     afdede3View commit details

     Copy full SHA for afdede3

     Browse repository at this point

   • Enforce proof contracts for custom simplifier pipelines (#11533)

     Show description for 6e215a1
     

     NikolajBjorner

     and

     github-actions[bot]

     authored
     6e215a1View commit details

     Copy full SHA for 6e215a1

     Browse repository at this point

   • Keep bit-vector pretty printing SMT-LIB compliant (#11551)

     Show description for 2c4570f
     

     4 peopleauthored
     2c4570fView commit details

     Copy full SHA for 2c4570f

     Browse repository at this point
5. Commits on Nov 6, 2026

   • Certify enumeration datatypes in Lean through the clause log (#11592)

     Show description for a807093
     

     levnach

     and

     claude

     authored
     a807093View commit details

     Copy full SHA for a807093

     Browse repository at this point