Skip to content

Tags: GrigoryEvko/z3

Tags

v2026.03.24.2

Toggle v2026.03.24.2's commit message
z3-iprit v2026.03.24.2 — 11,903/11,911 @15s (99.93%), 0 unknowns

New fixes: t154 relevancy/case-split guard, VMTF cycle, ARR-5/ARR-6 revert, lazy=24
G5 adaptive eager reverted (caused 22 regressions)

v2026.03.24.1

Toggle v2026.03.24.1's commit message
z3-iprit v2026.03.24.1 — 11,900/11,911 @15s, 0 unknowns

Fixes: VMTF cycle (+6), ARR-5/ARR-6 revert, lazy_threshold 24, I1 cache, D9 flattening

v2026.03.24

Toggle v2026.03.24's commit message
z3-iprit v2026.03.24

Results: 11,897/11,911 @15s (99.88%), 11,901/11,911 @120s (99.92%)
Zero unknowns. Only genuine timeouts remain.

Key changes since last tag:
- Fix I1 persistent rewrite cache stale elim_and bug (root cause of OrdSet-35)
- Fix D9 mk_and_as_or OR flattening bypass
- Raise QI lazy_threshold 20→25 (solves ModifiesGen-171)
- Solver driver with SPSA + landscape map
- Deferred landscape collection (zero overhead <5000 conflicts)

z3-4.15.8

Toggle z3-4.15.8's commit message
update release to dedup and include manylinux

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

Nightly

Toggle Nightly's commit message
fix the logic of adding all coefficients and blocking double insertio…

…ns in m_todo

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

z3-4.15.7

Toggle z3-4.15.7's commit message
Revert "mpz: use pointer tagging to save space (Z3Prover#8447)"

This reverts commit 2f4abe2.

z3-4.15.6

Toggle z3-4.15.6's commit message

Verified

This commit was created on GitHub.com and signed with GitHub’s verified signature.
Update RELEASE_NOTES.md for version 4.15.6

Added release notes for version 4.15.6, including optimizations and fixes.

z3-4.15.5

Toggle z3-4.15.5's commit message

Verified

This commit was created on GitHub.com and signed with GitHub’s verified signature.
Update RELEASE_NOTES.md for version 4.15.5

Removed several outdated features and added new functionalities across various APIs, including improvements for TypeScript, Java, and C++ bindings. Updated release notes for version 4.15.5 to reflect these changes.

z3-4.15.4

Toggle z3-4.15.4's commit message
update release notes

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

z3-4.15.3

Toggle z3-4.15.3's commit message
enable pypi public

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>