z3-4.12.5

4.12.5 release

Changes:

• a7b564c update release scripts and notes
• 7486e87 track quantifier instantiation method in proof hint #7080
• 302ebff prepare for release
• e722dc7 add status badge for windows build, remove windows build from Azure pipelines
• 2dd45f8 add Windows build
• 910b302 free memory the clean way
• d32dcfc free memory the clean way
• 1754523 encapsulate anum functionality
• 548be4c add explicit move constructor to deal with unit test regression test-z3 algebraic on Windows/debug -
• a2993f7 encapsulate mpz a bit more

See More

• d2706ba Fixes in Java's User Propagator (#7088)
• 2c55aa5 remove unused code
• d084a19 take care of strategy undecided, Nikolaj's comments
• 6e9a938 Merge branch 'master' of https://github.com/z3prover/z3
• c591a7a force int bound on int columns, call term_is_int() after subst
• fef1596 pin expression passed to validate_eq
• 4f75153 Update z3_api.h
• c340233 fix #7081
• afba43a fix #7085
• 4ff352f fix #7084
• 91ca55e change the definition of Gomory row
• d8df203 remove an unused declaration
• e2fb4fb fix dependencies for Gomory polarity
• 2eadcf0 avoid duplicate explanations
• 7d7fef0 add explanations and fix polarity
• ddf2eb5 deleted parameter
• 3381fd2 spell check from microsoft/z3guide#165
• 2717159 Update sat_params.pyg
• 59b18d4 create as_bin as_hex wrappers for display
• 999e67d address Nikolaj's comments in Gomory cut
• 2d24436 remove a blank line
• 2b974a0 do not delay update for the polar case
• 2ac866a take the coefficient from cut_result, not lia
• 1b39290 try to remove version spec
• b239371 try to remove version spec
• aa4e1b3 update Julia versions
• 955c80e import updates from poly branch
• 2ca1187 fix a bug in polarity
• 75005d9 add validation option for debugging regressions
• 2934618 remove simplify_inequality from gomory.cpp
• 696b70f fix
• 239d68e return conflict on an empty term in Gomory cuts
• b75367f port improvements to arith rewriter
• a7bfdcd readd big cuts
• 84997f8 move a TRACE statement
• fd2b6c6 bug fix in gomory polarity
• d66df26 Fix some typos. (#7075)
• ec2b8eb Merge shared parts from polysat branch (#7063)
• 53c95e3 cleanup
• 0728b81 add parameter lp_settings.m_gomory_simplify
• 5796e88 use vector instead of unordered_map in gomory
• a3529a0 create bounds for gomory cuts with big numbers
• af76912 adding the polarity bound
• d7931b9 Bump microsoft/setup-msbuild from 1.1 to 1.3 (#7071)
• ebe5ebf Add branch and bound solver, for fun
• ad07e0e add sub and super-slice functionality directory to euf-bv-plugin
• cd331b8 remove reference to tactic.h
• 7adb402 add missing dependencies
• 5f45118 missing cmake list
• e321643 move sls core functionality to be independent of tactic
• 606a9a7 fix test build
• cab3c45 remove unnecessary parameter copies
• ab22e76 some code simplifications in mpn
• 4fe4234 bugfix on slack
• 766f5f0 reduce memory allocs in params
• ae1d927 improve add bin/item functions
• b09c237 rudimentary bin cover solver using the user propagator
• 68a2c08 Add Z3_get_estimated_alloc_size to OCaml API (#7068)
• 19f3ad4 fix the build
• e9fa7db revert smt_enode
• a00eb08 Merge branch 'master' of https://github.com/z3prover/z3
• 4317d13 refactor: move gomory functionaly from int_solver to gomory
• c4fa719 revert last two commits; MSVC doesn't like to statically allocate flexible arrays
• 6246c65 fix debug build
• c9c53b7 tmp_enode: don't heap allocate an app. store it inline instead.
• 4898a15 shrink ast's app by 8 bytes on 64-bit platforms when number of args > 0
• b2d5c24 remove a few string copies
• e28b644 remove an empty line
• d636561 change some TRACE statements
• db5a1a7 Bump actions/upload-artifact from 3 to 4 (#7065)
• 97d4508 Vector updates from polysat branch (#7066)
• 4c9f705 tptr: add pointer tagging templates (#7067)
• fcc7b25 remove a few string copies
• e5f52e2 Update Windows.yml
• d088fe9 Merge branch 'master' of https://github.com/z3prover/z3
• 9a18628 remove unnecessary assignments
• 5cafda1 remove reference to matrix bindings to see if it works
• 2602fc2 remove reference to matrix bindings to see if it works
• 1b75504 add path n prefix
• 00965cb fix string
• 394a355 fix string
• 9469f75 Update Windows.yml
• ea03b55 Update Windows.yml
• bb8ed43 Update Windows.yml
• ea44c11 gc expressions in the scope of updates, not old expressions
• 842385a Update Windows.yml
• 62ae9a0 Update Windows.yml
• 91ba893 Update Windows.yml
• ee073be Update Windows.yml
• c7c007c Update Windows.yml
• 9e3a489 Update Windows.yml
• 0dc8511 Create Windows.yml
• 13be3c3 reset model converter between rounds to elim-unconstrained.
• 0daa05a add ability to log selected bv rewrites
• dff419a pin expressions to fix unsound behavior
• 5d4c18d fixes
• 6d23847 fix typos
• d008dbe port Jakob's update to bv_internalize
• 085b5e2 port Jakob's update to union_find from polysat branch
• 2f2bf74 fixes to intblast encoding and more arithmetic rewriters
• bb99f44 fix bugs in elim-unconstr2 and fix bugs in intblast_solver
• 4867073 remove windowsArm64 from nightly
• d0a59f3 intblast with lazy expansion of shl, ashr, lshr
• 50e0fd3 Use noexcept more. (#7058)
• b44ab2f add rewriters for and
• 4778f27 revert to standard solver
• 9293923 Add intblast solver
• 0520558 port updated pdd from polysat
• 2e83352 Fix bug in fp.round_to_integral (#7060)
• e90a844 Use override more. (#7059)
• f6e69d4 Merge branch 'master' of https://github.com/z3prover/z3
• a2b490b Disable Python compilation cache during build (#7057)
• 7c2e4f2 fiddle with what gets added to win-arm64
• f7d9a5b Revert "Disable Python compilation cache during build (#7052)" (#7054)
• b40e301 fix #7053
• c20b8cb nightly
• 995b408 remove readme reference, add arm64 build to nightly
• 8293be8 Disable Python compilation cache during build (#7052)
• 3ebec56 tptr.h: Include <cstdint> once rather than twice. (#7051)
• 536f4f8 Merge branch 'master' of https://github.com/z3prover/z3
• 0f4e96a fix character
• 5fc039d nuget spec: does this work?
• 5732c3c add readme under content
• 91837c3 try adding readme again
• 70d4f32 port updates from poly/polysat
• e580c38 import updates to rational from polysat
• 575538d follow error message to put dependencies in setup args
• 4123405 add version
• 6282f40 try add name to project
• 7e716f7 try fix suggested in #7041
• 8e26c2a fix #7049
• 6cd619d kludge to fixup osver in python for Mac
• 4d1d067 fix divergence reported by Guido Martinez
• 6afed08 update minor version number
• fc23a49 a simple version of choosing a column for gomory cut

This list of changes was auto generated.