Unclaimed project
Are you a maintainer of z3 ? Claim this project to take control of your public changelog and roadmap.
Claim this project Changelog
z3 The Z3 Theorem Prover
© 2026 AnnounceHQ. All rights reserved.
New October 29, 2025
z3-4.15.4 Changes:
745087e237e669d709ae35694728a0c479e572b3 update release notes
c88295a7c76cc62cf5a994c53d39766cc479abec fix C++ example and add polymorphic interface for C++
6efffa00548043d984b5e664d6076e40dac201a3 renemable Centos AMD nightly
1b9a6369107f6dd8ec2070f0edf9d90b45aa3ba0 fix build break introduced when adding support for polymorphic datatypes
88fcc05d6c17155a61517928ba6797f91e507de9 Bump actions/upload-artifact from 4 to 5 (#7998)
488c712f5b9891198542ccbfd02657964ed91cd0 Bump actions/download-artifact from 5 to 6 (#7999)
3570073c29382ef9ab8b1abc46622155edc631d2 Add missing mkLastIndexOf method and CharSort case to Java API (#8002)
b6e3a688390be425713d96ef41c9de0ac83dfbc4 update centos version
766eaa3376ae53fe451148590cc3d50f6f6381be disable centos build until resolved
efd5d04af50b5dc0a2203f59bb5b159101a964f1 enable always add all coeffs in nlsat
See More
887ecc0c98345533ab1ba28003d4e79fefd351c5 throttle grobner method more actively
58e64ea8264b42feb5a9c824bd4f3944aed65616 try exponential delay in grobner
2bf1cc7d61b3cd967791d7fdbb9790dd97e238e7 Enabling Control Flow Guard (CFG) by default for MSVC on Windows, with options to disable CFG. (#7988)
68a7d1e1b1cbca5796e0cbf647d6a940b08b4cde Bump actions/setup-node from 5 to 6 (#7994)
9a2867aeb7eaefadce0792a4f54f9387a5f66aa2 Add a fast-path to _coerce_exprs. (#7995)
06ed96dbda5ef3adc323ce2b4d3e5cfe13c1963a add the "noexcept" keyword to value_score=(value_score&&) declaration
f2e7abbdc13182c3ba0898f8618659baaa50148a disable manylinux until segfault is resolved
aaaa32b4a0644e6febf6336d1ae4a187ae28a911 build fixes
d65c0fbcd650903b7a13cf7dd8a7fd92b8998410 add explicit constructors for nightly mac build failure
fcc7e0216734bdac1a1f7f371c5d72343d95d08d Update arith_rewriter.cpp
62ee7ccf65d51c304553def478731aa17b848169 Revert "Add finite_set_value_factory for creating finite set values in model …" (#7985)
05ffc0a77be2c565d09c9bc12bc0a35fd61bbe80 Add finite_set_value_factory for creating finite set values in model generation (#7981)
a1792861831973e6cfed98b955f59742b1065be3 restore the method behavior
1921260c424036b40f4fad1eb9a3f171590cdfd3 restore single cell
3b565bb2846f69bf1b3ae5eff297b0771d003892 trim parametric datatype test
5163411f9b90a339167a41fb3d46a4811420a4db Update Z3_mk_datatype_sort API to accept array of sort parameters and add Z3_mk_polymorphic_datatype (#7966)
e669fbe55743517196361f52c16c6b3e002bf3fb Bump github/codeql-action from 3 to 4 (#7971)
641741f3a874130b28cf50a9a07e8bde19a0a855 parameter eval order
8af9a20e01e92523a593cb71776a5fc476463f82 parameter eval order
6a9520bdc263f19171ab3df242b263039b57f077 parameter eval order
8ccf4cd8f77fe9145947613c33657f2b29bdf7f6 parameter eval order
40b980079b6bb8351549a7f2c8557148aa9e54c3 parameter eval order
a41549eee69986b3cede4408f4f416811879bae0 parameter eval order
2b3068d85fc7f23d249537f2dd91e2c0f31d48e3 parameter eval order
3a2bbf4802cf40b97c7340188dfac888c6702691 param eval order
6e52b9584c031c6e6d139669152729da99f2939b param eval
93ff8c76db660cfc3cdcd82f9d29c18c7ef40ebb parameter evaluation order
00f1e6af7ecca97b81490c6c4595da55b9a865d1 parameter eval order
c154b9df9090c8c49e806db74c13d925b8f45e52 param order evaluation
77c70bf81297b681254a5fde93ce58fb1c7ece92 param order
63bb367a10e54316ca2f5da89d7ec5c32f12fc63 param order
e9a2766e6c680361062269322658d7a95e558ce2 remove AI slop
5a9663247b7887d09246bcd6de8c21e3ad86e0c9 fix the order of parameter evaluation
5ae858f66bdba3c5b0a0dd2ce072067d2c49b06e fixing the order
aa5645b54bea707f16935ae8b87b849995ee29fd fixing the order
542e01555081a0966bbd668db8a3582a493c35b4 Remove unused variable 'first' in mpz.cpp
cd1ceb6efeb935963235788529bdd806cce4bceb [WIP] Add a mutex to warning.cpp to ensure that warning messages from different threads don't interfere (#7963)
3ce8aca41108063920d586f8c4693992c7981233 Bump actions/checkout from 4 to 5 (#7954)
c8bdbd2dc4808bce28a075791a098808fc4758a2 remove directory
e137aaa24988b315874fedbfa0e512fcf89ef463 add user propagators to opt_solver
0e6b3a922acc249e2c26c24b3e4b2bc130f325c1 Add commands for forcing preferences during search
5d8fcaa3ee3d0d532a322c20f1fa99d9ef0e2bb2 update clang format
72c89e1a4e188c7bd07747853b526539ff307105 fix #7952 - make auto-selector detect large bit-vectors so it does't use the datalog engine for hopelessly large tables
0881a71ed234f3da155a7d0967831a987035fa99 update format
65c9a18c3a5b71d382a4fec71b17708ff6a00f50 fix #7956
339f0cd5f93c8d5c3ee5da7fee4cbe73ab914eb2 Correctly distinguish between Lambda and Quantifier in Z3 Java API (#7955)
253a7245d0aeb129f5823fe3a62e1292ea4222af add analysis
b5f79da76a3f5c6606553e217bc351d31aeec604 add analysis
ae55b6fa1efbdfadca9bb9251f8c710279b73429 add analysis
bda98d8da4453e6d6ccf9484879a636f0806cd63 fix #7948
b7eb21efedfbf691cbd1928c5f06af689ba1ed65 fix #7948
391880b6fcef2e8cb7a7a8dc0deb7533525b1a2a Add missing ::z3::sdiv to z3++.h (#7947)
6173a0d025eeb364159b538dfb7b2005bfd4e537 propagate value initialization to atoms
eae4de075bb8e32b6c9963078af95c2049fcfe61 fix latent bug in factorization
04ddade2ddd6b9791a58aac1aa17791d5f6b742f remove stale comment
f5c28a0b76a57c918a154709d7e2665fa867fe3c household cleanup
e26f7b900cdd81103bfc1846f40aa54c8e169a69 fix unsound axiom for lower-bounding
dcdae5a61c39898425673df7b7f071622058a97e add smt debug output for nla_core
ce53e06e29433cdc511656691d79c9d6b7634a31 Par (#7945)
2b5b9854925b0fe1466c7ee4ac80f49b497a7778 fix divergence regression
9876e85a45794e02e165cb72c736b9640d35ce96 turn on max of sums transformation
3256d1cc8b0100a09e83e8023cb66891462f818e fix bug in unit test
0e8648c7d74da0355230707856a0c9ffa157cc98 fix compile of lp.cpp
a8ae52bfbf59e8e4a76116cc4ee2161ad282d95c fix missing call change to cross-nested. Prepare for lower-bound and upper-bound cardinality constraints
2517b5a40a0a338138c4994608391f9b8c330729 port improvements from ilana branch to master regarding nla
5d91294e9078902c40989a973080e3793ee44ffe update workflows
59bd1cf4a0d6ef43e513f24d553d1bb2787b48bc updated clang format
b17df988ed1adbc1722a4fbfed01fd52c92ca236 Daily Test Coverage Improver: Add comprehensive API special relations tests (#7925)
3fa34952f07819cc2c2904361066095e79542b36 Daily Backlog Burner: Fix bad .dylib versioning in pip packages (#7914) [ #6651 ]
c43cb18e63c53189dbcd3799a135501794fcb05e better rewriting
37904b9e851e928cfa7bd391781811ea3021e6e9 fix the parameter evaluation order
cda0a922b9aa08b7a1c375ae4324e22cbbc19c17 Daily Test Coverage Improver: Add comprehensive API polynomial tests (#7905)
82ab6741a02598d2e8b615a84f9a05f7b315168f Daily Test Coverage Improver: Add comprehensive API pseudo-boolean constraint tests (#7898)
222c64fa6f20811474643fbe86fa591177e827ac Remove Windows-only guard from hashtable unit tests (#7901) [ #1163 ]
635d3b701739be771726e3ffff048ad5821ed0b0 Add .clang-format file for C++ code formatting (#7904) [ #1441 ]
1b058f23e9f2d053bbc29018d47a8cad16abc147 Daily Backlog Burner: Add include directory for easier Z3 integration (#7907) [ #1664 ]
4e1a9d1ef7077acd86fd5d4ef21129d573dd7fc7 Daily Test Coverage Improver: Add comprehensive API Datalog tests (#7921)
7cb491dd6a15dd59cd228ce2d47d262cfa8668e0 update compiled workflows
d989bcaebea8dbdae8099be70f63a9d811df0af5 update compiled workflows
f300dfc425e08a565f7362f3fc6e5aaa80462ea5 recompile improvers
2d0b9e69720bdc97ab423bdc3741e7096455ebae recompile improvers
aabdb407d10cc4f470a24554ac7504f9031aac14 latest improvers
2364ea42ba285de52803c8090708986b7323c743 update improvers
7268136bb6c3a23091dad3fce9883e1fabd0314f update workflows
db8206d2655cc7bafc249b04978803ff22f308d3 improve improvers
5b70f75d89d20e2ada9f319fb17ecfa920da115e allow burner to create PRs
81da4be2281bfa03e63b537562ec10f9734a0a10 backlog burner
ba4c9238c04bbd0405f802c7d2327d2fc3394183 add daily backlog burner
ee083a2e6c09bfe824d0abf57d99be4ecf0e0380 Daily Test Coverage Improver: Add comprehensive API AST map tests (#7890)
9b88aaf13468b2455a3f1295afe8ec4c521f56e9 determine parameter evaluation order
05ba67f432076d1fdf8cb739291104c1c36bf702 Merge branch 'master' of https://github.com/Z3Prover/z3
647c8cc6c1181ed17b65fd21bfcb8068a973d4a6 add roles
44d2bba3e5edc1273a547bcd6ae29cbb6e1051f2 Add comprehensive tests for API algebraic number functions (#7888)
6d3daa53383f3ebd0881fc2e349f0a7f86d5fbb2 add ask and pr-fix
75a6e7a3797fbf1867ca6cc1b1b90697d0fedf14 update improvers
ce81aa90786efb4d1aec28e63df611bb3c0e7212 Merge pull request #7886 from Z3Prover/fix-coverage-merge-mode-3c3ea7b0579fb998
9069a35b69c9ce031b217f7c902703595295659b Update wip.yml
6926a4e2ca58dc4cdb8ab8b7f9bac436950a91ee Fix coverage report generation with merge-mode-functions=separate
40a60f10ce1396bc53fb49cc53467860c25282b7 update token
1aeef3bf811e029376a56914b2032c8e48ee193e update agentics
96996bf9ec205f74aacb7a2a65d09d92f005d5c9 Bump actions/github-script from 7 to 8 (#7882)
7d6ff3fae4639c5ae739cbb9d2420d9017ddfa6d Bump anthropics/claude-code-base-action from 0.0.56 to 0.0.63 (#7881)
c4675cb46363bcd82405617820cfb5676f4a63b5 Bump actions/checkout from 3 to 5 (#7880)
6752be72635eb6bd63ddaac9dab7f9135784e385 Remove unused variable in polynomial.cpp
b0bc41457febff75c7b384317430b1f9fdb777f1 Update polynomial.cpp
58bab093d1af6c8e7b73d92d886cb8651eaa17c1 Change MSVC build trigger to scheduled cron job
9a91ba19551a62b1d449ec82f086aaf32902b63a Change MSVC Clang-CL build trigger to scheduled
01da2679886ba3ad34eac19a1a8e074499677b83 Update Pyodide workflow to use scheduled builds
93333eca66ef489b5c3a3c27431bd07e8ec983ad Change GitHub Actions trigger to scheduled
c496787923f001d725537c26add82c8e88c79e46 Change coverage schedule to run every two days
ff6a4f9b1271fe91d23b71e57e6e5af2360a4d9b Add scheduled trigger for Android build workflow
7efcda2674d06ef9ff084602d7727e263c5829f4 Update polynomial.cpp
f4a87d4f613f54c50058d9d1ce17ca2bd74026e6 shelve experiment with a variant of geobuckets
7b4194994a3a2f4166045e6f1a71c6161637b5c9 Merge pull request #7878 from Z3Prover/perf/daily-perf-improver-build-steps-8936dfa90701cfcd
a31656a7059bf7334d609abbd2f788e761c41faf Daily Perf Improver: Add build steps configuration [ #7872 ]
25a79d73b1b2dbee17d80ee25dcca20d43e076fc update workflows and use token for safe outputs
41491d79beb347ef25765818f4bf3fd65ea11ccf Add comprehensive test coverage for math/lp and math/polynomial modules (#7877)
6e767795dbd1192359ce578f4294827b15b151c8 set status to unknown
928a2e7cf22f574021814a968059c458958fbe1c update python doc tests
0d0dd0315abb337adec530c2bc17548ccea4f675 evaluate unhandled arithmetic operators based on an initialized model #7876
3c897b450f1bbcc2abfd6d20eac7ec144698d239 add rewrite rules for update-field under accessors and recognizers
6afa1c5be87eb5958ecb77b0e2826996ae5586fe add back coverage module
84bf34266b655e6380108325cbdb81a5f7560093 put back shortcut for square test. Remove assumption in unit test
8158a500d4e4be2fc3a05532f966e2d0c6d82eeb remove shortcut as it breaks current contract
573c2cb8f721e5b93b8471031f6c8539e4e62ac6 micro tuning perfect square test
c350ddf9906492cf229025aa996000834b333a82 remove a few useless dynamic casts
f0c788581ab380334d785e83b8e9d217ee4f8f3c Merge pull request #7871 from Z3Prover/add-workflow-githubnext-agentics-daily-perf-improver-9993
095e0f5db80def9a3e153660dc580591027e388b Add workflow: githubnext/agentics/daily-perf-improver
66acd4aa7b8048f275a9344ba5bd5f637c31e418 Merge pull request #7870 from Z3Prover/daily-test-coverage-improver-config-6b08d6955c91424a
93b00d9fcb6da3189458e4d4c4a7dc7b8eb1b16a Delete coverage-steps.log
3a187ea21651a8fa0593c0e737e595077d0920b0 Add test log for coverage configuration
cc8e2f372ba1b94013166079d84f47d70c0fea1c Add coverage steps configuration for Daily Test Coverage Improver
f0ffa60675fa47776e2f7b31811aa937b554df27 fix workflows
49872d27cda2c6d8151fde158dd2812a99abfc6c Merge pull request #7868 from Z3Prover/add-workflow-githubnext-agentics-daily-test-improver-6525
19f8001dd96846756a46cb38d2ee8e3458e207db Add workflow: githubnext/agentics/daily-test-improver
3a409e0673d06a191c578fa92eb0b7a31f953c8c #7861
8440623f6dedca274b23b255fcfb5a8c97c2d3d8 initialize table with power of 2
294f0578b06c5d0f5edafabe9dda7e983e945f82 Fix Java API mkString to properly handle Unicode surrogate pairs (#7865)
9196a3c36914533c234e0a2f304898d77c02d6c4 fix #7861
7566cc744d3aff13ced687104b2cb5bff1a1472b display assumptions used
e6b0b2d1b4cd5afb154ba370158125cfc2059421 Bump actions/setup-node from 4 to 5 (#7858)
b2acbaa0c9fec4720d68b775edac432e63fd774e Fix .NET performance issues by reducing multiple enumerations in constraint methods (#7854)
a7eed2a9f381c79d10d9602121132fbe538562bd remove flush_smc after m_solver.get_model #7855
d701702735bdea169f7748dea9cbf4a24c8fc518 remove model converter operator on expr_ref&
90e610eb2358a581db606f583a367e803278321c Fix performance issue in MkAnd(IEnumerable) and eliminate code duplication (#7851)
866393a8428005b871a0bfa3aa0ca22baf74c14b update defaults for new grobner featuers
d7718623a4a8c0039eefd5da778b9514cca12ee7 handle case where all variables are bounded
98a9a34f2bd68adc4616d1bc6c959e35253c33a5 add option to reduce pseudo-linear monomials
6eee8688c2b21570313ec8b86f10c46fb29fa933 Add Windows ARM64 builds to NuGet packages for nightly and release pipelines (#7847)
e0c315bc3e5b24b7508a6d134ff1ee3b6e869a57 filter pseudo-linear monomials
449704ef64a91a3322f8a8bdd15be52884ee12fa Enable ARM64 support in .NET NuGet package (#7846)
7005d0475580cd062b00077d777f1af4d8d4b119 propagate mod over ite even if it hurts
a382ddbd8ab84ac7d7955644c7e8235382ca91a7 add rewrite for mod over negation, refine axioms for grobner quotients
e2235d81d345b01ef9c88c1fe9b85dba41e2a983 add option for gcd-test to grobner
49703f8bba0e73fbd2aa6b180f8afdaeadd4d7a4 remove debug out
4c0c199e328a90ca63ce1d22fa728c672894d305 take into account integer coefficients
e91e432496b5877bd0a6fcbc7f390d3448954be5 add option to propagation quotients
91b4873b790e13a2b1feab3126b67e557a21bdcb categorize lp stats
06de5f422c19a6c97157e3d8f5475dea4568340f remove str parameters
9d16020a069fd5ebd3601a9862961af545ac238a Use '--tags' rather than '--long' for git describe. Closes #6823 (#7833)
3e216dbb2078e9b6d79f5b8f65a54d1ba31f5289 Fix method signature for onBindingWrapper, again (#7829) [ #7828 ]
a5609364ddc2285422daa3dbd4db9ebfab334b1a Fix method signature for onBindingWrapper [ #7828 ]
2337e68169e944900cd6768dda7334528805ba34 fix #7822
b8b9327a709eecc3977ec4d58367c298135983bb [CMake] Document hybrid approach and fix FetchContent C++ header path issue (#7819)
1bed5a4306b1eb7c8f19cbc73104bf871dca8277 remove double tweak versioning
894c0e9fbef5d17426a3217992a489b90dc3c8ea Bugfix: post-build sanity check when an old version of ocaml-z3 is installed (#7815)
12563c6963465b78b80ce263b9063d0e6d89a84b clean up a little of the handling of VERSION.txt
300e0ae69edd7b6668e4c22273cbdf98ca0968f4 Move VERSION.txt to scripts directory and update all references (#7811)
287464567b8ee39548d6babc271c2a7b8dfcddfb copy VERSION from SRC_DIR
116e1eca8bb45a758fae8c8f0b388813033933e7 print dirs
be22111df5282423c4fe87ecafb837801829b7ee more output
867bc6aee6c289bc3365f930e58e7609a857892c remove extra characters
438b41acbfa63ed98b9a83ea09baa038e2421023 try other dir
1987b3dde17e87608de86189d826d2b0f2ee394c try src_dir_repo
778b9a57c32e8f22ea423d0ab33a3af212ba969b try diferennt dirs
3b036369f9ca0581f79f8aa2e199499f563a5278 add more logging to setup.py
21e63dba8d839d942915d2929a143506fe2973c3 add print for version file
8d395d63aef4a1f1eda85838b6ce3a96e84501ec Fix Julia bindings linker errors on Windows MSVC (#7794)
ba068d751c08d0ae229eeaa34d289ec9922e4a92 Document how to use system-installed Z3 with CMake projects (#7809)
7e6e96f6aae5b65e15da8604cb7215a4aaec94b2 remove resources directive again
12e74783b6f92e1410fdc57ebeaceef5a18ac07d add resources
4792068517c3f98c0ed01a8badc8ac3b4a4420d8 Attempt at adding the README to the NuGet package (#7807)
64419ad85be164491355d0adbd20492eed4125b0 Update nightly.yaml to match release.yml NuGet tool installer changes (#7810)
5d29eb1060566662452d111568e5eeda5b50cd74 Fix Azure Pipeline PyPI package builds by including VERSION.txt in source distribution (#7808)
fa0f9c97bc0149eb7e98194f7793415165796fc1 fix parsing of version
02f195a380afe1c36885fae53361d6a691566377 fix version parse
72655637deebe5d3a79d7725287c634ac261b6fa read version from VERSION.txt
265265a68c4514a4ead7272d6c37135f1c416fb2 Create centralized version management with VERSION.txt (#7802)
debe04350cf620c3e54b6ed84c43c75e62c619a4 fix #7796
21e31684211bc76c5d69e52af3a34fc5db1eba2f fix #7753
4542fc0b3b942f9c971362348e2482adb4dfcd66 update version number to 4.15.4
7ff0b246e8e108d4649e0e1b302e9c9d87b01e73 fix #7792
ff74af7eaa8f419a36be355ed68a9b5c5cc984cd check for internalized in solve_for
4082e4e56adc19bd3eb45ca7c80a0df33936f334 update on euf
c75b8ec752c89abf6f726d2a9567efa45bee6204 add option to control epsilon #7791
d8bf0e047faa35a4196b66f6671522a4d843a602 Fix nullptr dereference in pp_symbol when handling null symbol names (#7790)