Welcome to the Chocolatey Community Package Repository! The packages found in this section of the site are provided, maintained, and moderated by the community.
Every version of each package undergoes a rigorous moderation process before it goes live that typically includes:
- Security, consistency, and quality checking
- Installation testing
- Virus checking through VirusTotal
- Human moderators who give final review and sign off
If you are an organization using Chocolatey, we want your experience to be fully reliable. Due to the nature of this publicly offered repository, reliability cannot be guaranteed. Packages offered here are subject to distribution rights, which means they may need to reach out further to the internet to the official locations to download files at runtime.
Fortunately, distribution rights do not apply for internal use. With any edition of Chocolatey (including the free open source edition), you can host your own packages and cache or internalize existing community packages.
Your use of the packages on this site means you understand they are not supported or guaranteed in any way. Learn more...
Downloads of v 4.3.2:
24 Jan 2015
- Microsoft Research
Tags:z3 smt solver smtlib theorem prover constraint
Z3 Theorem Prover
4.3.2 | Updated: 24 Jan 2015
To edit the metadata for a package, please upload an updated version of the package.
Chocolatey's Community Package Repository currently does not allow updating package metadata on the website. This helps ensure that the package itself (and the source used to build the package) remains the one true source of package metadata.
This does require that you increment the package version.
Z3 Theorem Prover
Some Checks Have Failed or Are Not Yet Complete
Not All Tests Have Passed
This package was approved by moderator purity on 09 Feb 2015.
Z3 is a high-performance theorem prover being developed at Microsoft Research.
$packageName = 'z3' $url = 'http://z3.codeplex.com/downloads/get/923671' $url64 = 'http://z3.codeplex.com/downloads/get/923672' Install-ChocolateyZipPackage "$packageName" "$url" "$(Split-Path -parent $MyInvocation.MyCommand.Definition)" "$url64"
Log in or click on link to see number of positives.
- z18.104.22.168.nupkg (034956add92e) - ## / 56
- z3-4.3.2-x64-win.zip (7f93915ebb86) - ## / 55
- z3-4.3.2-x86-win.zip (eb72ab5321bb) - ## / 56
In cases where actual malware is found, the packages are subject to removal. Software sometimes has false positives. Moderators do not necessarily validate the safety of the underlying software, only that a package retrieves software from the official distribution point and/or validate embedded software against official distribution point (where distribution rights allow redistribution).
Chocolatey Pro provides runtime protection from possible malware.
|Z3 Theorem Prover 4.3.2||1363||Saturday, January 24, 2015||Approved|
Copyright (c) 2006-2015 Microsoft
- Added preliminary support for the theory of floating point numbers (tactics qffpa, qffpabv, and logics QF_FPA, QF_FPABV).
- Added the interpolation features of iZ3, which are now integrated into the Z3.
- Fixed a multitude of bugs and inconsistencies that were reported to us either in person, by email, or on Codeplex. Of those that we do have records of, we would like to express our gratitude to:
Vladimir Klebanov, Konrad Jamrozik, Nuno Lopes, Carsten Ruetz, Esteban Pavese, Tomer Weiss, Ilya Mironov, Gabriele Paganelli, Levent Erkok, Fabian Emmes, David Cok, Etienne Kneuss, Arlen Cox, Matt Lewis, Carsten Otto, Paul Jackson, David Monniaux, Markus Rabe, Martin Pluecker, Jasmin Blanchette, Jules Villard, Andrew Gacek, George Karpenkov, Joerg Pfaehler, and Pablo Aledo
as well as the following Codeplex users that either reported bugs or took part in discussions:
xor88, parno, gario, Bauna, GManNickG, hanwentao, dinu09, fhowar, Cici, chinissai, barak_cohen, tvalentyn, krikunts, sukyoung, daramos, snedunuri, rajtendulkar, sonertari, nick8325, dvitek, amdragon, Beatgodes, dmonniaux, nickolai, DameNingen, mangpo, ttsiodras, blurium, sbrickey, pcodemod, indranilsaha, apanda, hougaardj, yoff, EfForEffort, Ansotegui, scottgw, viorelpreoteasa, idudka, c2855337, gario, jnfoster, omarmrivas, switicus, vosandi, foens, yzwwf, Heizmann, znajem, ilyagri, hougaardj, cliguda, rgrig, 92c849c1ccc707173, edmcman, cipher1024, MichaelvW, hellok, n00b42, ic3guy, Adorf, tvcsantos, zilongwang, Elarnon, immspw, jbridge99, danliew, zverlov, petross, jmh93, dradorf, fniksic, Heyji, cxcfan, henningg, wxlfrank, rvprasad, MovGP0, jackie1015, cowang, ffaghih, sanpra1989, gzchenyin, baitman, xjtulixiangyang, andreis, trucnguyenlam, erizzi, hanhchi, qsp, windypan, vadave, gradanne, SamWot, gsingh93, manjeetdahiya, zverlov, RaLa, and regehr.
- New parameter setting infrastructure. Now, it is possible to set parameter for Z3 internal modules. Several parameter names changed. Execute
z3 -pfor the new parameter list.
- Added get_version() and get_version_string() to Z3Py
- Added support for FreeBSD. Z3 can be compiled on FreeBSD using g++.
- Added support for Python 3.x.
- Reverted to
(set-option :global-decls false)as the default. In Z3 4.3.0 and Z3 4.3.1, this option was set to true.
Thanks to Julien Henry for reporting this problem.
docdirectory and scripts for automatically generating the API documentation.
- Removed 'autoconf' dependency. We do not need to execute 'autoconf' and './configure' anymore to build Z3.
- Fixed incorrect result returned by Z3_solver_get_num_scopes. (Thanks to Herman Venter). This bug was introduced in Z3 4.3.0
- Java bindings. To enable them, we must use the option
--javawhen executing the
python scripts/mk_make.py --java
- Fixed crash when parsing incorrect formulas. The crash was introduced when support for "arithmetic coercions" was added in Z3 4.3.0.
- Added new option to mk_make to allow users to specify where python bindings (Z3Py) will be installed. (Thanks to Dejan Jovanovic for reporting the problem).
- Fixed crash reported at http://z3.codeplex.com/workitem/10
- Removed auxiliary constants created by the nnf tactic from Z3 models.
- Fixed problem in the pretty printer. It was not introducing quotes for attribute names such as |foo:10|.
- Fixed bug when using assumptions (Thanks to Philippe Suter and Etienne Kneuss)
Consider the following example:
If 'F' is unstatisfiable independently of the assumption 'a', and
the inconsistenty can be detected by just performing propagation,
Then, version<= 4.3.1 may return
We say may because 'F' may have other unsatisfiable cores.
- Fixed bug reported at http://stackoverflow.com/questions/13923316/unprintable-solver-model
- Fixed timers on Linux and FreeBSD.
- Fixed crash reported at http://z3.codeplex.com/workitem/11.
- Fixed bug reported at http://stackoverflow.com/questions/14307692/unknown-when-using-defs
- Relax check_logic procedure. Now, it accepts coercions (to_real) automatically introduced by Z3. (Thanks to Paul Jackson). This is a fix for http://z3.codeplex.com/workitem/19.
- Fixed http://stackoverflow.com/questions/14524316/z3-4-3-get-complete-model.
- Fixed bugs in the C++ API (Thanks to Andrey Kupriyanov).
- Fixed bug reported at http://z3.codeplex.com/workitem/23 (Thanks to Paul Jackson).
- Fixed bug reported at http://stackoverflow.com/questions/15226944/segmentation-fault-in-z3 (Thanks to Tianhai Liu).
This package has no dependencies.
- This discussion is only about Z3 Theorem Prover and the Z3 Theorem Prover package. If you have feedback for Chocolatey, please contact the Google Group.
- This discussion will carry over multiple versions. If you have a comment about a particular version, please note that in your comments.
- The maintainers of this Chocolatey Package will be notified about new comments that are posted to this Disqus thread, however, it is NOT a guarantee that you will get a response. If you do not hear back from the maintainers after posting a message below, please follow up by using the link on the left side of this page or follow this link to contact maintainers. If you still hear nothing back, please follow the package triage process.
- Tell us what you love about the package or Z3 Theorem Prover, or tell us what needs improvement.
- Share your experiences with the package, or extra configuration or gotchas that you've found.
- If you use a url, the comment will be flagged for moderation until you've been whitelisted. Disqus moderated comments are approved on a weekly schedule if not sooner. It could take between 1-5 days for your comment to show up.