Downloads of v 4.3.2:


Last Update:

24 Jan 2015

Package Maintainer(s):

Software Author(s):

  • Microsoft Research


z3 smt solver smtlib theorem prover constraint

Z3 Theorem Prover

  • 1
  • 2
  • 3

4.3.2 | Updated: 24 Jan 2015



Downloads of v 4.3.2:



Software Author(s):

  • Microsoft Research

  • 1
  • 2
  • 3
Z3 Theorem Prover 4.3.2

  • 1
  • 2
  • 3

Some Checks Have Failed or Are Not Yet Complete

Not All Tests Have Passed

Validation Testing Unknown

Verification Testing Failed


Scan Testing Successful:

No detections found in any package files


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

  • 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 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

3. Enter your internal repository url

(this should look similar to

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'"

Write-Verbose "Exit code was $exitCode"
$validExitCodes = @(0, 1605, 1614, 1641, 3010)
if ($validExitCodes -contains $exitCode) {
  Exit 0

Exit $exitCode

- name: Ensure z3 installed
    name: z3
    state: present
    version: 4.3.2
    source: STEP 3 URL

See docs at

chocolatey_package 'z3' do
  action    :install
  version  '4.3.2'
  source   'STEP 3 URL'

See docs at

    Name: z3,
    Version: 4.3.2,
    Source: STEP 3 URL

Requires Otter Chocolatey Extension. See docs at

cChocoPackageInstaller z3
   Name     = 'z3'
   Ensure   = 'Present'
   Version  = '4.3.2'
   Source   = 'STEP 3 URL'

Requires cChoco DSC Resource. See docs at

package { 'z3':
  provider => 'chocolatey',
  ensure   => '4.3.2',
  source   => 'STEP 3 URL',

Requires Puppet Chocolatey Provider module. See docs at

salt '*' chocolatey.install z3 version="4.3.2" source="STEP 3 URL"

See docs at

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 = ''
$url64 = ''

Install-ChocolateyZipPackage "$packageName" "$url" "$(Split-Path -parent $MyInvocation.MyCommand.Definition)" "$url64"

Log in or click on link to see number of positives.

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

  • 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 the script. Example: python scripts/ --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
  • 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)
    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
    instead of
    We say may because 'F' may have other unsatisfiable cores.
  • Fixed bug reported at
  • Fixed timers on Linux and FreeBSD.
  • Fixed crash reported at
  • Fixed bug reported at
  • Relax check_logic procedure. Now, it accepts coercions (to_real) automatically introduced by Z3. (Thanks to Paul Jackson). This is a fix for
  • Fixed
  • Fixed bugs in the C++ API (Thanks to Andrey Kupriyanov).
  • Fixed bug reported at (Thanks to Paul Jackson).
  • Fixed bug reported at (Thanks to Tianhai Liu).

This package has no dependencies.

Discussion for the Z3 Theorem Prover Package

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.
comments powered by Disqus