./math/z3, The Z3 theorem prover / SMT solver

[ CVSweb ] [ Homepage ] [ RSS ] [ Required by ] [ Add to tracker ]

Branch: CURRENT, Version: 4.14.0, Package name: z3-4.14.0, Maintainer: dholland

z3 is an open source theorem prover / SMT solver from Microsoft Research.

(SMT stands for "satisfiability modulo theories".)


Required to run:
[lang/ocaml] [math/ocaml-num] [lang/python37]

Required to build:
[pkgtools/cwrappers]

Master sites:

Filesize: 5704.93 KB

Version history: (Expand)

CVS history: (Expand)


   2025-02-26 10:59:42 by Thomas Klausner | Files touched by this commit (1) 
Log message:
z3: this now requires C++20
   2025-02-20 11:27:01 by Adam Ciarcinski | Files touched by this commit (6) | Package updated
Log message:
z3 py-z3: updated to 4.14.0

4.14.0

bump timeout for jobs
Update release.yml for Azure Pipelines
Update nightly.yaml for Azure Pipelines
Update azure-pipelines.yml for Azure Pipelines
fix unit test
convert def into expression tree
adjust solve_for to handle rationals
fixes to failure conditions for unification
remove verbose output
Add unification based projection function
   2024-08-13 11:21:07 by Adam Ciarcinski | Files touched by this commit (5) | Package updated
Log message:
z3 py-z3: updated to 4.13.0

Version 4.13.0

- add ARM64 wheels for Python, thanks to Steven Moy, smoy
   2024-03-31 00:10:48 by Havard Eidnes | Files touched by this commit (1) 
Log message:
math/z3: add mk/atomic64.mk, to make this build on NetBSD/macppc.
   2024-02-21 11:50:35 by Nia Alarie | Files touched by this commit (2) 
Log message:
z3: Requires a C++17 compiler
   2024-01-23 21:01:04 by Adam Ciarcinski | Files touched by this commit (5) | Package updated
Log message:
z3 py-z3: updated to 4.12.5

z3-4.12.5

update release scripts and notes
track quantifier instantiation method in proof hint
prepare for release
add status badge for windows build, remove windows build from Azure pipelines
add Windows build
free memory the clean way
free memory the clean way
encapsulate anum functionality
add explicit move constructor to deal with unit test regression test-z3 \ 
algebraic on Windows/debug -
encapsulate mpz a bit more
   2023-08-14 07:25:36 by Thomas Klausner | Files touched by this commit (1247) 
Log message:
*: recursive bump for Python 3.11 as new default
   2023-05-25 12:53:24 by Jonathan Perkin | Files touched by this commit (2) 
Log message:
z3: Avoid ambiguous function call.