| Index | index by Group | index by Distribution | index by Vendor | index by creation date | index by Name | Mirrors | Help | Search |
| Name: python314-z3 | Distribution: openSUSE Tumbleweed |
| Version: 5.0.0 | Vendor: openSUSE |
| Release: 1.1 | Build date: Thu Jul 23 12:27:47 2026 |
| Group: Productivity/Scientific/Other | Build host: reproducible |
| Size: 2408737 | Source RPM: z3-5.0.0-1.1.src.rpm |
| Packager: https://bugs.opensuse.org | |
| Url: https://github.com/Z3Prover/z3/wiki | |
| Summary: Python bindings for z3 | |
Z3 is a theorem prover from Microsoft Research. Python bindings for the module.
MIT
* Thu Jul 23 2026 Jiri Slaby <jslaby@suse.cz>
- update to 5.0.0:
* see: https://github.com/Z3Prover/z3/releases/tag/z3-5.0.0
* Thu Mar 12 2026 Matej Cepl <mcepl@cepl.eu>
- Update to 4.16.0:
- Add Go bindings to supported APIs
- Update to 4.15.8:
- Fix release pipeline to publish all supported python
wheels properly.
- Re-enable npm tokens for publishing npm pacages.
- Update to 4.15.7:
- Bug fix release
- Update to 4.15.6:
- Optimize mpz (multi-precision integer) implementation
using pointer tagging to reduce memory footprint and
improve performance. #8447, thanks to Nuno Lopes.
- Fix macOS install_name_tool issue by adding
- Wl,-headerpad_max_install_names linker flag to all dylib
builds. Resolves "larger updated load commands do not fit"
errors when modifying library install names on macOS.
[#8535], fixes #7623
- Optimize parameter storage by storing rational values
directly in variant instead of using pointers. Thanks to
Nuno Lopes. #8518
- Update to 4.15.5:
- NLSAT now uses the Level wise algorithm for projection.
https://arxiv.org/abs/2212.09309
- Add RCF (Real Closed Field) API to TypeScript bindings,
achieving feature parity with Python, Java, C++, and C#
implementations. The API includes 38 functions for exact
real arithmetic with support for π, e, algebraic roots,
and infinitesimals. #8225
- Add sequence higher-order functions (map, fold) to Java,
C#, and TypeScript APIs. Functions include SeqMap,
SeqMapi, SeqFoldl, and SeqFoldli for functional
programming patterns over sequences.
Java API: #8226
C# API: #8227
TypeScript API included in #8228
- Add benchmark export functionality to C# and TypeScript
APIs for exporting solver problems as SMTLIB2 benchmarks.
[#8228]
- Fix UNKNOWN bug in search tree with inconsistent end state
during nonchronological backjumping. The fix ensures all
node closing occurs in backtrack to maintain consistency
between search tree and batch manager state. Thanks to
Ilana Shapiro. #8214
- Fix segmentation fault in dioph_eq.cpp when processing
UFNIRA problems without explicit set-logic declarations.
Added bounds checks before accessing empty column vectors.
[#8218], fixes #8208
- Migrate build and release infrastructure from Azure
Pipelines to GitHub Actions, including CI workflows,
nightly builds, and release packaging.
- Bug fixes including #8195
- Add functional datatype update operation to language
bindings. The datatype_update_field function enables
immutable updates to datatype fields, returning a modified
copy while preserving the original datatype value. #8500
- Add comprehensive regex support to TypeScript API with 21
functions including Re, Loop, Range, Union, Intersect,
Complement, and character class operations. Enables
pattern matching and regular expression constraints in
TypeScript applications. #8499
- Add move constructor and move assignment operator to
z3::context class for efficient resource transfer. Enables
move semantics for context objects while maintaining
safety with explicit checks against moved-from usage.
[#8508]
- Add solve_for and import_model_converter functions to C++
solver API, achieving parity with Python API for LRA
variable solving. #8465
- Add missing solver APIs to Java and C# bindings including
add_string, set_phase, get_units, get_non_units, and
get_levels methods. #8464
- Add polymorphic datatype APIs to Java and ML bindings for
creating and manipulating parameterized datatypes. #8438,
[#8378] #8507, #8467, #8494
- Add SLS (Stochastic Local Search) tactic as a separate
worker thread for parallel solving. Thanks to Ilana
Shapiro. #8263
- Add Windows ARM64 platform support for Python wheels,
expanding platform coverage for ARM-based Windows systems.
[#8280]
- Optimize bitvector operations for large bitwidths by
avoiding unnecessary power-of-two computations in
has_sign_bit and mod2k operations. Thanks to Nuno Lopes.
- Optimize linear arithmetic solver with throttled
patch_basic_columns() calls, especially beneficial for
unsatisfiable cases. Thanks to Lev Nachmanson.
- Fix memory leak in undo_fixed_column when handling big
number cleanup. Thanks to Lev Nachmanson.
- Fix assertion violation in mpzzp_manager::eq from
non-normalized values during fresh variable peeking. #8439
- Fix memory corruption in Z3_polynomial_subresultants API
where allocating result vector corrupted internal
converter mappings. Restructured to complete polynomial
computation before allocation. #8264, thanks to Lev
Nachmanson.
- Fix missing newline after attributes in
benchmark_to_smtlib_string output formatting. Thanks to
Josh Berdine. #8276
- Fix NuGet packaging to handle dynamic glibc versions
across different Linux distributions. #8474
- Preserve initial solver state with push/pop operations for
multiple objectives optimization. Thanks to Lev
Nachmanson. #8264
* Wed Mar 11 2026 Matej Cepl <mcepl@cepl.eu>
- Add support for generating of multiple versions of Python
subpackages (using %python_subpackage_only).
- Add python-z3-pyproject.toml and python-z3-setup.py for that.
* Tue Feb 24 2026 Jiri Slaby <jslaby@suse.cz>
- add _constraints as ppc64le failed with "No space left on device"
* Sat Jan 03 2026 Dirk Müller <dmueller@suse.com>
- update to 4.15.4:
* see: https://github.com/Z3Prover/z3/releases/tag/z3-4.15.4
* Fri May 30 2025 Jiri Slaby <jslaby@suse.cz>
- add python-use-non-devel-so.patch (bsc#1243028)
* Fri May 30 2025 Jiri Slaby <jslaby@suse.cz>
- update to 4.15.0
* see: https://github.com/Z3Prover/z3/releases/tag/z3-4.15.0
* Fri Mar 28 2025 Jiri Slaby <jslaby@suse.cz>
- update to 4.14.1
* Add ubv_to_int, sbv_to_int, int_to_bv to SMTLIB2 API.
* Fix nuget package regression omitting Microsoft.Z3.* files
* SLS modulo theories engine v1 release.
* API for accessing term depth and groundness.
* Two fixes to relevancy propagation.
* A new API for solving LRA variables modulo constraints.
* Performance and bug fixes.
* several updates to emscripten including #7473
* add preliminary pyodie build
* address issues with Java bindings
* Include start of sls-smt functionality SLS modulo theories
* Mon Oct 14 2024 Jiri Slaby <jslaby@suse.cz>
- build with g++-13 on < 1600 (z3 needs c++20)
* Sat Oct 12 2024 Andrea Manzini <andrea.manzini@suse.com>
- update to 4.13.3:
* Fixes, including #7363
* Fix paths to Java binaries in release
* Remove internal build names from pypi wheels
* Performance regression fix. #7404
* single-sample cell projection in nlsat
* using simple-checker together with and variable ordering
The projection is described in paper by Haokun Li and Bican Xia,
Solving Satisfiability of Polynomial Formulas By Sample - Cell Projection.
The code ported from https://github.com/hybridSMT/hybridSMT.git
* Add API for providing hints for the solver/optimize contexts for which
initial values to attempt to use for variables. The new API function are
Z3_solver_set_initial_value and Z3_optimize_set_initial_value, respectively.
* Fri Apr 12 2024 Andreas Stieger <andreas.stieger@gmx.de>
- includes changes from 4.13.0:
* remove expensive rewrite that coalesces adjacent stores
* improved Java use of reference queues
* fixes to conditional import of python library
* include universe for constants that get removed during
pre-processing
* code improvements
* fix nested callback handling for user propagators
* added Julia API
* Thu Feb 22 2024 Jiri Slaby <jslaby@suse.cz>
- update to 4.12.5
* track quantifier instantiation method in proof hint #7080
* prepare for release
* free memory the clean way
* encapsulate anum functionality
* encapsulate mpz a bit more
* Fixes in Java's User Propagator (#7088)
* remove unused code
* take care of strategy undecided, Nikolaj's comments
* Merge branch 'master' of https://github.com/z3prover/z3
* force int bound on int columns, call term_is_int() after subst
* pin expression passed to validate_eq
* Update z3_api.h
* fix #7081
* fix #7085
* fix #7084
* change the definition of Gomory row
* and more
- remove 0001-Fix-building-with-gcc-13-6723.patch (upstream)
* Thu Jun 15 2023 Jiri Slaby <jslaby@suse.cz>
- update to 4.12.2
* remove MSF (Microsoft Solver Foundation) plugin.
* updated propagate-ineqs tactic and implementing it as a simplifier,
bound_simplifier.
* add API function Z3_mk_real_int64 to take two int64 as arguments. The
Z3_mk_real function takes integers.
* Add _simplifiers_ as optional incremental pre-processing to solvers.
* Optimize added to JS API.
* SMTLIB2 proposal for bit-vector overflow predicates added.
* bug fixes.
- add 0001-Fix-building-with-gcc-13-6723.patch
* Sat Jan 21 2023 Dirk Müller <dmueller@suse.com>
- update to 4.12.1:
* change macos build to use explicit reference to Macos version 11. Hosted
builds are migrating to macos-12 and it broke a user Issue #6539.
* Tue Jan 17 2023 Andrea Manzini <andrea.manzini@suse.com>
- update to 4.12.0
* move bound_manager to simplifiers, add bound manager to extract_eqs for solve-eqs
* fix memory leak on proof justifications
* expose parameters to control behavior for
* many bugfixes, see https://github.com/Z3Prover/z3/releases
/usr/lib/python3.14/site-packages/z3 /usr/lib/python3.14/site-packages/z3/__init__.py /usr/lib/python3.14/site-packages/z3/__pycache__ /usr/lib/python3.14/site-packages/z3/__pycache__/__init__.cpython-314.opt-1.pyc /usr/lib/python3.14/site-packages/z3/__pycache__/__init__.cpython-314.pyc /usr/lib/python3.14/site-packages/z3/__pycache__/z3.cpython-314.opt-1.pyc /usr/lib/python3.14/site-packages/z3/__pycache__/z3.cpython-314.pyc /usr/lib/python3.14/site-packages/z3/__pycache__/z3consts.cpython-314.opt-1.pyc /usr/lib/python3.14/site-packages/z3/__pycache__/z3consts.cpython-314.pyc /usr/lib/python3.14/site-packages/z3/__pycache__/z3core.cpython-314.opt-1.pyc /usr/lib/python3.14/site-packages/z3/__pycache__/z3core.cpython-314.pyc /usr/lib/python3.14/site-packages/z3/__pycache__/z3num.cpython-314.opt-1.pyc /usr/lib/python3.14/site-packages/z3/__pycache__/z3num.cpython-314.pyc /usr/lib/python3.14/site-packages/z3/__pycache__/z3poly.cpython-314.opt-1.pyc /usr/lib/python3.14/site-packages/z3/__pycache__/z3poly.cpython-314.pyc /usr/lib/python3.14/site-packages/z3/__pycache__/z3printer.cpython-314.opt-1.pyc /usr/lib/python3.14/site-packages/z3/__pycache__/z3printer.cpython-314.pyc /usr/lib/python3.14/site-packages/z3/__pycache__/z3rcf.cpython-314.opt-1.pyc /usr/lib/python3.14/site-packages/z3/__pycache__/z3rcf.cpython-314.pyc /usr/lib/python3.14/site-packages/z3/__pycache__/z3regex.cpython-314.opt-1.pyc /usr/lib/python3.14/site-packages/z3/__pycache__/z3regex.cpython-314.pyc /usr/lib/python3.14/site-packages/z3/__pycache__/z3types.cpython-314.opt-1.pyc /usr/lib/python3.14/site-packages/z3/__pycache__/z3types.cpython-314.pyc /usr/lib/python3.14/site-packages/z3/__pycache__/z3util.cpython-314.opt-1.pyc /usr/lib/python3.14/site-packages/z3/__pycache__/z3util.cpython-314.pyc /usr/lib/python3.14/site-packages/z3/z3.py /usr/lib/python3.14/site-packages/z3/z3consts.py /usr/lib/python3.14/site-packages/z3/z3core.py /usr/lib/python3.14/site-packages/z3/z3num.py /usr/lib/python3.14/site-packages/z3/z3poly.py /usr/lib/python3.14/site-packages/z3/z3printer.py /usr/lib/python3.14/site-packages/z3/z3rcf.py /usr/lib/python3.14/site-packages/z3/z3regex.py /usr/lib/python3.14/site-packages/z3/z3types.py /usr/lib/python3.14/site-packages/z3/z3util.py /usr/lib/python3.14/site-packages/z3_solver-5.0.0.dist-info /usr/lib/python3.14/site-packages/z3_solver-5.0.0.dist-info/INSTALLER /usr/lib/python3.14/site-packages/z3_solver-5.0.0.dist-info/METADATA /usr/lib/python3.14/site-packages/z3_solver-5.0.0.dist-info/RECORD /usr/lib/python3.14/site-packages/z3_solver-5.0.0.dist-info/REQUESTED /usr/lib/python3.14/site-packages/z3_solver-5.0.0.dist-info/WHEEL /usr/lib/python3.14/site-packages/z3_solver-5.0.0.dist-info/top_level.txt /usr/share/doc/packages/python314-z3 /usr/share/doc/packages/python314-z3/README.md /usr/share/licenses/python314-z3 /usr/share/licenses/python314-z3/LICENSE.txt
Generated by rpm2html 1.8.1
Fabrice Bellet, Sat Aug 8 22:48:41 2026