| Index | index by Group | index by Distribution | index by Vendor | index by creation date | index by Name | Mirrors | Help | Search |
| Name: python3-z3 | Distribution: openSUSE Tumbleweed |
| Version: 4.15.0 | Vendor: openSUSE |
| Release: 1.2 | Build date: Fri May 30 10:22:16 2025 |
| Group: Development/Languages/Python | Build host: reproducible |
| Size: 641808 | Source RPM: z3-4.15.0-1.2.src.rpm |
| Packager: http://bugs.opensuse.org | |
| Url: https://github.com/Z3Prover/z3/wiki | |
| Summary: Python bindings for Z3 | |
Python bindings for the Z3 library.
MIT
* 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.13/site-packages/z3 /usr/lib/python3.13/site-packages/z3/__init__.py /usr/lib/python3.13/site-packages/z3/z3.py /usr/lib/python3.13/site-packages/z3/z3consts.py /usr/lib/python3.13/site-packages/z3/z3core.py /usr/lib/python3.13/site-packages/z3/z3num.py /usr/lib/python3.13/site-packages/z3/z3poly.py /usr/lib/python3.13/site-packages/z3/z3printer.py /usr/lib/python3.13/site-packages/z3/z3rcf.py /usr/lib/python3.13/site-packages/z3/z3test.py /usr/lib/python3.13/site-packages/z3/z3types.py /usr/lib/python3.13/site-packages/z3/z3util.py /usr/share/licenses/python3-z3 /usr/share/licenses/python3-z3/LICENSE.txt
Generated by rpm2html 1.8.1
Fabrice Bellet, Thu Mar 5 23:10:09 2026