z3-4.12.1

4.12.1 release

Changes:

• 3012293 update release script
• fcc1bb5 updated release notes
• 7368f9f increase build version, better propagation in euf-egraph, handle assumptions in sat.smt
• c8f197d specify macos-11 in nightly to force os11 build
• dde5218 fix mbqi value caching issue raised by Clemens and Martin
• d5fde2e #6538
• 4f7f437 fix bug in new core not detecting conflict, fix #6525, add tactic doc

This list of changes was auto generated.

z3-4.12.0

4.12.0 release

Changes:

• feda706 Update release.yml for Azure Pipelines
• 5dbd0bb add sign
• 54524de Update release.yml for Azure Pipelines
• c33b1e3 fixup manylinux reference in release script
• 234ff28 prepare release script
• f180513 missing code signing
• 60fef92 missing code signing
• 42fbf23 update code signing
• d289434 fix #6535
• 0d46787 update readme

See More

• d204413 remove update
• 85abbb8 include apt-get update for doc build
• e4bd406 update version of manylinux
• 25b0b14 move bound_manager to simplifiers, add bound manager to extract_eqs for solve-eqs #6532
• e5e1626 Initialize m_istamp_id in lookahead::init (#6533)
• 8970a54 expose parameters to control behavior for #5660
• 1c7ff72 add tactic doc
• d415f07 memory leak on proof justifications
• b700dbf fix #6528
• 2bd933d Fix hwf.cpp for MinGW-w64 32-bit clang (#6529)
• c3e3114 fix #6530
• a4d4e2e track assertions
• 64ec8ac fix model reconstruction ordering for elim_unconstrained
• 30e0f78 remove exit
• a4f2a1b Bump json5 from 2.2.1 to 2.2.3 in /src/api/js (#6527)
• 49ee570 split into separate function
• 5899fe3 Add rewrite for array selects of chain of stores of a same value (#6526)
• 1ddef11 several fixes to proof logging in legacy solver
• 61b90e6 disable new simplifcation for multiplier until really understood
• fcea323 add missing tactic descriptions, add rewrite for tamagochi
• 95cb06d add quasi macro detection
• 25112e4 bugfix to flatten-clases simplifier
• c07b6ab more tactic descriptions
• 0d8a472 pass sign into literal definition for pbge
• 81ce57b #6429
• e009915 #6429
• 380c701 restore debug clang/gcc build
• 21362c0 make case-def and recfun-num-rounds re-parsable for logging
• ef10119 #6429 fixes
• aa080a6 update ignore-int handling #6429
• 8d0d6d8 Merge branch 'master' of https://github.com/z3prover/z3
• 6f95c77 fix bugs in flatten_clauses simplifier, switch proof/fml
• e448191 array rewriter: expand select of store with const array into an ite
• e508ef1 fix Alive bug #875: bit blaster not respecting soft memory limit
• a2cc504 remove a couple more std::endl
• d30cb55 don't flush stream when printing param vals
• d449073 Merge branch 'master' of https://github.com/z3prover/z3
• ea0d09b add pointer to build parameters to README #6518
• dbf93c5 Fixing array select for lambda expressions in Python API (#6516)
• f6d411d experimental feature to access congruence closure of SimpleSolver
• c0f1f33 dampen second setup of theory_bv
• 5f6f2fc rename bit_blaster class to bit_blaster_simplifier to avoid name clash
• 0d05e06 initialization order
• 2c3ecce fix build
• 8002a51 tiny fix to qprofdiff (#6497)
• 293627c fix #6513
• 07ab4d3 fix #6513
• 47324af be nicer when memout is reached in SMT internalize: return undef rather than crashing
• 7cc58c9 Merge branch 'master' of https://github.com/z3prover/z3
• ec74a87 fix #6510
• 3e8cbb6 #5884
• abef260 Merge branch 'master' of https://github.com/z3prover/z3
• bc19992 add doc for ackermannize
• 8d332cc #6508 (#6509)
• 6fab4fe #6508
• b9c4f5d #6506
• 8efaaaf Fix #6503
• fe80347 fix #6501
• f961300 Merge branch 'master' of https://github.com/z3prover/z3
• 603597a deal with cancellation in qe for #6500
• e423fab tactic
• 0768a2e updated doc
• ecf25a4 outline scheme
• 13920c4 more doc
• d5316e0 add tactic descriptions
• f01d9d2 Merge branch 'master' of https://github.com/z3prover/z3
• aed3d76 add doc
• d47dd15 set encoding into gparams because this is the only entry point in zstring #6490
• c4b2aca add missing error checking #6492
• dbb4bbe remove debug out
• 9054e72 fix #6467
• cd3d38c sort out terminology/add explanations, add shortcut to C++, fix #6491
• 2d7a38e fix #6488
• 7afcaa5 update doc
• e648e68 add doc
• e82c8e7 Fix a compilation error with clang-cl (VS2022) (#6489)
• aded8e5 fix #6488
• 4598af7 fix #6488
• a3e6885 fix #6488
• 039de6a build issues
• cb86031 fix build
• d308b8f simplify code + remove unused file
• 6b60a3d fix syntax
• 2520dcb merge
• 2d43ccc Revert "fix crashes in elim-uncnstr2"
• 6a1b3f7 move debug output to before state update
• f7269bb update doc
• a9f52b0 doc fixes
• 527fb18 add doc for card2bv
• a302c2f fix crashes in elim-uncnstr2
• ee307dd Merge branch 'master' of https://github.com/z3prover/z3
• 1434c7d #6059
• 9ebacd8 fix buggy mask (typo in my last commit..)
• 96a2c04 fix bug reported by Nuno
• a96f5a9 fix overflow in mpz::bitwise_not
• c6f9c09 cleanup more in dependent_expr_state_tactic to reduce mem consumption
• ca6fed8 minor code simplification
• 8981d32 #6481
• 4a451b1 add custom coercion for floats. fix #6482
• c45c40e doc
• 7e69dab distribute forall cpp code
• c33e58e update distribute forall
• 80033e8 cave in to supporting proofs (partially) in simplifiers, updated doc
• aaabbfb remove comment that does not align with result
• d125d87 typo
• 1e06c74 add doc
• 7df4e04 add der description
• 90ba225 add more doc
• 5a5758b add documentation to initial selection of tactics
• f1a65d9 add documentation notes
• a2f5a5b remove memory alloc from statistics_report
• eb8c53c simplify factory of dependent_expr_state_tactic
• de916f5 add demodulator tactic based on demodulator-simplifier
• 8709595 fix #6477
• ead2a46 build
• b76ed6a proper fix to #6476
• 9b58135 try to fix linux builds
• 0f7bebc try big M for linux build
• 1974c22 add demodulator simplifier
• 9acbfa3 move it into substitution to handle dependencies
• 3d7bd40 a round of cleanup
• d218083 The demodulator doesn't produce proofs so remove code path that depends...

z3-4.11.2

4.11.2 release

Changes:

• 8e6f17e inc version
• 1382cde release notes
• 85c8168 use for pattern instead of iterators
• 60967ef fix wrong condition for delayed bit-blasting
• 0bdb2f1 add verbose=1 log for mbp failure
• 7e1e64d fix #6313
• 9dca8d1 fix negative contains bug (#6312)
• e4ef171 fix variable tracking bug in explanations with literals
• eb1ea94 detect nested as-array in model values
• eb2b95e spacer: trying to make C++ happy

See More

• f2afb36 extend distinct check to ADT
• 61f7dc3 remove creation of trivial testers
• 46383a0 AG - unary datatypes, tester always is true.
• ac5b190 track instantiations from MBQI in proof logging for new solver
• d3e6ba9 remove union
• 3011b34 log E-matching based quantifier instantiations as hints
• 6077c41 #6116 bv2int bug fix
• f72cdda Change to 4 digit assembly version (#6297)
• 4abff18 fill in missing pieces of proof hint checker for Farkas and RUP
• d2b618d Spacer Global Guidance (#6026) [ #3 ]
• 1a79d92 revert last ditch array
• 36d76a5 fix #6304
• 45d8d73 #6303
• 0f475f4 Add RUP checking mode to proof checker.
• 8cb1182 add missing status case for cancelation
• cd0af99 fix #6302
• dd90689 build fixes
• 6f2a6da address unused variable warnings
• 4d29925 build fixes
• 8b8caf9 re-add smt-solver for proof_cmds
• 37fab88 respect dependencies, move proof_cmds to extra_cmds
• f65a244 move proof_cmds
• f5d2b9b fix typo in comment defining macros (#6306)
• a0ca5d7 Fixed nested user-propagator callbacks in .NET (#6307)
• e2f4fc2 overhaul of proof format for new solver
• 9922c76 add extra information for type error message
• dd91fab Merge branch 'master' of https://github.com/Z3Prover/z3
• 159026b regression fix to ackerman gc and memory smash, perf fix for handling bv2int axioms, perf fix for filtering ackerman
• 458f417 move drat functionality into euf
• 1ffbe23 add virtual destructor to fix build
• 1894c86 virtual
• ca0a829 add function pointer to class to see how MacOs build reacts
• 0d7b7a4 selectively re-add solver_params
• 5f2387b revert some changes that coincide with breaking macos build
• a628e4c updates to printer to get instantiations, take 1
• f0eee41 include depenency
• 6c165e8 #6299
• f6e151a assert
• d975886 fix #6300
• fb8532b succinct logging
• 74c61f4 move std::function to header of sat-drat - alignment?
• c626358 fix validator bug returning true for unprocessed case, bug reported in #6116
• ce1f398 fix unsoundness in quantifier propagation #6116 and add initial lemma logging
• 912b284 disable validate_hint too permissive
• 2f8b133 add redirect for warnings
• fbf9e30 ack
• fbfb28e update release notes
• 916d1db fix default parameter regression
• 7ab904b remove spurious file
• 0eea021 include global parameters and fixup for HTML meta-characters
• f6e4a45 Merge branch 'master' of https://github.com/z3prover/z3
• 64e0e78 #5953
• 09ab575 parens
• daa24ef add missing error check
• 9eb4237 fix #6292
• a383087 #6288
• 4092302 use interface for creating unary equalities
• 17fc438 don't have bv-ackerman influence simplification
• be0cd74 #6289
• 2181a0f #6289
• 56fb161 ADT-constructor generation crashed in .NET/Java when no (= default) fields are given (#6287)
• 6ba9ada Fix typos. (#6291)
• 706f7fb Fix some warnings about unused stuff. (#6290)
• d5d77df minor code simplifications
• 08bf7a6 fix name
• 665ef2c add missing new
• bb5d811 use equalities
• b26420e #6285
• ea8b118 Android CI: Configure with CMAKE_ANDROID_API (#6284)
• e83a70f add newlines for description
• 514eaf3 Merge branch 'master' of https://github.com/z3prover/z3
• 600b449 don't forget parameter documentation
• 540e36e roll version number

This list of changes was auto generated.

z3-4.11.0

4.11.0 release

Changes:

• 19da3c7 fix closing parnetheses
• d094f6a fixing interface and test'
• c7eda4e fixing interface and test'
• 103cd24 update release notes
• c3d635c handle build warning
• 6fb7a04 test fromString
• 53e1688 add fromString method
• 4be26eb #6116
• 8e167aa #6116
• 1a5503c enable new code path for mod handling

See More

• cb272bd fix missing removal of x in solve_mod
• b3f4d3f Publish Z3 symbols (#6280)
• 48b1329 add bv-size reduce #6137
• 45a4b81 fixup github connection
• 2103379 add parameter documentation to nightly
• fe00e95 remove \r from output
• 9d6de2f parameters neatified
• 498b6de finish parameter help
• b169292 add parameter descriptions
• 583dae2 enable nested division
• 681ed95 Bump docker/build-push-action from 3.1.0 to 3.1.1
• 88b3e0c Update github service connection
• 88f4664 Standardize ubutu-latest vmImage
• e0aa32e fix #6270
• a0d4a8c update diagnostics
• 138f0d2 fix regression found by fuzzers fix #6271
• 1d87592 fixes to mod/div elimination
• f014e30 disable case1
• d80e2fb fix build
• 16a9486 Merge branch 'master' of https://github.com/z3prover/z3
• fa91a64 make extensionality commutative
• 5669cf6 bug fixes to mod/div quantifier elimination features
• 88b6c4a pdate decl collection to include functions under arrays
• 72f4ee9 api: Correctly map OP_BSREM0 to Z3_BSREM0.
• 550d691 updates to div/mod handling in quantifier projection
• d272bec fixes for division
• f989521 add initial skeleton for xor-solver
• b6d71fc fix #6265
• 03385bf improve quantifier elimination for arithmetic
• 786280c print skolem declarations only for lemma tracing
• 791ca02 formula simplification example
• b55ad5f fix #6267
• 4906425 fix issues for user-propagator from new core
• f27485d avoid push/pop if diseq/eq are not defined
• 78eaefe move solver-params to params
• 77a313f redo #6242
• 63f48f8 add options for logging learned lemmas and theory axioms
• 410eed9 #6116
• 8e077d8 #6116
• 539d444 #6196
• f34317d #6196
• a4ea281 fix #6260
• 5014b1a Use = default for virtual constructors.
• aa0719a model_based_opt: fix enabling complete resolution
• 80c516b squash stores
• 6835522 z3++.h: No longer include unused sstream.
• e48474e Merge branch 'master' of https://github.com/z3prover/z3
• c51af91 #6257
• a9b7348 (cmake): fix visibility on shell z3 binary
• 78a0f57 for #6257
• 7eb1e6d userPropagator: Compile as C++20.
• 1d9345c Fix typos.
• 08165f5 No need to return a const bool.
• 9da6895 add option to select with folding
• a8ff976 max maximal unfolding configurable
• a3161bd update_api.py: Remove usage of MKException.
• 8a3556e cmake: Remove dep on mk_util.py for update_api.py calls.
• ad4c786 mk_unix_dist.py: Fix --nopython
• dc75031 Remove all per-OS defines apart from _WINDOWS.
• 85b96dc cmake: Remove telling the Intel compiler to link OpenMP.
• d908ebe fix memory_high_watermark parameter according to documentation
• d8c9948 test/lp: Replace if linux with if not windows.
• 55b70b4 Remove contrib/cmake.
• 112dba5 Remove unused private member from smaller_pattern.
• 3ab9628 Remove Travis CI configs.
• 774ce3d create special case for osx arm
• 42f5047 cmake: Cleanup remnants of workaround for USES_TERMINAL.
• 8313282 Use char version of find_last_of when possible.
• b361226 Use cmake properties for symbol visibility and PIC.
• 886c3ab Remove remnants of _MP_MSBIGNUM checks.
• 053c3ec Bump docker/build-push-action from 3.0.0 to 3.1.0
• fb1d0bc cmake: Remove ExternalProject BUILD_ALWAYS workaround.
• 9a99c78 Enable thread_local code more broadly.
• 82d853e Use = delete to delete special methods.
• 059b795 Fix warning about \ref when building website.dox
• 2c2ab0d Additional BV matchers
• 5d858da union_find::reserve
• e8e64d3 dlist::insert_before/after
• de6a0ab PDD operations
• 42233ab Additional BDD operations; BDD vectors and finite domain abstraction
• 9275d1e sparse_matrix iterators
• 6eae27f numeral helper functions
• e31926d var_queue display
• 6a929f9 scoped_ptr_vector usability
• d2fe174 Add SASSERT_EQ and VERIFY_EQ
• 79ee543 Move tbv to util
• a89be68 Use false instead of 0.
• fe1e301 Remove Z3_bool, Z3_TRUE, Z3_FALSE from the API.
• 77e5d6a Use nullptr consistently instead of 0 or NULL.
• bf282b0 fix #6213
• 4a1baa7 fix #6165
• 5d0dea0 Remove empty leaf destructors. (#6211)
• f7fbb78 Merge branch 'master' of https://github.com/z3prover/z3
• a6fe260 update minor versin number to ABI change to remove Z3_bool from z3_api.h
• fc40e3c Remove usages of Z3_bool, just use bool.
• c682ec1 Remove remaining references to Z3_bool_opt.
• 591d485 update versions
• a2d4419 Update release.yml for Azure Pipelines

This list of changes was auto generated.

z3-4.10.2

4.10.2 release

Changes:

• 69b1337 inc release number
• 2a8e73f Merge branch 'master' of https://github.com/z3prover/z3
• 6d71d9e update coding style to C++11
• 1eb84fe Mark override methods appropriately. (#6207)
• 8e0d9bf Remove remainder workaround for pre-MSVC2013. (#6204)
• eba29a2 Use std::hexfloat more. (#6203)
• 75339c6 Fix doxygen warnings in C API docs. (#6202)
• 7823757 Enable more tests on non-Windows. (#6199)
• 44100a3 CI: Fix Android NDK home environment variable (#6198)
• ee80414 sketch initial for mpz/mpq numeral creation

See More

• 9c35971 Update RELEASE_NOTES.md
• 8551b21 fix #6194
• b6c80e8 fix #6193
• cd7ef11 add decide callbacks to propagator API
• 3e8daa5 fix re.range symbolic argument bug in z3str3 (#6189)
• 63ea7bd Revert "Bump docker/build-push-action from 3.0.0 to 3.1.0 (#6192)"
• 32bb60e Bump docker/build-push-action from 3.0.0 to 3.1.0 (#6192)
• 70895b2 Improve intra-doc linking. (#6191)
• 43f2b84 fix typo
• 5c2c0ae force-push on new_eq, new_diseq in user propagator, other fixes to Python bindings for user propagator
• 3e38bbb Make sure all headers do #pragma once. (#6188)
• 3a8eb1e increase version number
• 1155ea6 add await
• 212a065 try .ast
• 7c0ec21 try to add basic expression simplification

This list of changes was auto generated.

z3-4.10.1

4.10.1 release

Changes:

• 4368ec9 startswith
• 845e852 increment to include python fixes
• c6dad4a Update release.yml for Azure Pipelines
• 1eb2472 README: Fix release notes link. (#6185)
• 1e0f71c add way to access range bounds directly #6186
• 87dd837 Merge branch 'master' of https://github.com/Z3Prover/z3
• 89af9df add IEnumerable for distinct
• 0f9684e make fresh_eh() work for Python bindings of user-propagator
• 907dc2c adding toString() to model object

This list of changes was auto generated.

z3-4.10.0

4.10.0 release

Changes:

• 9cd3b9c Merge branch 'master' of https://github.com/z3prover/z3
• adcb3e8 set version number
• 59d47e3 don't publish pypi yet
• efa74fe fix #6180
• cf5a8fd fix validation code for pb
• a66095b fix the path to ../build/z3-built
• dc95659 did I mess up wasm paths in jest - or not?
• 3700822 did I mess up wasm paths in jest?
• 32c0d1f fix #6168
• 7f983e7 fix #6174

See More

• 3261472 fix #6176
• 1b83a45 fix #6178
• 5b219aa add mutual recursive datatypes to c++ API #6179
• 2e13c0b add API and example for one dimensional algebraic datatype #6179
• 81cb575 simplify
• 2e52029 add command-line overwrite capability to setup.py
• 2c8df54 enable fresh for python wrapper for user-propagator
• 914cfca updated release notes
• 111d27c remove dependency on pragma
• dead0c9 reverting relative path
• afcfc80 the relative path seems out of sync with how it is set up in node.ts
• 7f1893d add missing MkSub to NativeContext
• 7ded856 script to test jsdoc
• 393c63f fix #6114
• 527914d update documentation to use latest conventions
• b5a89eb add missing generation of z3.z3 for pydoc and add some explanations to logging function declaration
• 95c3dd9 Added missing decide-callback for tactics (#6166)
• 6e5ced0 optimizations to api ctx ref counting
• eb2ee34 fix typo
• aefd336 set OCaml default behaivor to enable concurrent dec ref #6160
• 6c5747a guard against lemmas that are already true
• 4ecb61a neatify
• b743e21 give java dynamic lib a chance for extra flags for #5848
• 2696775 remove stale assertion
• 6688c1d prepare for #6160
• b29cdca integrate factorization to Grobner
• 7c17758 add propagators to grobner
• af80bd1 Flush the trace stream before displaying sat results (#6162)
• 2f5fef9 Cache param descrs when modifying solver params (#6156)
• 4a19285 add var_factors
• 981c82c fix initialization order
• 894fb83 fix build break (debug assertion) and isolate gomory functionality
• b253db2 redundant parenthesis
• dec87fe fix issue with set-logic for eval_smtlib2_string
• 1378e71 fix #6157
• a3eb9da fix #6158
• 8e23af3 fix build
• b81f70f split nla_grobner to separate file
• 7d0c789 propagate has-length over map/mapi
• 8900db5 add diagnostics for grobner
• ca80d99 fix #6153
• 43cf053 fix #6128
• faf6c02 remove --js from nightly and release doc builds as the npm run 'check-engine' fails
• d5779bf handle trivial equalities in simplify_leaf
• 4dc88f0 add --js to nightly and release scripts, nb @ritave
• 2e79704 remove space
• 316ed77 Tune Grobner equations
• f33c933 Add substitution routine to pdd
• 5c54d65 fix #6143
• 8b29f40 Fix build on Mac (#6146)
• 49b7e90 Merge branch 'master' of https://github.com/z3prover/z3
• 7ae1a33 parallel-tactic: fix deadlocking race between shutdown and get_task (#6152)
• 99212a2 Use int64 for ocaml api functions that require it (#6150)
• 1f23460 Fixed missing assignment for binary clauses (#6148)
• 9dd529b missing initialization of List for cmd interpreter
• b68af0c working on reconciling perf for arithmetic solvers
• 9d9414c inc version number
• 0c42d3b small format update

This list of changes was auto generated.

z3-4.9.1

4.9.1 release

Changes:

• 6ed071b update release notes
• 0d41695 fix js distributable (#6139)
• cc841ca increment minor version for dev branch

This list of changes was auto generated.

z3-4.9.0

4.9.0 release

Changes:

• 2ae84f8 Update release.yml for Azure Pipelines
• 15391fc remove musll from release.yml
• f1b7ab3 x64
• 7f2ebf8 Remove package sub-directory from release script
• 580ed31 fix types and incompleteness for feature #6104
• bda8672 macarm
• 4f62336 download arm64
• 593d5be bind variables
• 8b35b7b bind variables
• 594b5da remove download of mullinux

See More

• 3ce6663 update release script
• 73f35e0 Update release.yml for Azure Pipelines
• 85c3d87 neatify
• f23dc89 add disabled pass to detect upper bound range constraints
• a374e2c ignore qid if they are both numerical - come from the parser
• 6e53621 #6112
• a251595 Merge branch 'master' of https://github.com/z3prover/z3
• d7472f0 fix #6124
• db09d38 bump emscripten version used to build wasm artifact (#6136)
• f82ca19 #6104 also in the new core
• de41cfd fix #6104
• 282c786 setting version to release
• 2a5d23b rename URL
• cd416ee add note about opt.incremental
• ac822ac add parameter incremental to ensure preprocessing does not interefere with adding constraints during search
• 2cf0c81 Update RELEASE_NOTES.md
• 2990b69 Update RELEASE_NOTES.md
• 605a312 make release notes markdown
• 71fc83c Move out equality use out of the loop
• 0353fc3 fix #6127 again
• 6ed2b44 probably won't fix #6127
• ac8aaed fix #6126
• d61d0f6 prepare release notes
• 02a92fb revert to use GCHandle for UserPropagator
• 1e8f907 fix unsoundness in explanation handling for nested datatypes and sequences
• e6e0c74 Update update_api.py
• bb96677 Update UserPropagator.cs
• d37ed41 Update Expr.cs
• c35d0d1 Update update_api.py
• 54b16f0 Update NativeStatic.txt
• 004139b rewrites for characters
• f20db3e allow for toggling proof and core mode until the first assertion.
• 4d23f28 ml pre
• 815518d add facility for incremental parsing #6123
• 8c2ba3d missing virtual functions
• 06771d1 missing virtual functions
• 4f9ef12 create dummy tactics for single threaded mode
• 3c94083 fix doc errors
• ea2a843 flat only
• b618537 Merge branch 'master' of https://github.com/z3prover/z3
• 94a2477 totalizer
• 959a0ba fix #6121
• e054f16 fixing compiler warn (missing override) (#6125)
• c3d2120 add totalizer version of rc2
• 8ab8b63 fix incorrect mod axiomatization #6116
• f6932f9 Merge branch 'master' of https://github.com/z3prover/z3
• 1a91226 remove unsound axioms, fix #6115
• 03287d6 fixes issue #6119 (#6120)
• ff26523 adjust trace output
• 5afcb48 adding totalizer
• fd8ee34 add logging
• 12e7b4c fix gc'ed callbacks in .NET propagator api (#6118)
• 7977876 add doc string
• 798a4ee use IEnumerator and format
• 556f0d7 use static list to connect managed and unmanaged objects
• 820c782 pinned semantics
• 9836d5e missing public
• b43965b make user propagator work with combined solver
• 4c8f6b6 fix #6107
• 61f5489 fix #6107
• 1fcf7cf add nl div mod axioms
• 30165ed fix #6105
• 56aa426 fix #6082
• 352666b JS api: fix type for from (#6103)
• c15a000 Make high-level JS API more idiomatic/type-safe (#6101)
• 8234eea unbreak
• 3189544 next split
• a7b41c4 fix for spurious wakeups in scoped_timer (#6102)
• 41deed5 fix bug in array rewriter introduced in 202ce1e
• 36a1f75 mask regression
• ab9aee1 perf #6100
• 202ce1e #6100 - two perf fixes
• f24c5ca #6095
• 5ba8231 make it work with old pythons
• d792d30 Update NativeContext.cs
• b254f40 Separate out native static content for Java [ #6097 ]
• 25e915f fix #5990: deadlock in the scoped_timer
• 911134b add new heuristic rc2bin (to be tested) to maxsat
• 940d10a Update coverage CI (#6099)
• 2fa60aa Added function to select the next variable to split on (User-Propagator) (#6096)
• f08e3d7 attempt to fix windows build bot
• f3c00a0 attempt to fix windows build bot
• c3407fc fix build of tests
• fcbbf7b fix build warning+error in c++ example
• d9fcfda fix debug build
• 73a24ca remove '#include ' from headers and from unneeded places
• 70bcf0b reduce sizeof(enode) from 120 to 112 bytes by swapping the order of fields
• 08c44bc remove unused static features
• 477e962 Don't reset the cache between applications of replace
• 99b606b add logging
• 7fdcbba Add high level bindings for js (#6048)
• 3d00d1d prepare for equality propagation from Grobner basis
• 8e20271 fix spacing
• 55421af fix regression in top-sort fix #6060
• 637120c Treat arguments to recursive functions as beta redexes
• 25ad5cb prepare ground for drup trim
• 35d4605 remove spurious output to stdout
• 04f94d8 fix #6091
• 46bc726 Better error message for mismatching sorts in substitutions in z3.substitute (#6093)
• 470bf27 drat
• 9cd3398 for Arie
• 994dab8 add pre-filter for F* use case
• 8efa3c8 introduce notion of beta redex to deal with lambdas in non-extensional positions
• b9b5377 add a way to supress lambdas
• 5db133f add a way to supress lambdas
• 97437bc Update sat_params.pyg
• 828850f prepare for trim
• c584750 contains-partition
• 6a1193e reorg if-then-else structure
• 72a6384 time overflow before stack overflow
• e468386 #5656
• dee6c30 na
• 80604c7 na
• 51ed13f update topological sort to use arrays instead of hash tables, expose Context over Z3Object for programmability
• 0e6c645 display model in add/del format
• a7b6f30 Bump docker/metadata-action from 3 to 4 (#6086)
• 35986f3 fix #6084
• fe08c99 fix #6081
• cc045de again
• bb6c274 fix #6085
• dca1dcc ea
• b629960 proof format
• ea365de add cut
• da93829 use common functionality
• f77608e...

z3-4.8.17

4.8.17 release

Changes:

• d420706 enable pypi release
• b8d0513 Merge branch 'master' of https://github.com/z3prover/z3
• cf1802d release notes
• 47459ca pre-release
• ffbabf2 enhance ocaml seq api (#6010)
• 5a685ba expose maxdiff
• 367bfed add min/max diff in final check
• c29cfa8 prep for max/min diff
• 87d2a3b map/mapi/foldl/foldli
• b3e0213 missing object ref

See More

• be653da init value
• d1f1e4c selectively enable dual strengthening
• 98e1c86 na
• 9cc5f69 na
• b5c7f00 add option to "rotate" cores during core finding
• 5a9b0dd Z3str3 Debug (#6000)
• 99e299b ocaml: fix is_arithmetic_numeral and is_bv_numeral (#6003)
• 02d6f6a fix build for Z3_mk_datatype_sort
• 81d97a8 enable nested ADT and sequences
• 8e2f09b #5778 - ensure arrays used inside of extensionality function are treated as shared
• 0a665b0 #5778
• 489459a #5778
• 0b453a4 set release version
• dc18b47 automatically release wasm build (#5997)
• 24baf56 fix missing propagation on final
• 33ffd46 inc version number

This list of changes was auto generated.