Welcome to the Chocolatey Community Package Repository! The packages found in this section of the site are provided, maintained, and moderated by the community.
Moderation
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
More detail at Security and Moderation.
Organizational Use
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.
Disclaimer
Your use of the packages on this site means you understand they are not supported or guaranteed in any way. Learn more...

Downloads:
1,009
Downloads of v 4.3.2:
1,009
Last Update:
24 Jan 2015
Package Maintainer(s):
Software Author(s):
- Microsoft Research
Tags:
z3 smt solver smtlib theorem prover constraint- Software Specific:
- Software Site
- Software License
- Package Specific:
- Possible Package Source
- Package outdated?
- Package broken?
- Contact Maintainers
- Contact Site Admins
- Software Vendor?
- Report Abuse
- Download

Z3 Theorem Prover
- Software Specific:
- Software Site
- Software License
- Package Specific:
- Possible Package Source
- Package outdated?
- Package broken?
- Contact Maintainers
- Contact Site Admins
- Software Vendor?
- Report Abuse
- Download
Downloads:
1,009
Downloads of v 4.3.2:
1,009
Maintainer(s):
Software Author(s):
- Microsoft Research
Edit Package
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.
Some Checks Have Failed or Are Not Yet Complete
1 Test Unknown and 1 Failing Test
To install Z3 Theorem Prover, run the following command from the command line or from PowerShell:
To upgrade Z3 Theorem Prover, run the following command from the command line or from PowerShell:
To uninstall Z3 Theorem Prover, run the following command from the command line or from PowerShell:
NOTE: This applies to both open source and commercial editions of Chocolatey.
1. Ensure you are set for organizational deployment
Please see the organizational deployment guide
2. Get the package into your environment-
Open Source or Commercial:
- Proxy Repository - Create a proxy nuget repository on Nexus, Artifactory Pro, or a proxy Chocolatey repository on ProGet. Point your upstream to https://chocolatey.org/api/v2. Packages cache on first access automatically. Make sure your choco clients are using your proxy repository as a source and NOT the default community repository. See source command for more information.
- You can also just download the package and push it to a repository Download
-
Open Source
- Download the Package Download
- Follow manual internalization instructions
-
Package Internalizer (C4B)
- Run
choco download z3 --internalize --source=https://chocolatey.org/api/v2
(additional options) - Run
choco push --source="'http://internal/odata/repo'"
for package and dependencies - Automate package internalization
- Run
3. Enter your internal repository url
(this should look similar to https://chocolatey.org/api/v2)
4. Choose your deployment method:
choco upgrade z3 -y --source="'STEP 3 URL'" [other options]
See options you can pass to upgrade.
See best practices for scripting.
Add this to a PowerShell script or use a Batch script with tools and in places where you are calling directly to Chocolatey. If you are integrating, keep in mind enhanced exit codes.
If you do use a PowerShell script, use the following to ensure bad exit codes are shown as failures:
choco upgrade z3 -y --source="'STEP 3 URL'"
$exitCode = $LASTEXITCODE
Write-Verbose "Exit code was $exitCode"
$validExitCodes = @(0, 1605, 1614, 1641, 3010)
if ($validExitCodes -contains $exitCode) {
Exit 0
}
Exit $exitCode
- name: Ensure z3 installed
win_chocolatey:
name: z3
state: present
version: 4.3.2
source: STEP 3 URL
See docs at https://docs.ansible.com/ansible/latest/modules/win_chocolatey_module.html.
Coming early 2020! Central Managment Reporting available now! More information...
chocolatey_package 'z3' do
action :install
version '4.3.2'
source 'STEP 3 URL'
end
See docs at https://docs.chef.io/resource_chocolatey_package.html.
Chocolatey::Ensure-Package
(
Name: z3,
Version: 4.3.2,
Source: STEP 3 URL
);
Requires Otter Chocolatey Extension. See docs at https://inedo.com/den/otter/chocolatey.
cChocoPackageInstaller z3
{
Name = 'z3'
Ensure = 'Present'
Version = '4.3.2'
Source = 'STEP 3 URL'
}
Requires cChoco DSC Resource. See docs at https://github.com/chocolatey/cChoco.
package { 'z3':
provider => 'chocolatey',
ensure => '4.3.2',
source => 'STEP 3 URL',
}
Requires Puppet Chocolatey Provider module. See docs at https://forge.puppet.com/puppetlabs/chocolatey.
salt '*' chocolatey.install z3 version="4.3.2" source="STEP 3 URL"
See docs at https://docs.saltstack.com/en/latest/ref/modules/all/salt.modules.chocolatey.html.
5. If applicable - Chocolatey configuration/installation
See infrastructure management matrix for Chocolatey configuration elements and examples.
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.
- z3.4.3.2.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.
Version | Downloads | Last Updated | Status |
---|---|---|---|
Z3 Theorem Prover 4.3.2 | 1009 | 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 -p
for 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. - Added
doc
directory 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
--java
when executing themk_make.py
script. Example: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:
(assert F)
(check-sat a)
(check-sat)
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
unsat
sat
instead of
unsat
unsat
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.
Ground Rules:
- 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.