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 of0
. - fe1e301 Remove Z3_bool, Z3_TRUE, Z3_FALSE from the API.
- 77e5d6a Use nullptr consistently instead of
0
orNULL
. - 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.