Downloads:
2,708
Downloads of v 4.3.2:
1,498
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
This is not the latest version of Z3 Theorem Prover available.
- 1
- 2
- 3
4.3.2 | Updated: 24 Jan 2015
- 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:
2,708
Downloads of v 4.3.2:
1,498
Maintainer(s):
Software Author(s):
- Microsoft Research
Z3 Theorem Prover 4.3.2
This is not the latest version of Z3 Theorem Prover available.
- 1
- 2
- 3
Some Checks Have Failed or Are Not Yet Complete
Not All Tests Have Passed
Deployment Method: Individual Install, Upgrade, & Uninstall
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:
Deployment Method:
This applies to both open source and commercial editions of Chocolatey.
1. Enter Your Internal Repository Url
(this should look similar to https://community.chocolatey.org/api/v2/)
2. Setup Your Environment
1. Ensure you are set for organizational deployment
Please see the organizational deployment guide
2. Get the package into your environment
Option 1: Cached Package (Unreliable, Requires Internet - Same As Community)-
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://community.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: (additional options)
choco download z3 --internalize --version=4.3.2 --source=https://community.chocolatey.org/api/v2/
-
For package and dependencies run:
choco push --source="'INTERNAL REPO URL'"
- Automate package internalization
-
Run: (additional options)
3. Copy Your Script
choco upgrade z3 -y --source="'INTERNAL REPO URL'" --version="'4.3.2'" [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="'INTERNAL REPO URL'" --version="'4.3.2'"
$exitCode = $LASTEXITCODE
Write-Verbose "Exit code was $exitCode"
$validExitCodes = @(0, 1605, 1614, 1641, 3010)
if ($validExitCodes -contains $exitCode) {
Exit 0
}
Exit $exitCode
- name: Install z3
win_chocolatey:
name: z3
version: '4.3.2'
source: INTERNAL REPO URL
state: present
See docs at https://docs.ansible.com/ansible/latest/modules/win_chocolatey_module.html.
chocolatey_package 'z3' do
action :install
source 'INTERNAL REPO URL'
version '4.3.2'
end
See docs at https://docs.chef.io/resource_chocolatey_package.html.
cChocoPackageInstaller z3
{
Name = "z3"
Version = "4.3.2"
Source = "INTERNAL REPO URL"
}
Requires cChoco DSC Resource. See docs at https://github.com/chocolatey/cChoco.
package { 'z3':
ensure => '4.3.2',
provider => 'chocolatey',
source => 'INTERNAL REPO URL',
}
Requires Puppet Chocolatey Provider module. See docs at https://forge.puppet.com/puppetlabs/chocolatey.
4. 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.
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.
Add to Builder | Version | Downloads | Last Updated | Status |
---|---|---|---|---|
Z3 Theorem Prover 4.13.0 | 27 | Thursday, March 7, 2024 | Approved | |
Z3 Theorem Prover 4.12.6 | 23 | Sunday, February 25, 2024 | Approved | |
Z3 Theorem Prover 4.12.5 | 58 | Wednesday, January 31, 2024 | Approved | |
Z3 Theorem Prover 4.12.4 | 9 | Sunday, February 25, 2024 | Approved | |
Z3 Theorem Prover 4.12.3 | 246 | Tuesday, December 5, 2023 | Approved | |
Z3 Theorem Prover 4.12.2 | 152 | Friday, May 12, 2023 | Approved | |
Z3 Theorem Prover 4.12.1 | 123 | Wednesday, January 18, 2023 | Approved | |
Z3 Theorem Prover 4.12.0 | 32 | Saturday, January 14, 2023 | Approved | |
Z3 Theorem Prover 4.11.2 | 92 | Sunday, September 4, 2022 | Approved | |
Z3 Theorem Prover 4.11.0 | 45 | Friday, August 19, 2022 | Approved | |
Z3 Theorem Prover 4.10.2 | 49 | Saturday, July 30, 2022 | Approved | |
Z3 Theorem Prover 4.10.1 | 37 | Friday, July 22, 2022 | Approved | |
Z3 Theorem Prover 4.9.1 | 59 | Wednesday, July 6, 2022 | Approved | |
Z3 Theorem Prover 4.8.17 | 88 | Thursday, May 5, 2022 | Approved | |
Z3 Theorem Prover 4.8.16 | 58 | Sunday, April 24, 2022 | Approved | |
Z3 Theorem Prover 4.8.15 | 63 | Monday, March 21, 2022 | Approved | |
Z3 Theorem Prover 4.8.14 | 49 | Thursday, March 17, 2022 | Approved | |
Z3 Theorem Prover 4.3.2 | 1498 | 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.