Nightly

Automated nightly build from commit a96a4f5

z3-4.15.8

4.15.8 release

z3-4.15.7

4.15.7 release

z3-4.15.6

4.15.6 release

z3-4.15.5

4.15.5 release

z3-4.15.4

Changes:

• 745087e update release notes
• c88295a fix C++ example and add polymorphic interface for C++
• 6efffa0 renemable Centos AMD nightly
• 1b9a636 fix build break introduced when adding support for polymorphic datatypes
• 88fcc05 Bump actions/upload-artifact from 4 to 5 (#7998)
• 488c712 Bump actions/download-artifact from 5 to 6 (#7999)
• 3570073 Add missing mkLastIndexOf method and CharSort case to Java API (#8002)
• b6e3a68 update centos version
• 766eaa3 disable centos build until resolved
• efd5d04 enable always add all coeffs in nlsat

See More

• 887ecc0 throttle grobner method more actively
• 58e64ea try exponential delay in grobner
• 2bf1cc7 Enabling Control Flow Guard (CFG) by default for MSVC on Windows, with options to disable CFG. (#7988)
• 68a7d1e Bump actions/setup-node from 5 to 6 (#7994)
• 9a2867a Add a fast-path to _coerce_exprs. (#7995)
• 06ed96d add the "noexcept" keyword to value_score=(value_score&&) declaration
• f2e7abb disable manylinux until segfault is resolved
• aaaa32b build fixes
• d65c0fb add explicit constructors for nightly mac build failure
• fcc7e02 Update arith_rewriter.cpp
• 62ee7cc Revert "Add finite_set_value_factory for creating finite set values in model …" (#7985)
• 05ffc0a Add finite_set_value_factory for creating finite set values in model generation (#7981)
• a179286 restore the method behavior
• 1921260 restore single cell
• 3b565bb trim parametric datatype test
• 5163411 Update Z3_mk_datatype_sort API to accept array of sort parameters and add Z3_mk_polymorphic_datatype (#7966)
• e669fbe Bump github/codeql-action from 3 to 4 (#7971)
• 641741f parameter eval order
• 8af9a20 parameter eval order
• 6a9520b parameter eval order
• 8ccf4cd parameter eval order
• 40b9800 parameter eval order
• a41549e parameter eval order
• 2b3068d parameter eval order
• 3a2bbf4 param eval order
• 6e52b95 param eval
• 93ff8c7 parameter evaluation order
• 00f1e6a parameter eval order
• c154b9d param order evaluation
• 77c70bf param order
• 63bb367 param order
• e9a2766 remove AI slop
• 5a96632 fix the order of parameter evaluation
• 5ae858f fixing the order
• aa5645b fixing the order
• 542e015 Remove unused variable 'first' in mpz.cpp
• cd1ceb6 [WIP] Add a mutex to warning.cpp to ensure that warning messages from different threads don't interfere (#7963)
• 3ce8aca Bump actions/checkout from 4 to 5 (#7954)
• c8bdbd2 remove directory
• e137aaa add user propagators to opt_solver
• 0e6b3a9 Add commands for forcing preferences during search
• 5d8fcaa update clang format
• 72c89e1 fix #7952 - make auto-selector detect large bit-vectors so it does't use the datalog engine for hopelessly large tables
• 0881a71 update format
• 65c9a18 fix #7956
• 339f0cd Correctly distinguish between Lambda and Quantifier in Z3 Java API (#7955)
• 253a724 add analysis
• b5f79da add analysis
• ae55b6f add analysis
• bda98d8 fix #7948
• b7eb21e fix #7948
• 391880b Add missing ::z3::sdiv to z3++.h (#7947)
• 6173a0d propagate value initialization to atoms
• eae4de0 fix latent bug in factorization
• 04ddade remove stale comment
• f5c28a0 household cleanup
• e26f7b9 fix unsound axiom for lower-bounding
• dcdae5a add smt debug output for nla_core
• ce53e06 Par (#7945)
• 2b5b985 fix divergence regression
• 9876e85 turn on max of sums transformation
• 3256d1c fix bug in unit test
• 0e8648c fix compile of lp.cpp
• a8ae52b fix missing call change to cross-nested. Prepare for lower-bound and upper-bound cardinality constraints
• 2517b5a port improvements from ilana branch to master regarding nla
• 5d91294 update workflows
• 59bd1cf updated clang format
• b17df98 Daily Test Coverage Improver: Add comprehensive API special relations tests (#7925)
• 3fa3495 Daily Backlog Burner: Fix bad .dylib versioning in pip packages (#7914) [ #6651 ]
• c43cb18 better rewriting
• 37904b9 fix the parameter evaluation order
• cda0a92 Daily Test Coverage Improver: Add comprehensive API polynomial tests (#7905)
• 82ab674 Daily Test Coverage Improver: Add comprehensive API pseudo-boolean constraint tests (#7898)
• 222c64f Remove Windows-only guard from hashtable unit tests (#7901) [ #1163 ]
• 635d3b7 Add .clang-format file for C++ code formatting (#7904) [ #1441 ]
• 1b058f2 Daily Backlog Burner: Add include directory for easier Z3 integration (#7907) [ #1664 ]
• 4e1a9d1 Daily Test Coverage Improver: Add comprehensive API Datalog tests (#7921)
• 7cb491d update compiled workflows
• d989bca update compiled workflows
• f300dfc recompile improvers
• 2d0b9e6 recompile improvers
• aabdb40 latest improvers
• 2364ea4 update improvers
• 7268136 update workflows
• db8206d improve improvers
• 5b70f75 allow burner to create PRs
• 81da4be backlog burner
• ba4c923 add daily backlog burner
• ee083a2 Daily Test Coverage Improver: Add comprehensive API AST map tests (#7890)
• 9b88aaf determine parameter evaluation order
• 05ba67f Merge branch 'master' of https://github.com/Z3Prover/z3
• 647c8cc add roles
• 44d2bba Add comprehensive tests for API algebraic number functions (#7888)
• 6d3daa5 add ask and pr-fix
• 75a6e7a update improvers
• ce81aa9 Merge pull request #7886 from Z3Prover/fix-coverage-merge-mode-3c3ea7b0579fb998
• 9069a35 Update wip.yml
• 6926a4e Fix coverage report generation with merge-mode-functions=separate
• 40a60f1 update token
• 1aeef3b update agentics
• 96996bf Bump actions/github-script from 7 to 8 (#7882)
• 7d6ff3f Bump anthropics/claude-code-base-action from 0.0.56 to 0.0.63 (#7881)
• c4675cb Bump actions/checkout from 3 to 5 (#7880)
• 6752be7 Remove unused variable in polynomial.cpp
• b0bc414 Update polynomial.cpp
• 58bab09 Change MSVC build trigger to scheduled cron job
• 9a91ba1 Change MSVC Clang-CL build trigger to scheduled
• 01da267 Update Pyodide workflow to use scheduled builds
• 93333ec Change GitHub Actions trigger to scheduled
• c496787 Change coverage schedule to run every ...

z3-4.15.3

Changes:

• a121e6c enable pypi public
• 7b8482a Remove NugetPublishNightly stage from nightly.yaml (#7787)
• a467d8c Fix compilation warning: add missing is_passive_eq case to switch statement (#7785)
• 7422d81 remove upload artifact for azure-pipeline
• e24a5b6 Revert "Parallel solving (#7775)" (#7777)
• 1e7832a Use solver factory translate method in Z3_solver_translate (#7782)
• 174d64c fix releaseNotesSource to inline
• 6df8b39 Update seq_rewriter.cpp
• eb7fd9e Add virtual translate method to solver_factory class (#7780)
• 237891c updates to euf completion

See More

• 57a60c8 add > operator as shorthand for Array
• 3abb091 fix #7776
• c8e866f Parallel solving (#7775) [ #7741, #7752, #7743, #7745, #7739, #7748, #7750, #7756, #7758, #7734, #7759, #7769, #7771, #7603, #7755, #7774 ]
• d375d97 Bump actions/checkout from 4 to 5 (#7773)
• 6486d92 Add .github/copilot-instructions.md with comprehensive Z3 development guide (#7766)
• cf8a17a restore the square-free check
• e33dc47 remove unused square-free check
• b7d5add Update RELEASE_NOTES.md
• 8598a74 rename add_lcs to add_lc
• 88293bf get the finest factorizations before project
• efb0bda remove ref to theory_str
• baa0588 remove automata from python build
• fcd3a70 remove theory_str and classes that are only used by it
• 2ac1b24 avoid interferring side-effects in function calls
• 7ba967e fix java build for java bindings
• 0cefc92 register on_binding attribute
• d57dd6e use jboolean in Native interface
• fa3d341 add on_binding callbacks across APIs
• 30830aa rename a Python file
• f5016b4 remove a printout
• 3eda386 precalc parameters to define the eval order
• eeb1c18 more untangle params
• efa63db debug under defined calls
• d218e87 add python file
• 31a3037 add Z3_solver_propagate_on_binding to ml callback declarations
• aad511d missing new closure
• b33f444 add an option to register callback on quantifier instantiation
• d4a4dd6 add arithemtic saturation
• b1ab695 fix #7603: race condition in Ctrl-C handling (#7755)
• 7a8ba4b Add support for Algebraic Datatypes in JavaScript/TypeScript bindings (#7734)
• d66fabe Update smt_parallel.cpp
• b9b3e0d Update euf_completion.cpp
• d8fafd8 Update euf_ac_plugin.cpp
• f23b053 remove a bunch of string copies
• 97aa46a remove default constructor
• 89cc9bd disable pre-processing during cubing
• 2d876d5 allow for internalize implies
• f77123c enable passive, add check for bloom up-to-date
• 67695b4 updates to ac-plugin
• 0761394 Add parameter validation for selected API functions
• e3139d4 #7750
• eb24488 FreshConst is_sort (#7748)
• ad2934f fix unsound len(substr) axiom
• 1f8b081 #7739 optimization
• 8e1a528 ensure atomic constraints are processed by arithmetic solver
• 0528c86 fix #7745
• 95be0cf remove verbose output
• e549286 add option to selectively disable variable solving for only ground expressions
• 1a488bb indentation
• 01633f7 respect smt configuration parameter in elim_unconstrained simplifier
• a6c51df ensure solve_eqs is fully disabled when smt.solve_eqs=false, #7743
• a2f1742 moving to active/passive division
• 44cd38c Update msvc-static-build.yml
• fc51067 compile warnings
• 1d1a01c update logging
• dbcbc6c revamp ac plugin and plugin propagation
• b983524 add diagnostics instrumentation to mam
• 383f4db update pretty printer to show lambdas
• 47a2376 bugfix to ac-plugin
• fd54554 fix #7725 - proofs are only possible if context was created with proofs enabled
• e575919 debug : Add support for selecting LLDB via invoke on macOS (#7726)
• 0995928 wip - throttle AC completion, enable congruences over bound bodies
• 35b1d09 working on ho-matcher
• 195f3c9 update build dependencies
• 0c5b0c3 turn on ho-matcher for completion
• 1b3c3c2 initial pattern abstraction and move matching to src
• 2d1a42d fixes to ho-matcher
• 3ccf7a6 make concurrent collect_statistics in a timeout thread safe
• 951554e ho matcher draft
• 0ee1ee5 Update azure-pipelines.yml for Azure Pipelines
• d2990e2 use usize to suppress the data loss warnings
• f544dd4 deal with warnings
• bb100a4 c is non-null
• 75678fc Fix O(n²) performance issue in CLI datatype declaration processing (#7712)
• 53c48f7 trace : Sort and reorder trace tags by tag_class and tag_name (#7714)
• 0218fb7 fixup pipleline to support testing packaging
• 0928a1f trace : Classify tag_names unique to smt_internalize.cpp (#7713)
• 8de80e6 #7710
• 97193b4 call into collect_statistics in case of -T interrupt
• a28f55a log scope level of lemma
• bfed237 expose scope level
• bc96e9e Add python packaging to main pipeline to check updates to sdist
• 725c093 use usize to work around mess with static_cast insertions when looping over small vectors
• a73e244 nits
• 661ccb3 Revert "Fix source installation to create dist-info directory for package dis…" (#7704)
• b1259fb Update nightly.yaml for Azure Pipelines
• ad0afbb Fix source installation to create dist-info directory for package discovery (#7695)
• 28d0b47 following the review comments
• 84a6e4d Fix pydoc doctest failures by updating expected output format for string operations (#7703)
• c2efd3d Update on building OCaml binding with CMake (#7698)
• 2de40ff Improve Extract function documentation to clarify bit-vector vs sequence usage (#7701)
• d717dae remove the parameter for throttling nla lemmas
• 2b6c73a add stats for throttling
• 899677e fix a warning
• 9e52a38 add throttling to generate_plane1/2
• ac34dbd consolidate throttling
• 727dfd2 use the new throttle in order lemmas
• 832cfb3 consolidate throttling
• f320667 remove debug_location parameter
• 5caa7f1 throttle lemmas in nla_solver untested
• 4631915 a version of key
• 20fb830 filter out empty lemmas from nla_solver on consumption
• 4e33b44 add lemma.is_empty()
• 5bda42e rename new_lemma to lemma_builder
• 2f2289e update minor version number

This list of changes was auto generated.

z3-4.15.2

Changes:

• bd3e722 remove nuget signing steps
• 23bd844 Update RELEASE_NOTES.md
• 3916c45 Fix: typo in z3 python api (#7693)
• 9804387 add -> as another array sort constructor
• 5ad1647 missing ;
• 95ffad8 dealloc m_imp
• 218379a [WIP] Leaks (#7691)
• a3c8bbb Update build-win-signed-cmake.yml
• bce1be4 Update build-win-signed.yml
• ffb0bd9 Update nightly.yaml

See More

• f81d973 Update prd.yml
• 8f88bf9 use is_square_free_at_sample instead of is_well_oriented
• f2912b2 remove debug output
• 126e06b fix the test-z3 build
• 0e71a9d comment and restore
• 84c8a93 renaming
• 945eef7 work on well-orientedness
• b2f0170 euf_completion with AC: add first cut of AC matching for top-level, add plugins and fix shared expression rewriting in ac-plugin
• bc31276 remove dependency on pattern inference
• cb22cdc remove dependency on pattern inference
• 20ddfc7 sketch possible AC functionality
• f932d48 use propagation queues and hash-tables to schedule bindings
• 7b432ae Rename labeler.yml to labeller.yml
• 6389214 Create dedup.yml
• 8d1e954 introduce notion of auxiliary constraints created by nla_solver lemmas
• 93d5e3f use mk_ite utility instead of custom local function
• a2ad90c Update bit_blaster_tpl_def.h
• a15e4ad #7673
• e018b02 adding proofs to euf-completion
• bba10c7 dampen order lemmas
• 3927fdb enable debug logging on labeler workflow (#7681)
• 4584d1d Create labeler.yml
• 423930d missing files
• e166175 update version to 4.15.2

This list of changes was auto generated.

z3-4.15.1

---

Changes:

• b665c99 add missing dependencies
• c387b20 move smt params to params directory, update release.yml
• dc42033 use userSpecifiedTag instead of gitTag
• 81f4125 update to @1 for githubpublish action
• 602cfaf update version number of github release
• e8f627c disable pypi publishing
• d37336e remove trace by default from tests
• 98d86c6 disable tracing in test code
• 4bd999c update release notes
• befbd8d add parameter

See More

• 9d35a8c updates to euf-completion to
• 9db227d fix bug in trim code missing dependecy
• 2897661 register completion with solver
• 1cd1622 make rule processing fully incremental
• 590b79d Fix #7623 (#7672)
• 3e75b22 fix build
• d33d6eb handle build warnings
• 7566f08 vtable
• 08c4f73 add dependencies to fix build
• e2cf4d9 add better bit-blasting for rotation #7673
• 564830a enable conditional euf-completion with (optional) solver
• 16452fe pretty printing for lp
• ef284cc for Arie
• bcedb66 Expose z3_static target for Bazel build (#7660)
• e2e5452 remove trace that accesses stale data #7668
• 7f5427b disable assertion that checks nl lemmas if using nra core
• 2fc3b07 some cleanup and functionality for tracing
• b4c2b45 #7667 - add API documentation
• 2714dc2 fix #7661
• 819c207 use array instead of hash-table to track trace
• 257b8e9 Fix out of bounds error in OCaml API (#7665) (#7666)
• 4b2e5ad enable tag classes
• bbb3d53 initialize tag class circular linked list
• a3aee02 remove commented out include directives to avoid confusing build scripts
• 6d70b49 add full path to util in include directives
• 0a93ff5 Centralize and document TRACE tags using X-macros (#7657) [ #7663 ]
• d766292 add seed parameter, fix trail undo order from insertion to ensure lifetime
• b44c897 Fix setup_relevancy for relevancy-dependent case split strategies (#7662)
• 80c553d missing file
• 77fed8b v1 of a randomizer simplifier
• 84a5303 for future ignoring genai files
• 85e7243 update add-term to avoid duplicating fresh aux-expr
• c2098b4 Pr (#7654) [ #7647, #7484 ]
• 8d67fee Update prd.yml
• a4e7123 Update prd.yml
• a7fbddd Update prd.yml
• ad02d18 add prd (#7649) [ #7647 ]
• 3381220 Create prd.yml
• 47c12f9 refactoring to use for-range
• 7ebe7c4 remove stale API #7648
• 0b26f7e Add support for building Z3 using Bazel. (#7646)
• f680242 adjust the frequency of dio calls
• 15a3818 cleanup in dioph_eq.cpp
• 1109139 move to readme-cmake
• ce15351 include some build cheat sheet
• a5a2a13 update version number
• 0d3c29a handle larger buffers
• 6b32aae remove slack heuristic
• a5e5d4d testing
• bbaec0b trying randomly shuffle the indices in the slack utilization
• 52241b6 some refactoring of lar_solver.h
• fef954c shring lar_solver.h
• 4abd984 fix the build
• e3f5e8c restore lar_solver::add_named_var
• b375faa continue PIMPL refactor in lar_solver
• b7ffcb7 implement imp of lar_solver as lar_solver::imp
• 39955f1 remove a function from lar_solver
• 4e56834 test
• a527667 shuffle more functionality from lar_solver.h to lar_solver::imp
• c81eb74 apply the slack idea in a loop
• e041fe9 slack
• 7ca94e8 add E-matching to EUF completion

This list of changes was auto generated.

z3-4.15.0

4.15.0 release

Changes:

• 9232ef5 remove copy of LICENSE.txt - pypi doesn't take it
• 49dffae enable pypi
• b54ed38 enable pypi
• 59a7e00 disable pypi
• d4b622e update version number
• a51239c update namespace, hoist exported functions outside of embedded namespace
• 6441186 list euf dependency in api cmakefile
• eca5cd1 mark virtual methods as override
• 9a299eb move mam to euf
• 0e4c033 fix #7639

See More

• 4bedb5f fix #7638
• dd211ba filter out terms that are not solved
• f89e133 revert the behavior of add_zero_assumption (#7631)
• 6af61fa remove experiment
• b502126 fix #7634
• 24090fc move flush smc to first use
• a626cd0 flush smc before use in model construction
• 71b5e44 #7596 - flush smc before copy
• 7a30223 fix #7630
• d581dc1 #7630 propagate parameters on lazy tactics
• 322e444 Fix conversion of signed 1-bit BV to FP
• 792ffee fix latent sign bug
• fe1fff3 add scaffolding for experiments with slack
• 12ccf59 rename fields to compile on c++ platforms
• e41acd7 convert m_r_upper and m_r_lower bounds to plain vectors
• fae6094 consolidate some bounds references
• f6fbeda fix #7629
• 7641393 use inlined functions
• 5cc57b8 coalesce updates to bounds
• 579ba8b add power axioms to arith_solver
• d73d104 remove overwriting x,y,rval
• ff920ba handle root expressions, and checking exponentiation with nlsat
• 2fe2735 Replace _DEBUG with Z3DEBUG (#7628)
• a1673f2 fallback to Gomory cuts and gcd conflicts if dio fails
• cc1bb0a remove superfluous makefile
• 17cac7d provide shortcut to command-line version to retrieve parameters
• 6e88d91 add badge for ocaml cmake
• 3761dd8 address build warning with overloaded virtual operators
• f7aec02 WIP: Migrating OCaml binding to CMake (#7254)
• ab9f330 change the default of running dio to true, and running gcd to false, remove branching in dio
• dbde713 remove testing code in is_big_term_on_no_term
• 1131d52 fix a bug in tracking the changes in dio
• d289495 allow gcd when dio ignores some terms
• 17af18f make gcd call in dio optional
• 436eefb always remove the tightened term
• dc7185d change the name of m_changed_columns to m_changed_f_columns
• 32e77d8 typo
• cb1818f reject more terms with big numbers
• 1cde40b dio_calls_period=4
• 87e2ce8 Update lp_settings.h - m_dio_calls_period = 4
• 59edb81 Update lp_settings.cpp
• 8db9f52 add parameter m_dio_calls_period
• ae97ee0 throttle dio
• 972f801 throttle dio for big numbers
• 3e49d9f reuse dio branch
• e31e981 Add an option "ctrl_c" that can be used to disable Ctrl-C signal handling (#7619)
• ed5dd26 remove non-working ts mcp server, settle with python variant
• 741cb5c minimal z3 MCP server
• f63c9e3 disable assignment for param_descrs
• 3f73c8b stab at SMTLIB REL mcp server
• 755f579 fix #7622
• 81f1091 remove unused bdd based variable elimination
• e41090d fix #7602
• 8035edb remove lp_assert
• 1510b31 fix build warnings
• 5ad79f2 Add Iterators as acceptable arguments to functions (#7620)
• 6ecc7a2 Fix a race condition in scoped_timer::finalize (#7618)
• a83efa6 spacing
• 8138829 fix #7616
• d792840 Add Z3_is_recursive_datatype_sort to the API (#7615)
• 14e2aad include LICENSE.txt in wheels (#7614) [ #7604 ]
• 0b7a81b list[ExprRef] doesn't build for python
• 2b60550 update agentz3 sample based on hugging face training/test data
• e7ff600 #7605
• a39efbb fix #7607
• 9d8291a remove type annotation Context | None to ensure Centos ARM Build pass
• f607331 type annotations across Python versions
• bd2c7aa remove downlevel version incompatible elements of typing
• 305f1e8 remove references to TypeGuard
• a5048e4 add initial sample agent use case
• 0a37194 fix #7609
• 5e10fd3 add selected type annotations to python API
• 26ab0de rename function
• eb4e28d [z3.py] Fix incorrect call to _get_ctx in SeqMapI (#7610)
• 8d81a2d Note that Z3_get_numeral_small is essentially redundant (#7599)
• 63ad283 Add Z3_get_array_arity (#7598)
• 934455a Remove vestiges of old ml api (#7597)
• e4897ff replace Exists by ForAll in the mathematica lemmas
• 39df899 enable shorterter mathematica printouts in nlsat
• e86a918 turn on ite simplification by default
• 8368094 fix indentation
• 4fd6ba4 replace costly ite reduction by disjointnes check
• 392bc16 optimize bool rewriter
• 2971250 add option to rewrite ite value trees
• e92ccdd change line breaks
• 17bd02d change a comment
• 8bbe752 remove dead code
• 7e4a1f2 fix crash in elim_constr2
• 93cf989 household chores - move to iterators
• dee3cf8 remove an unused field
• 9302a02 reintroduce m_var_register, and avoid modulo gcd in normalize conflicts
• 9a62ed5 added some comments
• c634701 formatting
• f073da9 cleaning up the inner tightening code
• 8c96178 avoid the variable mapping to m_ematrix and suppressing redundand constraints
• 29c5c20 use more descriptive functions than casting comparisons
• 7fb40e8 tidy
• a41bd38 use pattern of matching with undef instead of matching with conflict to reduce assumptions on procedure contracts
• 676a536 fix a print out
• d507d0f attempt to use the gcd of fixed vars
• f181e3a add comment on derivation of bound
• dd19b38 detect more m_terms_to_tighten
• 307af0f remove an unused field
• fc1c8c4 add public access to bijection key_val iterator
• 8b5510b nit
• 7577f6f neatify loops
• f091b6f remove 'unsat' move, we already have 'conflict'. Add display for cancelled
• 1af2474 code review updates, tidy pretty printer for column info
• 3202808 fix bug introduced while absstracting m_conflict_index
• f3b34fd isolate m_conflict_index functionality
• ff5ae4d add systematic way to combine lia_move results
• 00277ba nits
• 488c74d print also column values
• 22cfab3 remove term sorting by the span
• 12203fc sort terms by weight for tightening
• 0a3c118...