MyGit

z3-4.11.2

Z3Prover/z3

版本发布时间: 2022-09-04 08:28:04

Z3Prover/z3最新发布版本:z3-4.13.0(2024-03-08 03:21:18)

4.11.2 release

Changes:

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.

相关地址:原始地址 下载(tar) 下载(zip)

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

查看:2022-09-04发行的版本