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

Z3 Theorem Prover

4.3.2 | Updated: 24 Jan 2015

Downloads:

1,009

Downloads of v 4.3.2:

1,009

Maintainer(s):

Software Author(s):

  • Microsoft Research

Tags:

z3 smt solver smtlib theorem prover constraint

Z3 Theorem Prover 4.3.2

Some Checks Have Failed or Are Not Yet Complete

1 Test Unknown and 1 Failing Test

Hide Checks
Hide Checks

Validation Testing Unknown

Verification Testing Failed

Details

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

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.

Description

Z3 is a high-performance theorem prover being developed at Microsoft Research.

tools\chocolateyInstall.ps1 
$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.

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

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