z3-4.11.2
版本发布时间: 2022-09-04 08:28:04
Z3Prover/z3最新发布版本:z3-4.13.0(2024-03-08 03:21:18)
4.11.2 release
Changes:
- 8e6f17ebd011a352b3e67fcec03dcd4378a1472c inc version
- 1382cdefea3cf595cea3ca03f752277c696f741d release notes
- 85c8168af5caa17fb5c6d441c8d16b14ea573c0b use for pattern instead of iterators
- 60967efd3803ddee4515ca7820da8e9e48af9386 fix wrong condition for delayed bit-blasting
- 0bdb2f16910779f02af3d401cb589c11f847743f add verbose=1 log for mbp failure
- 7e1e64d027b2d44c5b17e3ea4b8d82c002760175 fix #6313
- 9dca8d18ed9711ad14e12cb4176454c38bbbc355 fix negative contains bug (#6312)
- e4ef1717e3a7b30fc87a4959dd80195a519721a2 fix variable tracking bug in explanations with literals
- eb1ea9482edf11a7136bfeb9d5da15d26bb889e8 detect nested as-array in model values
- eb2b95e5fe0ab226fa50dd91ffd5fa90f2e5a8bc spacer: trying to make C++ happy
See More
- f2afb369bdf63c8db5dffc395aa2accfb0b96f73 extend distinct check to ADT
- 61f7dc3513dcf521db60b7304b75e21edee80812 remove creation of trivial testers
- 46383a08111609e8f4d41a2b1398bd203d1b4084 AG - unary datatypes, tester always is true.
- ac5b190a72303e33bdcf07828c1002ffdc26632e track instantiations from MBQI in proof logging for new solver
- d3e6ba9f98bd455239ad51bc0a2167fa64dbf72a remove union
- 3011b34b3b87ca0bfe20cc7c7471dfd1d2a127a4 log E-matching based quantifier instantiations as hints
- 6077c4154a5fa251975d9c828ed25ed893f419d5 #6116 bv2int bug fix
- f72cdda5fb5b482fe61768ca9f17a3f07838d50c Change to 4 digit assembly version (#6297)
- 4abff18e8d41b5e1ae9357b3c11d564eb17791d5 fill in missing pieces of proof hint checker for Farkas and RUP
- d2b618df23364369ba583bce1c392dd8412d4f5f Spacer Global Guidance (#6026) [ #3 ]
- 1a79d92f3a071739eb0be63bb3196e1e7e65d607 revert last ditch array
- 36d76a5bb2f5d2ead1c1a4823bcc3bde95d8c70b fix #6304
- 45d8d73fce8409a6e9ac71c86abde1fb3a0cdba0 #6303
- 0f475f45b5adc62de1172f2ab2ba2e1dd64a81ac Add RUP checking mode to proof checker.
- 8cb118235aa94588012510483327d03cf3f826b0 add missing status case for cancelation
- cd0af999a824cbcc2478639b400e2c788b9393d1 fix #6302
- dd906893394344d7a68ea38f57ec83195744f81b build fixes
- 6f2a6da600c3a5f0cb756052b7a41a62bb120b93 address unused variable warnings
- 4d29925c3fbbfbe8ab998fa0c383353cbb7bcf85 build fixes
- 8b8caf9dedc41f38a8c16d024cecfe27beee6909 re-add smt-solver for proof_cmds
- 37fab88de006c6b625d9d67f4b94fff8da42716f respect dependencies, move proof_cmds to extra_cmds
- f65a244385b18eeb33cced8eb11f355cebb5eb5f move proof_cmds
- f5d2b9b89a4a45ba33bd187efcb462b6070f8d88 fix typo in comment defining macros (#6306)
- a0ca5d745e6cefc93358b18ff29774ec569c96f8 Fixed nested user-propagator callbacks in .NET (#6307)
- e2f4fc23076032935daa85e305d0453dc1470d73 overhaul of proof format for new solver
- 9922c766b960b79178596d2dff64b72b3e28bad7 add extra information for type error message
- dd91fab6f434aff5aef0db7886a23f8ddc90c261 Merge branch 'master' of https://github.com/Z3Prover/z3
- 159026b5e878a4ffee771725e0262754ace15c0d regression fix to ackerman gc and memory smash, perf fix for handling bv2int axioms, perf fix for filtering ackerman
- 458f417f44c1ef53f352899bb317e6367982fd7d move drat functionality into euf
- 1ffbe23ee3e85dd8b4cba81a3481d8e3158f6115 add virtual destructor to fix build
- 1894c86ee015eafbacb0730d44d625034271d6e4 virtual
- ca0a82952fa551668d53583eedd5b27a60c55c45 add function pointer to class to see how MacOs build reacts
- 0d7b7a417a3b3743546324af43d154cfe8d09c17 selectively re-add solver_params
- 5f2387b3be9ea974bd95b17899d099fd7344c293 revert some changes that coincide with breaking macos build
- a628e4c4e5cbb5db727f643c647302eec77e370c updates to printer to get instantiations, take 1
- f0eee41ab987c8b34b03687a87a2bcaa365c8373 include depenency
- 6c165e89dcc88da56f7fdc8a51349478f0574947 #6299
- f6e151a49cab91f31c24f838bea8d8df5be2d742 assert
- d975886cdcfc9e03107bf17e666938582a13dfa8 fix #6300
- fb8532bf55a63e9cb53cbe7d3d4aa825ed73bccb succinct logging
- 74c61f49b4fbdcc4920a62253eaed0c6cac26aa0 move std::function to header of sat-drat - alignment?
- c6263587c3a1f44849802ad3875e5c9e40086270 fix validator bug returning true for unprocessed case, bug reported in #6116
- ce1f3987d9ad2a9141e9e6d2d66cdd9dadf59427 fix unsoundness in quantifier propagation #6116 and add initial lemma logging
- 912b284602d8efda658de4706405e7f3fedc9b57 disable validate_hint too permissive
- 2f8b13368da6685f569c83949cb0259bd09cdf8f add redirect for warnings
- fbf9e3004f870749694c9f9c4494293f286a8959 ack
- fbfb28eba958d34974f373f957533c4d808a52d3 update release notes
- 916d1dbb137cb5192ec9099f1e5487c68844fbed fix default parameter regression
- 7ab904bfc61a6ee38d95d3d8c48a8dbfbaf52559 remove spurious file
- 0eea021dc32761a1dd854fd6dfa27427b12080fb include global parameters and fixup for HTML meta-characters
- f6e4a45f4beddb1b213f3233527777aed681a0bd Merge branch 'master' of https://github.com/z3prover/z3
- 64e0e785e786a1baa2bf4e32dfe16727bd11ad25 #5953
- 09ab575d2933531449e30955e67ccac2c79c3807 parens
- daa24ef4ced30c2d9164c8907471cc49504fd0b1 add missing error check
- 9eb4237dfe23a70ec15b5e55b6ee2688d1ef46bd fix #6292
- a38308792efceb062fd1b9d5ad6c52ef9a47f552 #6288
- 409230259095bdc157321c5bdc2d8644f1157fda use interface for creating unary equalities
- 17fc43847623bff8a0a3e2fb1ebfbd6719e6d23a don't have bv-ackerman influence simplification
- be0cd74c71eb3e6f9709fb05e5aba78ba13ec35f #6289
- 2181a0ff7464ab4c6a140d258d6f1ad36689b501 #6289
- 56fb1615327b75567bbf2b3c5c64806f7ba6d9ff ADT-constructor generation crashed in .NET/Java when no (= default) fields are given (#6287)
- 6ba9ada1e2d4aefd6cbe0602b743124b40e11628 Fix typos. (#6291)
- 706f7fbdc786509169abbb8483f055da9e1689e7 Fix some warnings about unused stuff. (#6290)
- d5d77dfe642181d61f033be508daba2fc88bb286 minor code simplifications
- 08bf7a62933c787c5184b64727a849b551ecf2a2 fix name
- 665ef2c6bae91fb13e7cf4f9aab37b89d08c473a add missing new
- bb5d81195c124f74906da83c4a58e03c3624f14b use equalities
- b26420ed997a6a064b8fdb243e7d2d07541a321a #6285
- ea8b118eb1c50a3ca1138af5d1b4c34d7d77fa85 Android CI: Configure with CMAKE_ANDROID_API (#6284)
- e83a70f9ad2153d480118b7d384e9016fe00dc02 add newlines for description
- 514eaf33aae719e750be664940a00774fef3cf38 Merge branch 'master' of https://github.com/z3prover/z3
- 600b4491aa7c21d101098e699a6d25073dde6216 don't forget parameter documentation
- 540e36e6cba7501a0b3f86e246cbaade20f35f2e roll version number
This list of changes was auto generated.
1、 CodeSignSummary-433d3772-a9cf-4468-824f-e0e16f0bdea5.md 383B
2、 CodeSignSummary-540ed51d-78b3-4381-94f2-2e280104aead.md 383B
3、 CodeSignSummary-90477d83-f97f-49fd-b161-8955bd10f567.md 383B
4、 CodeSignSummary-eb019d1f-ba4a-41fc-9da4-ad9123be08da.md 383B
5、 Microsoft.Z3.4.11.2.nupkg 28.04MB
6、 Microsoft.Z3.4.11.2.snupkg 39.69MB
7、 Microsoft.Z3.x86.4.11.2.nupkg 5.52MB
8、 Microsoft.Z3.x86.4.11.2.snupkg 34.22MB
9、 z3-4.11.2-arm64-osx-11.0.zip 31.57MB
10、 z3-4.11.2-x64-glibc-2.31.zip 43.57MB
11、 z3-4.11.2-x64-osx-10.16.zip 34.23MB
12、 z3-4.11.2-x64-win.zip 52.51MB
13、 z3-4.11.2-x86-win.zip 44.67MB
14、 z3-solver-4.11.2.0.tar.gz 4.51MB
15、 z3doc.zip 10.25MB
16、 z3_solver-4.11.2.0-py2.py3-none-macosx_10_16_x86_64.whl 27.76MB
17、 z3_solver-4.11.2.0-py2.py3-none-macosx_11_0_arm64.whl 24.95MB
18、 z3_solver-4.11.2.0-py2.py3-none-manylinux1_x86_64.whl 51.31MB
19、 z3_solver-4.11.2.0-py2.py3-none-win32.whl 50.9MB
20、 z3_solver-4.11.2.0-py2.py3-none-win_amd64.whl 53.58MB