Releases: Z3Prover/z3
Releases · Z3Prover/z3
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.
Contributors
ritave
Assets 22
z3-4.9.1
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.
z3-4.8.16
4.8.16 release
Changes:
- 312e037 wasm build: disable error handler (#5996)
- 39f57fb update release notes
- bd6b302 Document gotcha with z3-js (#5994)
- 0529e88 enable pypi
- 459cfc8 fix #5993
- 8e509d3 remove test
- 8778f4d updated release script
- 5a2c92f format
- 81189d6 Added bit2bool to the API (#5992)
- 0dd0fd2 remove buggy prototype
See More
- e6e00d8 update nightly/release scripts to produce arm64 for what is tested
- d9f3625 change default output to print objective value
- e3c3584 remove out
- ec57d3b missing switch cases
- 5393f1d #5980
- a180254 fix #5980
- b7169e2 fix #5985
- a1ead5f #5986
- 9b66d86 add shortcut to serialize/deserialize based on question at FV hangout
- 09b0c4b fix #5988
- df98166 na
- 98c7069 add rewrite for hoisting multipliers over modular inverses
- c727e2d add rc2 option
- 4a59ae4 fixes
- 7496f11 na
- b5309d5 na
- c131eb4 build fix
- f4c500c fix build
- 807121a wip
- 8e70112 Update z3.py
- 11d992a wip: tweak GC further (#5982)
- e11496b Added decide-callback to user-propagator (#5978)
- 9ecd4f8 MANIFEST.in will now include pyproject.toml (#5979)
- c33611e include map for non vs builds
- cc36dd1 include map for non vs builds
- 3cc9d7f improve pre-processing
- a634876 sort muxes
- 7d47e45 Add a hacky patch so that Z3 on M1 hardware can link to libs properly (#5974)
- ddbe17d #5965
- 3f5eb7f re-enable pre-process
- c9fa00a expose recursive functions with own op-code over API
- c0b455e Add cmake setup.py build dep (#5972)
- 9834d7a Setup.py fix dependencies (#5971)
- 032768b setup.py: copy generated python files correctly (#5975)
- b264e6c Reverted reusing can_propagate (#5966)
- ac55e29 disable propagation
- eb2dd92 Merge branch 'master' of https://github.com/z3prover/z3
- c996a66 separate pre-processing, add callback parameter to push/pop in python API
- b0d8b27 Fixed registering expressions in push/pop (#5964)
- f43d9d0 Z3_add_rec_def body is not a macro (#5963)
- 4f4e9a9 fix a tiny typo (#5960)
- 0b20a4e Added rewriting distinct with bitvectors to false if bit-size is too low (#5956)
- f55b233 #5778
- 011c1b2 remove refs to bare_str
- 405a26c allow adding constraints during on_model
- 005b8e3 arc -> arch
- fe834b9 update regex
- c98eda0 nightly osx arm64 wheel
- d6d9b25 Allow adding constraints in the model_eh callback
- fbd35fb skip unit tests for arm
- 91ca028 arm64
- 3821eb4 fpflags
- f3789e2 id doesn't use mk_util
- 67434a3 again
- 9533dba missing arg specifier
- 746a416 more passing of parameters
- cb6aba2 more arm
- 7955326 no uname on nt
- 1346a16 #5952
- babac78 syntax error?
- 83d2aa8 add arm64 build path
- 2e91d66 Update mk_util.py
- c47bd1d add arm64 auto-detect
- 8c2909f working on python make for arm
- 1953165 set ARM64 if detected under OSX
- a863a91 Allow nightly builds to complete even if package signing fails - NOT published to nuget.org (#5951)
- 0fa0feb allow add_expr during pop
- b0dce5b remove debug asserts
- 2f63747 #5778
- cebbc71 #5778 ensure else value so that defaults align across equivalence class
- ac2523a Fix null ref on access of Entry[] contents (#5947)
- bd70c79 Update target_arch_detect.cpp
- a5d588c add example for #5933
- 053cb72 handle return status
- 4f6811a with simplification
- 05ec77c revert
- 321745f #5941
- 03a2d9a fix #5942
- 46cc54f outdated warning
- 3427215 add stubs to control memory usage
- 4b495e4 nits
- d0ef594 nits
- 25feb0e #5938 catch also rewriter_exception that can be raised on cancelation and memory pressure
- ef28f0e #5778
- 2fedcbd #5778
- 229ea56 #5778
- 97115e5 #5778
- 4cc3327 #5778
- c7922d6 #5778
- 81084b8 #5778 #5937
- 5154295 #5932
- 28e9458 break self recursion #5937
- dd27f7e #5935
- b0605a9 Update nightly.yaml
- 431c3af fix #5929 - add parameter bv_le2extract to allow disabling the disassembly to extract
- cb1e16f Update nightly.yaml for Azure Pipelines
- da00dee disable arm
- ae07a53 Update nightly.yaml for Azure Pipelines
- ff97120 Merge branch 'master' of https://github.com/z3prover/z3
- a9a8432 try add ARM path for MacOS
- 7bb969a Fixed problem with registering bitvector functions (#5923)
- 3828130 fix #5922 use 0u to help type inference
- 0bf2875 Merge pull request #5921 from Z3Prover/jfleisher/nugetpublic
- 42da976 Continue on error in GitHub tagging
- a4af26e Shorten public feed to Z3Nightly
- 32233e1 set default to true to avoid regression failures
- bb4a2b9 remove project from public/org level feed
- 365b8f3 change default to not include auxiliary functions in model as this seems to break fewer'
- d790523 #5917
- b8c61ca continue on error in deploy
- 3ffc3c2 continue on github tagging error
- 1ee3de5 temporary workaround for build
- d9e93d5 revert to buildid in version number
- 13a33a3 fix authentication input
- 16f4795 Use camel case service name
- 7bf2df1 Update nightly nuget service connection
- a24a922 fix #5915
- 8273a20 test publish to public project feed
- ce04c16 Jfleisher/nightlynuget (#5916)
- 815c971 #5778
- 4b14192 #5778
- 9011100 Update .gitignore
- 20bd59b #5778 - missed tracking literal assignment justification
- 00608cd notes
- a418678 increment version number
This list of changes was auto generated.
z3-4.8.15
4.8.15 release
Changes:
- f1806d3 remove buggy code, close, fix #5825
- 1e8bae0 enable pypi in release pipeline
- b4873d2 fix #5907
- f053daa fix #5906
- bbb2777 ensure that objects in callback are of sort Ast.
- 3439d24 Revert "doc: update readme (#5898)" (#5905)
- 9061ca5 call it macOSBuild
- b5b9c85 call it UbuntuBuild
- dfa6544 fix name for artifact
- 964e513 re-add bv_eq_axioms, fix #5842
See More
- cfe02ed remove stale return
- fd1f5cd fix callback type declarations for propagators
- eaa2fb7 update release pipeline with x86 Nuget
- 86af723 remove left-over debug output
- 6d836e7 expose model update
- a9d7026 add note about transform
- 81a5e56 publish to github
- 39df8ee update win build
- 669a1d6 na
- 29e2883 pre-release pipeline
- 6010d75 fix #5903
- 41d1c34 remove else case
- 1fa373d old bug: unit of xor is false
- 4e0a2f5 Dispose of intermediate Z3Objects created in dotnet api. (#5901)
- bdf7de1 Care for root index being undefine while calling Z3_algebraic_get_i() (#5888) [ #5807 ]
- 6455ae4 Merge branch 'master' of https://github.com/z3prover/z3
- 0b230ee move some functions to using var pattern #5900
- 6c4780a Update cross-build.yml
- 3d87d86 github action: add riscv64/aarch64/powerpc64 cross compile (#5897)
- a151725 call dispose on sorts #5900, missing charSort
- cd5e114 call dispose on sorts #5900
- cb9dcb7 add regex power to API and for Java per request
- e1929ca add regex power to API and for Java per request
- 706d7ea native context uses legacy mk_context
- 313b87f doc: update readme (#5898)
- 545341e fix #5895
- c51ca86 add another constant folding case
- e839e18 minimal addition to rewrite bit-vector to character conversion using constant folding.
- 8f2ea90 Merge branch 'master' of https://github.com/Z3Prover/z3
- 081c62d allow range comparison for bit-vectors and int/real
- 580012e fix #5894
- f26c12a fix #5882. Use model true when inlining (#5892)
- 8e18a94 Update README with info about Smalltalk bindings (#5893)
- 43f7636 remove some copies/moves
- 1d224d1 na
- c6f8ee3 na
- 3293aeb na
- e7ded9c update to 2022
- 97c7ce6 Clean up build warnings (#5884)
- e3568d5 Handle additional cases in rule_properties::check_accessor (#5821)
- 882fc31 doc strings
- b0c0f4d fix #5876
- 3e51b69 no fun!
- 2b71d8b doc macros
- 87e6f10 commenting
- 676ba78 fix else case: it is first argument of const array
- 35d26bc NativeModel: TryGetArrayValue (#5881)
- 248a367 na
- e1e8d15 stub out array serialization
- cd324a4 na
- 8d1276f using directives
- 35fb956 Updated user-propagator example (#5879)
- a08be49 NativeContext, NativeSolver, NativeModel - updates for Pex (#5878)
- 811cd9d add example
- ee18c50 add stubs for injective function axioms, add some parameter functions
- 757cf76 sketch ArrayValue, add statistics
- 80506df sketch ArrayValue, add statistics
- bf14aeb stub out nativesolver
- bbadd17 fix #5874
- 5f79a97 use conventions from Context
- c812d1e update native func interp
- 61d2654 quantifier
- deeb5e9 finish NativeModel
- c0826d5 add stubs for native model and func interp
- deaad86 nit
- 2b6dadc fix #5869
- 302c0d1 fix #5867
- 412b050 User-functions fix (#5868)
- 689e2d4 remove a bunch of unneeded memory allocations
- 7f149a3 refining model update rules for del_rule #5865 #5866
- 30a2f2f initial stab at NativeContext
- f2e712b throttle is_compatible to check variables at most once
- 7b4f1ed missing initialization of m_user_propagator, disable unsound in-processing in pb_solver
- dc110f1 Update mk_util.py (#5864)
- 6be0a66 fix #5863
- 6af170b fix #5861
- c2f1bdc fix #5862
- 11030fc disable unsound mk_seq_butlast
- ea0876b add lambda definitions during ast translation #5820
- d06c51d na
- 061e94d #5858
- e8d4804 Revert "use horn_subsume_model_converter in coi filter (#5844)" (#5859)
- 456b8ee nightly
- c47e5af multi
- cfe9846 multi
- b843618 fix #5798
- 5c26249 #5849
- 1e46395 #4889 avoid double internalize of bvle
- b38b6da add option to disable FPMATH
- f66b4f0 fir #5856
- 14ee021 nightly
- e800269 na
- d0d4ab7 #5820
- ff5d210 na
- c25d710 try out arch arm64 on the mac
- 4d184fe skip expensive equality rewriting of Booleans
- 10b611b fix #5850
- 91045d3 two words
- 9a1a728 Add str.<= and str.< to Java API
- 7091b1c add additional regex operators to API
- 2e00f2f Propagator (#5845) [ #5818, #5835, #5829, #5843 ]
- 2e15e2a Add access to builtin special relations (
Context::mkLinearOrderandContext::mkPartialOrder) to Java API (#5832) - 9cf5076 fix compiler warnings under clang (#5839)
- 09da87d use horn_subsume_model_converter in coi filter (#5844)
- 5bbb8fb add bail #5825
- 33985eb update expected
- 6202cd5 fix #5842
- aa6ec41 move idiv test to after cuts/branch
- 9a4d6ce overhead with push-ite on shared terms
- 3d26b50 fix #5827 #5828
- d745d03 switch to vs 2022
- 81e94b2 na
- 07d02ea fix #5829
- 4f6fcf8 fix #5814
- 0059e88 fix #5808
- 9958cab fix #5808
- 3f3d058 extract also units from search state
- d4ea67a Fix a few typos in README (#5782)
- 03ff320 block recursive definitions with lambdas until they are properly supported #5813
- 1c10ce4 #5815 - surface multi-arity arrays over python API
- 8a84cac add tuple support for getitem #5815
- e9dad84 update documentation comments
- 9d655cc track all unhandled operators instead of latest
- 4749495 Merge branch 'master' of https://github.com/z3prover/z3
- 05e28e4 fix #5812
- 6a412f7...
z3-4.8.14
4.8.14 release
Changes:
- df8f9d7 Update release.yml for Azure Pipelines
- bd2a53c Update release.yml for Azure Pipelines
- 5d4420a Update release.yml for Azure Pipelines
- a00d68f update release scripts and notes in master
- 5afb95b improved subset checking for regexes with counters (#5731)
- 71b868d #5722 - internalize unary xnor
- 4d8bf2a wrong unit for xor in aig tactic #5722
- f11fcec Migrate from deprecated
distutils.sysconfigin scripts (#5729) - 78222f2 remove action that fails too often
- f3af219 Use Stdlib. instead of Pervasives. due to deprecation (#5730)
See More
- cf6486f bug in flatten/and/or introduced when skipping sub-expressions
- 4b5ee91 na
- 09ee60c update comment
- 9d82c1d fix deadlock in scoped_timer destructor (#5371)
- 94a2c91 fix a few compiler warnings
- 1d9aad6 improved regex merging avoiding unsat nontermination (#5728)
- e0d6e04 fix c++
- 7a60705 #5727
- f01d096 fix again
- ad91748 Merge branch 'master' of https://github.com/z3prover/z3
- 83b47f1 fix #5726
- be38b25 fixed bug in is_char_const_range (#5724)
- 25d54eb fixing regression of issue 1224 (#5723)
- 4b813ba na
- 6a039c2 Update z3++.h
- a7b1db6 State graph dgml update and fixes in condition simplifier (#5721)
- bee7421 na
- 7441bd7 na
- 85e3622 Update z3++.h
- f0740bd move user propagte declare to context level
- 4856581 na
- 8ca023d expose propagate created
- e1ffaa7 na
- 9c8800b adding a new toy for Clemens
- 6963451 na
- 5974200 fixes to previous push and streamlining
- 4e82a9a pin expressions
- 6cc9aa3 prepare user propagator declared functions for likely Clemens use case
- a288f90 Update regex union and intersection to maintain ANF (#5717)
- db62038 Update nightly.yaml
- 4641a20 #5700 - Add download x86 as part of release NuGet
- 122b0fe fix #5710
- a099972 fix #5714
- dd6a11b fix #5715
- 2caa7e6 remove EnumToNative as it drops reference counts, fixes #5713
- 2be9387 Cleanup regex info and some fixes in Derivative code (#5709)
- 3b58f54 remove dead code
- 03b5380 na
- b1d167d fix co-factoring'
- 5348af3 fix co-factoring
- f40becf remove case for non-emptiness to combine with standard membership [ #5693 ]
- b2af7ea stdout
- 9ec0f94 hoisting out blocker for empty [ #5693 ]
- fcdf8d4 include atomic
- b85f2f7 #5704
- 0a7e003 this one is for you Nuno
- 96e871c add stub for testing updates to scoped_timer
- 0405a59 Fix return type of as_int64 (#5703)
- 51fa40e fix spelling
- b69ad78 na
- e45ae32 unsound equality propagation #5676
- a5bd115 replace_re axiom placeholder
- 773a2ae na
- 60d5a00 na
- 04906bd na
- 36f5105 na
- d74ff29 na
- 9f2b18c add tactic name
- e3bd5ba pass through for unary tactical
- 1e95fb4 add ability to register expressions during callback
- 50d50cd register forbidden functions with reduce_args for user-propagator
- 658a334 clear tactic user propagate state on solver destructor
- fdc253a update arithmetic contract for unbounded (#5696)
- 9b4f3a7 start using lar_solver::is_feasible() (#5697)
- 7758b51 Handle correctly cancelled run (#5695)
- 0242566 remove
- f0e9363 fix bug in smt_tactic_core for translating user-ids
- 0d055b8 update input for doxygen #5400
- c845b22 fix translation for equality propagation
- 1b0ac49 prevent stale user-propagators from being used on the same tactic after it was applied.
- da76535 don't rely on cleanup
- 3d528c8 typo
- eae567a indirection for user ids
- 68b072e only use setup_and_check if there is no user propagator set.
- 1618c97 adding checks
- 970347e infeas
- 0077ddf try delay init for user propagator in smt_tactic
- 41aa7d7 stack
- bfd61fe enable user propagation on tactics
- cbdd7b0 three smt2 examples added and one python example updated (#5690)
- 71cbb16 fix regression from today, see #5676
- 87aec88 fix #5687
- c6a5aa0 try th_lemma, update documentation of api functions for creating strings
- 3b4f976 na
- 4daba29 change user propagation to apply scheme similar to theory_recfun
- 3c1aedf fixing #5473
- 9e51691 add virtual destructor
- b5efb87 base -> core
- 959f4c9 rename files to theory_user_propagator
- 5857236 introducing base namespace for user propagator
- c083aa8 add debug information in user-propagate #5687
- 1e9e52a #5641
- d50c4bf remove an unused var
- d50bfc6 #5641
- 833dd62 fix #5681
- e8f5a29 fix #5679
- fee4821 include thread
- a7d2478 wasm build issue
- 741c5f4 Merge branch 'master' of https://github.com/z3prover/z3
- ca2c2bb ensure smt2log works with multi-threaded consumers, ease scenarios around #5655
- 4928c28 fix #5675
- 99d5215 revert use of f format
- f83367a mac builds
- 518ef9f fix #5674
- 4587575 if you read this commit message you probably are a programmer who has no life
- 43a827c Update release.yml for Azure Pipelines
- 71d5d24 Update release.yml for Azure Pipelines
- 72f28f0 Update release.yml for Azure Pipelines
- b95ba89 update release pipeline
This list of changes was auto generated.
z3-4.8.13
4.8.13 release
Changes:
- feadfbf enable publish
- 41a5b93 update release notes
- 5351640 Fix stray semicolon in examples (#5669)
- 5194aa1 nightly
- 1752055 update nightly
- c826b64 prepare release
- b6f7dea fix #5663
- 3c16edc check for v1 == v2
- 63ac2ee #5614 turn on / off options to get better performance.
- b28a801 #5653
See More
- b5deba8 add EFSMT solving example (#5654)
- 3a9656b fixing issues with user propagator from python
- f2fcbc7 capture values not reference
- af2cc46 #5646
- dd1e0fc #5643
- 091079e Added user propagator example (#5625)
- 87d4ce2 working on #5614
- a94e2e6 build warnings
- 036b38a ubuntu 16 is no more
- a11ca1a Update wasm.yml
- 8e59b34 Update README.md
- 933bb4f Update wasm.yml
- dfba177 Update wasm.yml
- f61e6ab Update wasm.yml
- f83226d Update wasm.yml
- fe0e1cc Update wasm.yml
- e7a54db Use emscripten to create a wasm build (#5634)
- d1fbf01 Update azure-pipelines.yml
- 96671cf Add and fix a few general compiler warnings. (#5628)
- 1d45a33 fix one typo and two misunderstandings for doxygen (#5633)
- d1592c6 fix misspelled \brief for doxygen (#5632)
- 780761a Create wasm.yml
- 4dad414 fix performance regression after adding user declared functions to model
- f5f35f8 fix grouping for latest doxygen (#5626)
- 723b755 Fix the command of
install_name_tool -id. (#5622) - eb8c8da ex handler
- 125eae0 #4869 load datatype parsing for HORN logic
- 61eb8d1 add ref for regression
- aa5b4b8 strengthen contract for log_axiom_instantiation #5621
- bdecc25 strengthen contract for log_axiom_instantiation #5621
- efcad5f fixed nullability bug in the if-then-else info (#5620)
- 4cfc737 update build
- 075769c try get_string contents again
- 45681b4 update API type annotation to make it OCaml friendly
- 3036b88 support threading for TRACE mode
- 4b7c08d Update azure-pipelines.yml for Azure Pipelines
- 09bda6f Update azure-pipelines.yml for Azure Pipelines
- cd4481b Update azure-pipelines.yml for Azure Pipelines
- ec9498e Fix ocaml link and load (#5618) [ #4840 ]
- 0660765 Add post-install testing for ocaml binding. (#5617) [ #4840 ]
- 3a3cef8 #5615 - update documentation and use non-encoded versions for ASCII characters in get_lstring
- 7f41d61 use some suggestions from #5615
- 0516163 remove deprecated escape string from Julia bindings
- cd8d8bb Fix runtime search path for shared-lib and add '-static' to the name of static-lib. (#5616)
- f05ac8a updated C++ API for escaped and unescaped strings #5615
- 05e7ed9 add API to access unescaped strings, update documentation of Z3_get_lstring, #5615
- 6eed885 print bounded terms for better efficiency
- 13da6a0 add handling of quantifiers #5612
- 839a085 Merge branch 'master' of https://github.com/z3prover/z3
- 86147d0 #5605
- f9dde2e #5605
- 3557e0b Added eq/fixed/final functions in C++ user propagator as methods (#5607)
- fc3a701 push-pop
- d5e5dcf add nff and auto-relevant
- bc2020a #5604
- 115203e fixes to sat.euf ematching #5573
- f78546c fixed bug of computing butlast of a sequence (#5602)
- fb9fa1b updated printer
- cb120c9 Regex range bug fix (#5601)
- 6302b86 tweak GC in OCaml bindings (#5600)
- f60ed2c #5591
- 7b34131 #5593
- fd77f0c fix #5594
- 96e117d Update smt_context.cpp
- c15968a fix #4901
- 9a76bf0 #5591
- 58fd4fc Merge pull request #5550 from wintersteiger/cwinter_fpa_fixes
- 52032b9 #5467
- b471ebd Revert "Fix off-by-one in fp.div bit-blasting. Inspired by #4841 but doesn't quite fix it."
- 738783a Fix off-by-one in fp.div bit-blasting. Inspired by #4841 but doesn't quite fix it.
- c24f438 Fix for mk_to_fp_float; pertains to #4841
- 00e8ea7 Make terms that are internalized on the fly relevant
- 8e69f76 Add additional equality in theory_fpa
- f1acc4b Make fpa2bv debug symbol names optional
- 515a2a7 Whitespace
- e8d6d97 Refine fpa_decl_plugin::is_unique_value
- 12c3266 Fix error messsages
- c3549ec na
- 73102cf fix #5589
- 75702c3 na
- f7a2d08 Update README.md
- 88c3119 Create android-build.yml (#5588)
- 0fc9f1d fix max/min length to handle concatenation
- f1b8376 Rename 'user' to 'user_solver' #5586 (#5587)
- bfa960c fix internalize regression
- 6f55971 Newderiv (#5585)
- 146f462 Updated regex derivative engine (#5567)
- c0c3e68 disable all propagation until ematch incompleteness is fixed
- 94cc4ea remove arith_lhs simplification from preamble tactic
- 33f4e65 redo bindings/fingerprints
- 281fb67 unit propagate with fingerprints
- 8a85cfd fix #5579 -
- cbe7dd4 missing continue fixes unsound sat result from #5573
- ff723f1 Update z3++.h
- 62fd22f disable macro finder tactic if there are recursive functions fix #5574
- 137e5c5 fix tmp_eq
- 67ae75b fix tmp_eq
- da124e4 tune q-eval and q-ematch
- 92c1b60 tuning eval
- 2e176a0 count lazy bindings
- 3abecc3 add extra commands to API parser
- 6c71baf lifting iff to binary
- 1dcbd2d Correct capitalization of package (#5569)
- d174f87 #5532
- 18d1b36 #5532
- cabd5b1 #5532
- de20bff import goodies from ps
- 708602d fix #5560 - add a throttle on maximal size of bignums created for propagate-value lemmas
- 2e96557 fix #5560 - add a throttle on maximal size of bignums created for propagate-value lemmas
- 2c266a9 #5545
- 1352aa0 #5532
- 0170f1f #5532
- fd79908 fix build
- 6f31d83 fix #5541
- 4263063 CNF conversion refactoring (#5547)
- 91fb646 Fix Z3Config.cmake.in when generating a static library (#5555)
- d36c3fa #4880 add interpreted versions of to_bv functions for MBQI quantifier models
- 1fc7b63 ...
- cef964f fixes for model converter default case
- fe3f139 na
- c3c5c14 prepa...