Z3Prover/z3 z3-4.15.4

on GitHub

• 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 two days
• ff6a4f9 Add scheduled trigger for Android build workflow
• 7efcda2 Update polynomial.cpp
• f4a87d4 shelve experiment with a variant of geobuckets
• 7b41949 Merge pull request #7878 from Z3Prover/perf/daily-perf-improver-build-steps-8936dfa90701cfcd
• a31656a Daily Perf Improver: Add build steps configuration [ #7872 ]
• 25a79d7 update workflows and use token for safe outputs
• 41491d7 Add comprehensive test coverage for math/lp and math/polynomial modules (#7877)
• 6e76779 set status to unknown
• 928a2e7 update python doc tests
• 0d0dd03 evaluate unhandled arithmetic operators based on an initialized model #7876
• 3c897b4 add rewrite rules for update-field under accessors and recognizers
• 6afa1c5 add back coverage module
• 84bf342 put back shortcut for square test. Remove assumption in unit test
• 8158a50 remove shortcut as it breaks current contract
• 573c2cb micro tuning perfect square test
• c350ddf remove a few useless dynamic casts
• f0c7885 Merge pull request #7871 from Z3Prover/add-workflow-githubnext-agentics-daily-perf-improver-9993
• 095e0f5 Add workflow: githubnext/agentics/daily-perf-improver
• 66acd4a Merge pull request #7870 from Z3Prover/daily-test-coverage-improver-config-6b08d6955c91424a
• 93b00d9 Delete coverage-steps.log
• 3a187ea Add test log for coverage configuration
• cc8e2f3 Add coverage steps configuration for Daily Test Coverage Improver
• f0ffa60 fix workflows
• 49872d2 Merge pull request #7868 from Z3Prover/add-workflow-githubnext-agentics-daily-test-improver-6525
• 19f8001 Add workflow: githubnext/agentics/daily-test-improver
• 3a409e0 #7861
• 8440623 initialize table with power of 2
• 294f057 Fix Java API mkString to properly handle Unicode surrogate pairs (#7865)
• 9196a3c fix #7861
• 7566cc7 display assumptions used
• e6b0b2d Bump actions/setup-node from 4 to 5 (#7858)
• b2acbaa Fix .NET performance issues by reducing multiple enumerations in constraint methods (#7854)
• a7eed2a remove flush_smc after m_solver.get_model #7855
• d701702 remove model converter operator on expr_ref&
• 90e610e Fix performance issue in MkAnd(IEnumerable) and eliminate code duplication (#7851)
• 866393a update defaults for new grobner featuers
• d771862 handle case where all variables are bounded
• 98a9a34 add option to reduce pseudo-linear monomials
• 6eee868 Add Windows ARM64 builds to NuGet packages for nightly and release pipelines (#7847)
• e0c315b filter pseudo-linear monomials
• 449704e Enable ARM64 support in .NET NuGet package (#7846)
• 7005d04 propagate mod over ite even if it hurts
• a382ddb add rewrite for mod over negation, refine axioms for grobner quotients
• e2235d8 add option for gcd-test to grobner
• 49703f8 remove debug out
• 4c0c199 take into account integer coefficients
• e91e432 add option to propagation quotients
• 91b4873 categorize lp stats
• 06de5f4 remove str parameters
• 9d16020 Use '--tags' rather than '--long' for git describe. Closes #6823 (#7833)
• 3e216db Fix method signature for onBindingWrapper, again (#7829) [ #7828 ]
• a560936 Fix method signature for onBindingWrapper [ #7828 ]
• 2337e68 fix #7822
• b8b9327 [CMake] Document hybrid approach and fix FetchContent C++ header path issue (#7819)
• 1bed5a4 remove double tweak versioning
• 894c0e9 Bugfix: post-build sanity check when an old version of ocaml-z3 is installed (#7815)
• 12563c6 clean up a little of the handling of VERSION.txt
• 300e0ae Move VERSION.txt to scripts directory and update all references (#7811)
• 2874645 copy VERSION from SRC_DIR
• 116e1ec print dirs
• be22111 more output
• 867bc6a remove extra characters
• 438b41a try other dir
• 1987b3d try src_dir_repo
• 778b9a5 try diferennt dirs
• 3b03636 add more logging to setup.py
• 21e63db add print for version file
• 8d395d6 Fix Julia bindings linker errors on Windows MSVC (#7794)
• ba068d7 Document how to use system-installed Z3 with CMake projects (#7809)
• 7e6e96f remove resources directive again
• 12e7478 add resources
• 4792068 Attempt at adding the README to the NuGet package (#7807)
• 64419ad Update nightly.yaml to match release.yml NuGet tool installer changes (#7810)
• 5d29eb1 Fix Azure Pipeline PyPI package builds by including VERSION.txt in source distribution (#7808)
• fa0f9c9 fix parsing of version
• 02f195a fix version parse
• 7265563 read version from VERSION.txt
• 265265a Create centralized version management with VERSION.txt (#7802)
• debe043 fix #7796
• 21e3168 fix #7753
• 4542fc0 update version number to 4.15.4
• 7ff0b24 fix #7792
• ff74af7 check for internalized in solve_for
• 4082e4e update on euf
• c75b8ec add option to control epsilon #7791
• d8bf0e0 Fix nullptr dereference in pp_symbol when handling null symbol names (#7790)

This list of changes was auto generated.