From d7781ac96b250c9cdb90b65324acace150ed4a46 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Fri, 27 Dec 2024 11:42:08 -0700 Subject: [PATCH 01/30] Version 4.13.4 --- sources | 2 +- z3.spec | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/sources b/sources index 5d76ed9..979efb1 100644 --- a/sources +++ b/sources @@ -1 +1 @@ -SHA512 (z3-4.13.3.tar.gz) = c899f57d8cb5450801463b07cd651869d766a920e41a4beedc96c4978e940bfadff9af2fbbb5ba10f94f6742bb33f7abaca0a351f3e1803d778e84d735d6829e +SHA512 (z3-4.13.4.tar.gz) = fd554122f3bb65e5d6622e2e331546d24892dfd3e5310bc4e041bd1c61fecfe53dbb487e4b125d87367338cacc9e06f28c71f380aac5fe8a74f4b45aaa27b6ce diff --git a/z3.spec b/z3.spec index 885ec05..ae0a3c8 100644 --- a/z3.spec +++ b/z3.spec @@ -14,7 +14,7 @@ %global giturl https://github.com/Z3Prover/z3 Name: z3 -Version: 4.13.3 +Version: 4.13.4 Release: %autorelease Summary: Satisfiability Modulo Theories (SMT) solver From 4379c0be96b771d12248953ba53e896f09a70eac Mon Sep 17 00:00:00 2001 From: Jerry James Date: Wed, 15 Jan 2025 15:13:42 -0700 Subject: [PATCH 02/30] Move configuration steps to %conf --- z3.spec | 1 + 1 file changed, 1 insertion(+) diff --git a/z3.spec b/z3.spec index ae0a3c8..e913d54 100644 --- a/z3.spec +++ b/z3.spec @@ -156,6 +156,7 @@ Python 3 interface to z3. %patch -P0 -p1 %endif +%conf # Enable verbose builds, use Fedora CFLAGS, preserve timestamps when installing, # include the entire contents of the archives in the library, link the library # with the correct flags, and build the ocaml files with debuginfo. From 0e33bcfe81115b0a0612b00028b17d0eb9ff82f3 Mon Sep 17 00:00:00 2001 From: Fedora Release Engineering Date: Sun, 19 Jan 2025 16:39:17 +0000 Subject: [PATCH 03/30] Rebuilt for https://fedoraproject.org/wiki/Fedora_42_Mass_Rebuild From 91c848ba1e2f55e8b5a5bc11999c36855c4f45b7 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Wed, 29 Jan 2025 07:02:31 -0700 Subject: [PATCH 04/30] OCaml 5.2.1 rebuild for Fedora 41 - Version 4.13.4 --- sources | 2 +- z3.spec | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/sources b/sources index 5d76ed9..979efb1 100644 --- a/sources +++ b/sources @@ -1 +1 @@ -SHA512 (z3-4.13.3.tar.gz) = c899f57d8cb5450801463b07cd651869d766a920e41a4beedc96c4978e940bfadff9af2fbbb5ba10f94f6742bb33f7abaca0a351f3e1803d778e84d735d6829e +SHA512 (z3-4.13.4.tar.gz) = fd554122f3bb65e5d6622e2e331546d24892dfd3e5310bc4e041bd1c61fecfe53dbb487e4b125d87367338cacc9e06f28c71f380aac5fe8a74f4b45aaa27b6ce diff --git a/z3.spec b/z3.spec index 885ec05..ae0a3c8 100644 --- a/z3.spec +++ b/z3.spec @@ -14,7 +14,7 @@ %global giturl https://github.com/Z3Prover/z3 Name: z3 -Version: 4.13.3 +Version: 4.13.4 Release: %autorelease Summary: Satisfiability Modulo Theories (SMT) solver From b0d1169569a7096061218d382b5d6458d34f6982 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Tue, 4 Mar 2025 13:24:44 -0700 Subject: [PATCH 05/30] Version 4.14.0 --- sources | 2 +- z3.spec | 5 ++--- 2 files changed, 3 insertions(+), 4 deletions(-) diff --git a/sources b/sources index 979efb1..3cbf117 100644 --- a/sources +++ b/sources @@ -1 +1 @@ -SHA512 (z3-4.13.4.tar.gz) = fd554122f3bb65e5d6622e2e331546d24892dfd3e5310bc4e041bd1c61fecfe53dbb487e4b125d87367338cacc9e06f28c71f380aac5fe8a74f4b45aaa27b6ce +SHA512 (z3-4.14.0.tar.gz) = 5a3de3207b5c05f77f8369d7fdbb9e13a7db850f8c3edaa8f2adfcf58b186d34409e4a56d44646f853027850941135be5042e67a53ddf3302dc3b645c1ab3db4 diff --git a/z3.spec b/z3.spec index e913d54..d85ee1d 100644 --- a/z3.spec +++ b/z3.spec @@ -14,7 +14,7 @@ %global giturl https://github.com/Z3Prover/z3 Name: z3 -Version: 4.13.4 +Version: 4.14.0 Release: %autorelease Summary: Satisfiability Modulo Theories (SMT) solver @@ -184,7 +184,6 @@ export PYTHON=%{python3} %cmake -G Ninja \ -DCMAKE_INSTALL_INCLUDEDIR=%{_includedir}/z3 \ - -DCMAKE_JAVA_COMPILE_FLAGS="-source;1.8;-target;1.8" \ -DZ3_BUILD_DOCUMENTATION:BOOL=ON \ %ifarch %{java_arches} -DZ3_BUILD_JAVA_BINDINGS:BOOL=ON \ @@ -267,7 +266,7 @@ cd - %files libs %license LICENSE.txt -%{_libdir}/libz3.so.4.13* +%{_libdir}/libz3.so.4.14* %files devel %{_includedir}/z3/ From d134122827d35cc2b3d9e1b4ab13a0bff13b0470 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Tue, 11 Mar 2025 10:14:39 -0600 Subject: [PATCH 06/30] Version 4.14.1 --- sources | 2 +- z3.spec | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/sources b/sources index 3cbf117..1daade0 100644 --- a/sources +++ b/sources @@ -1 +1 @@ -SHA512 (z3-4.14.0.tar.gz) = 5a3de3207b5c05f77f8369d7fdbb9e13a7db850f8c3edaa8f2adfcf58b186d34409e4a56d44646f853027850941135be5042e67a53ddf3302dc3b645c1ab3db4 +SHA512 (z3-4.14.1.tar.gz) = 5850821aa93908c952663bfdcae291a9e8cd00082e0fa6d3ea4ffaebf076116d524660e22934e339da4972f43510adcccba1816be0a3e6bb60ab2c380f5a58ab diff --git a/z3.spec b/z3.spec index d85ee1d..7612459 100644 --- a/z3.spec +++ b/z3.spec @@ -14,7 +14,7 @@ %global giturl https://github.com/Z3Prover/z3 Name: z3 -Version: 4.14.0 +Version: 4.14.1 Release: %autorelease Summary: Satisfiability Modulo Theories (SMT) solver From 9c591d7697a3db234e554d7abcbc1de70862eb8d Mon Sep 17 00:00:00 2001 From: Yaakov Selkowitz Date: Mon, 5 May 2025 08:16:30 -0400 Subject: [PATCH 07/30] Specify Python bindings installation directory This is needed for flatpak builds which install into the /app prefix while python is part of the runtime in /usr (but is configured to find modules in /app as well for flatpaks). --- z3.spec | 1 + 1 file changed, 1 insertion(+) diff --git a/z3.spec b/z3.spec index 7612459..35c1bd7 100644 --- a/z3.spec +++ b/z3.spec @@ -189,6 +189,7 @@ export PYTHON=%{python3} -DZ3_BUILD_JAVA_BINDINGS:BOOL=ON \ %endif -DZ3_BUILD_PYTHON_BINDINGS:BOOL=ON \ + -DCMAKE_INSTALL_PYTHON_PKG_DIR=%{python3_sitelib} \ -DZ3_INCLUDE_GIT_HASH:BOOL=OFF \ -DZ3_INCLUDE_GIT_DESCRIBE:BOOL=OFF \ -DZ3_USE_LIB_GMP:BOOL=ON From 71f8a222c81ec4161a6ebaeb7ccbfc51125aa74f Mon Sep 17 00:00:00 2001 From: Jerry James Date: Wed, 21 May 2025 13:43:17 -0600 Subject: [PATCH 08/30] Version 4.15.0 --- sources | 2 +- z3.spec | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/sources b/sources index 1daade0..2eacbf6 100644 --- a/sources +++ b/sources @@ -1 +1 @@ -SHA512 (z3-4.14.1.tar.gz) = 5850821aa93908c952663bfdcae291a9e8cd00082e0fa6d3ea4ffaebf076116d524660e22934e339da4972f43510adcccba1816be0a3e6bb60ab2c380f5a58ab +SHA512 (z3-4.15.0.tar.gz) = 1e10d5e09611412b52dfd552d6b15eb1a819354ba074aa3427ce7b7431b0e3fff0f8bb7b84028c52ff7a6f01080e3d9cd1cacdc379c0dad1830fb7b36adeb445 diff --git a/z3.spec b/z3.spec index 35c1bd7..bff832a 100644 --- a/z3.spec +++ b/z3.spec @@ -14,7 +14,7 @@ %global giturl https://github.com/Z3Prover/z3 Name: z3 -Version: 4.14.1 +Version: 4.15.0 Release: %autorelease Summary: Satisfiability Modulo Theories (SMT) solver @@ -267,7 +267,7 @@ cd - %files libs %license LICENSE.txt -%{_libdir}/libz3.so.4.14* +%{_libdir}/libz3.so.4.15* %files devel %{_includedir}/z3/ From 5720dba19b4700110598e498ea6b3c9ae020dc32 Mon Sep 17 00:00:00 2001 From: Python Maint Date: Mon, 2 Jun 2025 22:56:18 +0200 Subject: [PATCH 09/30] Rebuilt for Python 3.14 From 0e4394de8214d0487bf7273cbd854183821bda3c Mon Sep 17 00:00:00 2001 From: Jerry James Date: Wed, 11 Jun 2025 06:46:55 -0600 Subject: [PATCH 10/30] Version 4.15.1 --- sources | 2 +- z3.spec | 7 +------ 2 files changed, 2 insertions(+), 7 deletions(-) diff --git a/sources b/sources index 2eacbf6..eb2eb2e 100644 --- a/sources +++ b/sources @@ -1 +1 @@ -SHA512 (z3-4.15.0.tar.gz) = 1e10d5e09611412b52dfd552d6b15eb1a819354ba074aa3427ce7b7431b0e3fff0f8bb7b84028c52ff7a6f01080e3d9cd1cacdc379c0dad1830fb7b36adeb445 +SHA512 (z3-4.15.1.tar.gz) = 50af354056b3e796a39f1e53525c1fb4039f4a76c13fbf2ce5d57dc62a941acb5ecc7436a519898ae0af3cc5660bfb50100e0532b3a3b7d6f932308fb639b642 diff --git a/z3.spec b/z3.spec index bff832a..2e3d566 100644 --- a/z3.spec +++ b/z3.spec @@ -14,7 +14,7 @@ %global giturl https://github.com/Z3Prover/z3 Name: z3 -Version: 4.15.0 +Version: 4.15.1 Release: %autorelease Summary: Satisfiability Modulo Theories (SMT) solver @@ -57,11 +57,6 @@ uninterpreted functions, and quantifiers. %package libs Summary: Library for applications that use z3 functionality -# This can be removed when F40 reaches EOL -%ifnarch %{java_arches} -Obsoletes: java-z3 < 4.8.17-5 -%endif - %description libs Library for applications that use z3 functionality. From 507d8c89936840a12beae7c794278310fe3c2d00 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Wed, 25 Jun 2025 14:15:56 -0600 Subject: [PATCH 11/30] Version 4.15.2 --- sources | 2 +- z3.spec | 6 +++--- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/sources b/sources index eb2eb2e..17253b1 100644 --- a/sources +++ b/sources @@ -1 +1 @@ -SHA512 (z3-4.15.1.tar.gz) = 50af354056b3e796a39f1e53525c1fb4039f4a76c13fbf2ce5d57dc62a941acb5ecc7436a519898ae0af3cc5660bfb50100e0532b3a3b7d6f932308fb639b642 +SHA512 (z3-4.15.2.tar.gz) = ef752530cec0c08dbc53671c9fd04b6ed4d190905598d3d7dc1cb21dfde97fd0d69962c478ccc60e823718e2c57d9b3ee670f48fd09215597fa44d04b60fb21c diff --git a/z3.spec b/z3.spec index 2e3d566..4a7c78c 100644 --- a/z3.spec +++ b/z3.spec @@ -14,7 +14,7 @@ %global giturl https://github.com/Z3Prover/z3 Name: z3 -Version: 4.15.1 +Version: 4.15.2 Release: %autorelease Summary: Satisfiability Modulo Theories (SMT) solver @@ -61,11 +61,11 @@ Summary: Library for applications that use z3 functionality Library for applications that use z3 functionality. %package devel -Summary: Header files for build applications that use z3 +Summary: Header files for building applications that use z3 Requires: z3-libs%{?_isa} = %{version}-%{release} %description devel -Header files for build applications that use z3. +Header files for building applications that use z3. %package doc # The content is MIT. From 043ebfe270048b051ffd167ea005358f1c652d55 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Fri, 11 Jul 2025 16:48:34 -0600 Subject: [PATCH 12/30] Rebuild to fix OCaml dependencies From 22a3a8a3262743dfcf05a9530d9ce8d786b6bfbe Mon Sep 17 00:00:00 2001 From: Fedora Release Engineering Date: Fri, 25 Jul 2025 21:15:02 +0000 Subject: [PATCH 13/30] Rebuilt for https://fedoraproject.org/wiki/Fedora_43_Mass_Rebuild From 466f109dbd9df9ef3a4f7da82cdbb8b7732494d0 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Wed, 6 Aug 2025 19:58:21 -0600 Subject: [PATCH 14/30] Stop building on 32-bit x86 - Provide the PyPI name for the python subpackage --- z3.spec | 17 ++++++----------- 1 file changed, 6 insertions(+), 11 deletions(-) diff --git a/z3.spec b/z3.spec index 4a7c78c..e412c77 100644 --- a/z3.spec +++ b/z3.spec @@ -25,6 +25,9 @@ Source: %{giturl}/archive/%{name}-%{version}.tar.gz # Do not try to build or install native OCaml artifacts on bytecode-only arches Patch: %{name}-ocaml.patch +# See https://fedoraproject.org/wiki/Changes/EncourageI686LeafRemoval +ExcludeArch: %{ix86} + BuildRequires: cmake BuildRequires: doxygen BuildRequires: gcc-c++ @@ -37,12 +40,10 @@ BuildRequires: javapackages-tools %endif BuildRequires: make BuildRequires: ninja-build -%ifnarch %{ix86} BuildRequires: ocaml BuildRequires: ocaml-findlib BuildRequires: ocaml-ocamldoc BuildRequires: ocaml-zarith-devel -%endif BuildRequires: python3-devel BuildRequires: %{py3_dist setuptools} @@ -119,8 +120,6 @@ Requires: javapackages-tools Java interface to z3. %endif -# OCaml packages not built on i686 since OCaml 5 / Fedora 39. -%ifnarch %{ix86} %package -n ocaml-z3 Summary: Ocaml interface to z3 Requires: z3-libs%{?_isa} = %{version}-%{release} @@ -135,13 +134,15 @@ Requires: ocaml-zarith-devel%{?_isa} %description -n ocaml-z3-devel Files for building ocaml applications that use z3. -%endif %package -n python3-z3 Summary: Python 3 interface to z3 BuildArch: noarch Requires: z3-libs = %{version}-%{release} +# Provide the PyPI name +%py_provides python3-z3-solver + %description -n python3-z3 Python 3 interface to z3. @@ -191,7 +192,6 @@ export PYTHON=%{python3} %cmake_build -%ifnarch %{ix86} # The cmake build system does not build the OCaml interface. Do that manually. # # First, run the configure script to generate several files. @@ -208,7 +208,6 @@ sed -i '/^api/s/ libz3\$(SO_EXT)//g' build/Makefile # Fourth, build the OCaml interface %make_build -C build ml -%endif %install # Install the C++, python3, and Java interfaces @@ -223,7 +222,6 @@ ln -s %{_jnidir}/com.microsoft.z3.jar %{buildroot}%{_libdir}/z3 mv %{buildroot}%{_libdir}/libz3java.so %{buildroot}%{_libdir}/z3 %endif -%ifnarch %{ix86} # Install the OCaml interface cd build/api/ml mkdir -p %{buildroot}%{ocamldir}/Z3 @@ -234,7 +232,6 @@ cp -p META *.{a,cma,cmi,mli} %{buildroot}%{ocamldir}/Z3 mkdir -p %{buildroot}%{ocamldir}/stublibs cp -p *.so %{buildroot}%{ocamldir}/stublibs cd - -%endif # We handle the documentation files below rm -rf %{buildroot}%{_docdir}/Z3 @@ -280,7 +277,6 @@ cd - %{_jnidir}/com.microsoft.z3*jar %endif -%ifnarch %{ix86} %files -n ocaml-z3 %dir %{ocamldir}/Z3/ %{ocamldir}/Z3/META @@ -298,7 +294,6 @@ cd - %{ocamldir}/Z3/*.cmxa %endif %{ocamldir}/Z3/*.mli -%endif %files -n python3-z3 %{python3_sitelib}/z3/ From ae57f901436161161e2934b2688530395fe1b728 Mon Sep 17 00:00:00 2001 From: Python Maint Date: Fri, 15 Aug 2025 15:23:57 +0200 Subject: [PATCH 15/30] Rebuilt for Python 3.14.0rc2 bytecode From b4193b0bfb198df22e3a6babf931d239ab09458c Mon Sep 17 00:00:00 2001 From: Jerry James Date: Sat, 16 Aug 2025 15:19:33 -0600 Subject: [PATCH 16/30] Version 4.15.3 --- sources | 2 +- z3.spec | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/sources b/sources index 17253b1..b9b674e 100644 --- a/sources +++ b/sources @@ -1 +1 @@ -SHA512 (z3-4.15.2.tar.gz) = ef752530cec0c08dbc53671c9fd04b6ed4d190905598d3d7dc1cb21dfde97fd0d69962c478ccc60e823718e2c57d9b3ee670f48fd09215597fa44d04b60fb21c +SHA512 (z3-4.15.3.tar.gz) = fde2e334e455401b69ff1d518a8c9e14590b3140e3f6ef907f6d502cebcb0861478229a1a94e5e687d989cdb63f4fd8cde76c6501ea1b5f2b2d34c876aff3486 diff --git a/z3.spec b/z3.spec index e412c77..f47a8e8 100644 --- a/z3.spec +++ b/z3.spec @@ -14,7 +14,7 @@ %global giturl https://github.com/Z3Prover/z3 Name: z3 -Version: 4.15.2 +Version: 4.15.3 Release: %autorelease Summary: Satisfiability Modulo Theories (SMT) solver From 437edefdb975fa34d26fd31506d2122af024c1a5 Mon Sep 17 00:00:00 2001 From: Python Maint Date: Fri, 19 Sep 2025 15:04:28 +0200 Subject: [PATCH 17/30] Rebuilt for Python 3.14.0rc3 bytecode From 73af82e4190f95920866d69f85d98be74903bf21 Mon Sep 17 00:00:00 2001 From: "Richard W.M. Jones" Date: Mon, 13 Oct 2025 21:32:24 +0100 Subject: [PATCH 18/30] OCaml 5.4.0 rebuild From 514a1e5e564c663161645e263d319f6a5252cbc5 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Thu, 30 Oct 2025 09:56:46 -0600 Subject: [PATCH 19/30] Version 4.15.4 --- sources | 2 +- z3.spec | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/sources b/sources index b9b674e..efaf1df 100644 --- a/sources +++ b/sources @@ -1 +1 @@ -SHA512 (z3-4.15.3.tar.gz) = fde2e334e455401b69ff1d518a8c9e14590b3140e3f6ef907f6d502cebcb0861478229a1a94e5e687d989cdb63f4fd8cde76c6501ea1b5f2b2d34c876aff3486 +SHA512 (z3-4.15.4.tar.gz) = 3037a6c9077cf5b5bbc9db89973311e66233144ad6c8fc8da9fb2aa35bb34944068874868cf571b247130251a8361cbd1e24288768cc49e4166985cf0ca921a2 diff --git a/z3.spec b/z3.spec index f47a8e8..361d44a 100644 --- a/z3.spec +++ b/z3.spec @@ -14,7 +14,7 @@ %global giturl https://github.com/Z3Prover/z3 Name: z3 -Version: 4.15.3 +Version: 4.15.4 Release: %autorelease Summary: Satisfiability Modulo Theories (SMT) solver From 0e1cc638741f9180b082b822e37dd1fcf1a7fb99 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Wed, 14 Jan 2026 08:53:40 -0700 Subject: [PATCH 20/30] Reflow the description text - Be more precise about globbing in %files --- z3.spec | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/z3.spec b/z3.spec index 361d44a..a91ada6 100644 --- a/z3.spec +++ b/z3.spec @@ -49,11 +49,11 @@ BuildRequires: %{py3_dist setuptools} %description Z3 is a satisfiability modulo theories (SMT) solver; given a set of -constraints with variables, it reports a set of values for those -variables that would meet the constraints. The Z3 input format is an -extension of the one defined by the SMT-LIB 2.0 standard. Z3 supports -arithmetic, fixed-size bit-vectors, extensional arrays, datatypes, -uninterpreted functions, and quantifiers. +constraints with variables, it reports a set of values for those variables +that would meet the constraints. The Z3 input format is an extension of the +one defined by the SMT-LIB 2.0 standard. Z3 supports arithmetic, fixed-size +bit-vectors, extensional arrays, datatypes, uninterpreted functions, and +quantifiers. %package libs Summary: Library for applications that use z3 functionality @@ -259,7 +259,7 @@ cd - %files libs %license LICENSE.txt -%{_libdir}/libz3.so.4.15* +%{_libdir}/libz3.so.4.15{,.*} %files devel %{_includedir}/z3/ From ed67b528b59af2ea6544cbce69cc8a5193ab607f Mon Sep 17 00:00:00 2001 From: Fedora Release Engineering Date: Sat, 17 Jan 2026 21:04:57 +0000 Subject: [PATCH 21/30] Rebuilt for https://fedoraproject.org/wiki/Fedora_44_Mass_Rebuild From 4857863f075b607a9b5d8f774626643a21998b59 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Mon, 9 Feb 2026 21:17:37 -0700 Subject: [PATCH 22/30] Version 4.15.7 - Make the doc subpackage noarch again --- sources | 2 +- z3-s390x-doc.patch | 505 +++++++++++++++++++++++++++++++++++++++++++++ z3.spec | 53 +++-- 3 files changed, 531 insertions(+), 29 deletions(-) create mode 100644 z3-s390x-doc.patch diff --git a/sources b/sources index efaf1df..4b1ed9a 100644 --- a/sources +++ b/sources @@ -1 +1 @@ -SHA512 (z3-4.15.4.tar.gz) = 3037a6c9077cf5b5bbc9db89973311e66233144ad6c8fc8da9fb2aa35bb34944068874868cf571b247130251a8361cbd1e24288768cc49e4166985cf0ca921a2 +SHA512 (z3-4.15.7.tar.gz) = 7771e762c5413a67434027ef86f06cd7596b1bc187c093ebc63e2abe425374d098d84a169ffdb2ebab6e9af989046dd207e8a21e0e640d7a54003f496d6c30a8 diff --git a/z3-s390x-doc.patch b/z3-s390x-doc.patch new file mode 100644 index 0000000..ec9ae91 --- /dev/null +++ b/z3-s390x-doc.patch @@ -0,0 +1,505 @@ +--- a/doc/api/html/z3.z3core.html ++++ b/doc/api/html/z3.z3core.html +@@ -277,13 +277,21 @@ Data descriptors defined here:
+ a3, + _elems=<z3.z3core.Elementaries object> + ) +-
Z3_ast_map_keys(a0, a1, _elems=<z3.z3core.Elementaries object>)
++
Z3_ast_map_keys( ++ a0, ++ a1, ++ _elems=<z3.z3core.Elementaries object> ++)
+
Z3_ast_map_reset( + a0, + a1, + _elems=<z3.z3core.Elementaries object> + )
+-
Z3_ast_map_size(a0, a1, _elems=<z3.z3core.Elementaries object>)
++
Z3_ast_map_size( ++ a0, ++ a1, ++ _elems=<z3.z3core.Elementaries object> ++)
+
Z3_ast_map_to_string( + a0, + a1, +@@ -833,7 +841,11 @@ Data descriptors defined here:
+ a2, + _elems=<z3.z3core.Elementaries object> + )
+-
Z3_get_app_decl(a0, a1, _elems=<z3.z3core.Elementaries object>)
++
Z3_get_app_decl( ++ a0, ++ a1, ++ _elems=<z3.z3core.Elementaries object> ++)
+
Z3_get_app_num_args( + a0, + a1, +@@ -866,9 +878,17 @@ Data descriptors defined here:
+ a1, + _elems=<z3.z3core.Elementaries object> + )
+-
Z3_get_ast_hash(a0, a1, _elems=<z3.z3core.Elementaries object>)
++
Z3_get_ast_hash( ++ a0, ++ a1, ++ _elems=<z3.z3core.Elementaries object> ++)
+
Z3_get_ast_id(a0, a1, _elems=<z3.z3core.Elementaries object>)
+-
Z3_get_ast_kind(a0, a1, _elems=<z3.z3core.Elementaries object>)
++
Z3_get_ast_kind( ++ a0, ++ a1, ++ _elems=<z3.z3core.Elementaries object> ++)
+
Z3_get_bool_value( + a0, + a1, +@@ -1347,7 +1367,11 @@ Data descriptors defined here:
+ a2, + _elems=<z3.z3core.Elementaries object> + )
+-
Z3_goal_dec_ref(a0, a1, _elems=<z3.z3core.Elementaries object>)
++
Z3_goal_dec_ref( ++ a0, ++ a1, ++ _elems=<z3.z3core.Elementaries object> ++)
+
Z3_goal_depth(a0, a1, _elems=<z3.z3core.Elementaries object>)
+
Z3_goal_formula( + a0, +@@ -1355,7 +1379,11 @@ Data descriptors defined here:
+ a2, + _elems=<z3.z3core.Elementaries object> + )
+-
Z3_goal_inc_ref(a0, a1, _elems=<z3.z3core.Elementaries object>)
++
Z3_goal_inc_ref( ++ a0, ++ a1, ++ _elems=<z3.z3core.Elementaries object> ++)
+
Z3_goal_inconsistent( + a0, + a1, +@@ -1420,7 +1448,11 @@ Data descriptors defined here:
+ )
+
Z3_is_app(a0, a1, _elems=<z3.z3core.Elementaries object>)
+
Z3_is_as_array(a0, a1, _elems=<z3.z3core.Elementaries object>)
+-
Z3_is_char_sort(a0, a1, _elems=<z3.z3core.Elementaries object>)
++
Z3_is_char_sort( ++ a0, ++ a1, ++ _elems=<z3.z3core.Elementaries object> ++)
+
Z3_is_eq_ast( + a0, + a1, +@@ -1532,7 +1564,12 @@ Data descriptors defined here:
+ _elems=<z3.z3core.Elementaries object> + )
+
Z3_mk_bool_sort(a0, _elems=<z3.z3core.Elementaries object>)
+-
Z3_mk_bound(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)
++
Z3_mk_bound( ++ a0, ++ a1, ++ a2, ++ _elems=<z3.z3core.Elementaries object> ++)
+
Z3_mk_bv2int( + a0, + a1, +@@ -1546,7 +1583,12 @@ Data descriptors defined here:
+ _elems=<z3.z3core.Elementaries object> + )
+
Z3_mk_bv_sort(a0, a1, _elems=<z3.z3core.Elementaries object>)
+-
Z3_mk_bvadd(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)
++
Z3_mk_bvadd( ++ a0, ++ a1, ++ a2, ++ _elems=<z3.z3core.Elementaries object> ++)
+
Z3_mk_bvadd_no_overflow( + a0, + a1, +@@ -1560,7 +1602,12 @@ Data descriptors defined here:
+ a2, + _elems=<z3.z3core.Elementaries object> + )
+-
Z3_mk_bvand(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)
++
Z3_mk_bvand( ++ a0, ++ a1, ++ a2, ++ _elems=<z3.z3core.Elementaries object> ++)
+
Z3_mk_bvashr( + a0, + a1, +@@ -1573,7 +1620,12 @@ Data descriptors defined here:
+ a2, + _elems=<z3.z3core.Elementaries object> + )
+-
Z3_mk_bvmul(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)
++
Z3_mk_bvmul( ++ a0, ++ a1, ++ a2, ++ _elems=<z3.z3core.Elementaries object> ++)
+
Z3_mk_bvmul_no_overflow( + a0, + a1, +@@ -1599,7 +1651,12 @@ Data descriptors defined here:
+ a1, + _elems=<z3.z3core.Elementaries object> + )
+-
Z3_mk_bvnor(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)
++
Z3_mk_bvnor( ++ a0, ++ a1, ++ a2, ++ _elems=<z3.z3core.Elementaries object> ++)
+
Z3_mk_bvnot(a0, a1, _elems=<z3.z3core.Elementaries object>)
+
Z3_mk_bvor(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)
+
Z3_mk_bvredand(a0, a1, _elems=<z3.z3core.Elementaries object>)
+@@ -1616,11 +1673,36 @@ Data descriptors defined here:
+ a2, + _elems=<z3.z3core.Elementaries object> + ) +-
Z3_mk_bvsge(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)
+-
Z3_mk_bvsgt(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)
+-
Z3_mk_bvshl(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)
+-
Z3_mk_bvsle(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)
+-
Z3_mk_bvslt(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)
++
Z3_mk_bvsge( ++ a0, ++ a1, ++ a2, ++ _elems=<z3.z3core.Elementaries object> ++)
++
Z3_mk_bvsgt( ++ a0, ++ a1, ++ a2, ++ _elems=<z3.z3core.Elementaries object> ++)
++
Z3_mk_bvshl( ++ a0, ++ a1, ++ a2, ++ _elems=<z3.z3core.Elementaries object> ++)
++
Z3_mk_bvsle( ++ a0, ++ a1, ++ a2, ++ _elems=<z3.z3core.Elementaries object> ++)
++
Z3_mk_bvslt( ++ a0, ++ a1, ++ a2, ++ _elems=<z3.z3core.Elementaries object> ++)
+
Z3_mk_bvsmod( + a0, + a1, +@@ -1633,7 +1715,12 @@ Data descriptors defined here:
+ a2, + _elems=<z3.z3core.Elementaries object> + )
+-
Z3_mk_bvsub(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)
++
Z3_mk_bvsub( ++ a0, ++ a1, ++ a2, ++ _elems=<z3.z3core.Elementaries object> ++)
+
Z3_mk_bvsub_no_overflow( + a0, + a1, +@@ -1653,10 +1740,30 @@ Data descriptors defined here:
+ a2, + _elems=<z3.z3core.Elementaries object> + )
+-
Z3_mk_bvuge(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)
+-
Z3_mk_bvugt(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)
+-
Z3_mk_bvule(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)
+-
Z3_mk_bvult(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)
++
Z3_mk_bvuge( ++ a0, ++ a1, ++ a2, ++ _elems=<z3.z3core.Elementaries object> ++)
++
Z3_mk_bvugt( ++ a0, ++ a1, ++ a2, ++ _elems=<z3.z3core.Elementaries object> ++)
++
Z3_mk_bvule( ++ a0, ++ a1, ++ a2, ++ _elems=<z3.z3core.Elementaries object> ++)
++
Z3_mk_bvult( ++ a0, ++ a1, ++ a2, ++ _elems=<z3.z3core.Elementaries object> ++)
+
Z3_mk_bvurem( + a0, + a1, +@@ -1669,7 +1776,12 @@ Data descriptors defined here:
+ a2, + _elems=<z3.z3core.Elementaries object> + )
+-
Z3_mk_bvxor(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)
++
Z3_mk_bvxor( ++ a0, ++ a1, ++ a2, ++ _elems=<z3.z3core.Elementaries object> ++)
+
Z3_mk_char(a0, a1, _elems=<z3.z3core.Elementaries object>)
+
Z3_mk_char_from_bv( + a0, +@@ -1705,7 +1817,12 @@ Data descriptors defined here:
+ _elems=<z3.z3core.Elementaries object> + )
+
Z3_mk_config(_elems=<z3.z3core.Elementaries object>)
+-
Z3_mk_const(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)
++
Z3_mk_const( ++ a0, ++ a1, ++ a2, ++ _elems=<z3.z3core.Elementaries object> ++)
+
Z3_mk_const_array( + a0, + a1, +@@ -1765,7 +1882,11 @@ Data descriptors defined here:
+ a2, + _elems=<z3.z3core.Elementaries object> + )
+-
Z3_mk_empty_set(a0, a1, _elems=<z3.z3core.Elementaries object>)
++
Z3_mk_empty_set( ++ a0, ++ a1, ++ _elems=<z3.z3core.Elementaries object> ++)
+
Z3_mk_enumeration_sort( + a0, + a1, +@@ -2056,7 +2177,10 @@ Data descriptors defined here:
+ a0, + _elems=<z3.z3core.Elementaries object> + )
+-
Z3_mk_fpa_sort_half(a0, _elems=<z3.z3core.Elementaries object>)
++
Z3_mk_fpa_sort_half( ++ a0, ++ _elems=<z3.z3core.Elementaries object> ++)
+
Z3_mk_fpa_sort_quadruple( + a0, + _elems=<z3.z3core.Elementaries object> +@@ -2197,7 +2321,12 @@ Data descriptors defined here:
+ _elems=<z3.z3core.Elementaries object> + )
+
Z3_mk_int2real(a0, a1, _elems=<z3.z3core.Elementaries object>)
+-
Z3_mk_int64(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)
++
Z3_mk_int64( ++ a0, ++ a1, ++ a2, ++ _elems=<z3.z3core.Elementaries object> ++)
+
Z3_mk_int_sort(a0, _elems=<z3.z3core.Elementaries object>)
+
Z3_mk_int_symbol( + a0, +@@ -2333,7 +2462,12 @@ Data descriptors defined here:
+ a5, + _elems=<z3.z3core.Elementaries object> + )
+-
Z3_mk_power(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)
++
Z3_mk_power( ++ a0, ++ a1, ++ a2, ++ _elems=<z3.z3core.Elementaries object> ++)
+
Z3_mk_probe(a0, a1, _elems=<z3.z3core.Elementaries object>)
+
Z3_mk_quantifier( + a0, +@@ -2426,7 +2560,11 @@ Data descriptors defined here:
+ a3, + _elems=<z3.z3core.Elementaries object> + )
+-
Z3_mk_re_option(a0, a1, _elems=<z3.z3core.Elementaries object>)
++
Z3_mk_re_option( ++ a0, ++ a1, ++ _elems=<z3.z3core.Elementaries object> ++)
+
Z3_mk_re_plus(a0, a1, _elems=<z3.z3core.Elementaries object>)
+
Z3_mk_re_power( + a0, +@@ -2520,7 +2658,11 @@ Data descriptors defined here:
+ a2, + _elems=<z3.z3core.Elementaries object> + )
+-
Z3_mk_seq_empty(a0, a1, _elems=<z3.z3core.Elementaries object>)
++
Z3_mk_seq_empty( ++ a0, ++ a1, ++ _elems=<z3.z3core.Elementaries object> ++)
+
Z3_mk_seq_extract( + a0, + a1, +@@ -2627,7 +2769,11 @@ Data descriptors defined here:
+ a2, + _elems=<z3.z3core.Elementaries object> + )
+-
Z3_mk_seq_to_re(a0, a1, _elems=<z3.z3core.Elementaries object>)
++
Z3_mk_seq_to_re( ++ a0, ++ a1, ++ _elems=<z3.z3core.Elementaries object> ++)
+
Z3_mk_seq_unit(a0, a1, _elems=<z3.z3core.Elementaries object>)
+
Z3_mk_set_add( + a0, +@@ -2683,7 +2829,10 @@ Data descriptors defined here:
+ a2, + _elems=<z3.z3core.Elementaries object> + )
+-
Z3_mk_simple_solver(a0, _elems=<z3.z3core.Elementaries object>)
++
Z3_mk_simple_solver( ++ a0, ++ _elems=<z3.z3core.Elementaries object> ++)
+
Z3_mk_simplifier( + a0, + a1, +@@ -3052,7 +3201,11 @@ Data descriptors defined here:
+ a2, + _elems=<z3.z3core.Elementaries object> + )
+-
Z3_optimize_pop(a0, a1, _elems=<z3.z3core.Elementaries object>)
++
Z3_optimize_pop( ++ a0, ++ a1, ++ _elems=<z3.z3core.Elementaries object> ++)
+
Z3_optimize_push( + a0, + a1, +@@ -3288,8 +3441,18 @@ Data descriptors defined here:
+ a1, + _elems=<z3.z3core.Elementaries object> + )
+-
Z3_probe_eq(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)
+-
Z3_probe_ge(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)
++
Z3_probe_eq( ++ a0, ++ a1, ++ a2, ++ _elems=<z3.z3core.Elementaries object> ++)
++
Z3_probe_ge( ++ a0, ++ a1, ++ a2, ++ _elems=<z3.z3core.Elementaries object> ++)
+
Z3_probe_get_descr( + a0, + a1, +@@ -3300,16 +3463,36 @@ Data descriptors defined here:
+ a1, + _elems=<z3.z3core.Elementaries object> + )
+-
Z3_probe_gt(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)
++
Z3_probe_gt( ++ a0, ++ a1, ++ a2, ++ _elems=<z3.z3core.Elementaries object> ++)
+
Z3_probe_inc_ref( + a0, + a1, + _elems=<z3.z3core.Elementaries object> + )
+-
Z3_probe_le(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)
+-
Z3_probe_lt(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)
++
Z3_probe_le( ++ a0, ++ a1, ++ a2, ++ _elems=<z3.z3core.Elementaries object> ++)
++
Z3_probe_lt( ++ a0, ++ a1, ++ a2, ++ _elems=<z3.z3core.Elementaries object> ++)
+
Z3_probe_not(a0, a1, _elems=<z3.z3core.Elementaries object>)
+-
Z3_probe_or(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)
++
Z3_probe_or( ++ a0, ++ a1, ++ a2, ++ _elems=<z3.z3core.Elementaries object> ++)
+
Z3_qe_lite(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)
+
Z3_qe_model_project( + a0, +@@ -3605,7 +3788,11 @@ Data descriptors defined here:
+ a3, + _elems=<z3.z3core.Elementaries object> + )
+-
Z3_solver_check(a0, a1, _elems=<z3.z3core.Elementaries object>)
++
Z3_solver_check( ++ a0, ++ a1, ++ _elems=<z3.z3core.Elementaries object> ++)
+
Z3_solver_check_assumptions( + a0, + a1, +@@ -3862,7 +4049,11 @@ Data descriptors defined here:
+ a3, + _elems=<z3.z3core.Elementaries object> + )
+-
Z3_solver_reset(a0, a1, _elems=<z3.z3core.Elementaries object>)
++
Z3_solver_reset( ++ a0, ++ a1, ++ _elems=<z3.z3core.Elementaries object> ++)
+
Z3_solver_set_initial_value( + a0, + a1, +@@ -4118,7 +4309,11 @@ Data descriptors defined here:
+ _elems=<z3.z3core.Elementaries object> + )
+
Z3_to_app(a0, a1, _elems=<z3.z3core.Elementaries object>)
+-
Z3_to_func_decl(a0, a1, _elems=<z3.z3core.Elementaries object>)
++
Z3_to_func_decl( ++ a0, ++ a1, ++ _elems=<z3.z3core.Elementaries object> ++)
+
Z3_toggle_warning_messages( + a0, + _elems=<z3.z3core.Elementaries object> diff --git a/z3.spec b/z3.spec index a91ada6..eeb0277 100644 --- a/z3.spec +++ b/z3.spec @@ -11,19 +11,22 @@ # the koji builders have available. %bcond test 0 -%global giturl https://github.com/Z3Prover/z3 - Name: z3 -Version: 4.15.4 +Version: 4.15.7 Release: %autorelease Summary: Satisfiability Modulo Theories (SMT) solver +%global giturl https://github.com/Z3Prover/z3 +%global majver %{gsub %version ^(%d*%.%d*)%..*$ %1} + License: MIT URL: https://github.com/Z3Prover/z3/wiki VCS : git:%{giturl}.git Source: %{giturl}/archive/%{name}-%{version}.tar.gz # Do not try to build or install native OCaml artifacts on bytecode-only arches Patch: %{name}-ocaml.patch +# Fix up the s390x docs so they look like other arches +Patch: %{name}-s390x-doc.patch # See https://fedoraproject.org/wiki/Changes/EncourageI686LeafRemoval ExcludeArch: %{ix86} @@ -74,37 +77,19 @@ Header files for building applications that use z3. # examples/tptp/tptp5.tab.c # examples/tptp/tptp5.tab.c # Other licenses are due to files installed by doxygen. -# html/bc_s.png: GPL-1.0-or-later -# html/bdwn.png: GPL-1.0-or-later -# html/closed.png: GPL-1.0-or-later -# html/doc.png: GPL-1.0-or-later +# html/clipboard.js: MIT +# html/cookie.js: MIT # html/doxygen.css: GPL-1.0-or-later # html/doxygen.svg: GPL-1.0-or-later # html/dynsections.js: MIT -# html/folderclosed.png: GPL-1.0-or-later -# html/folderopen.png: GPL-1.0-or-later # html/jquery.js: MIT -# html/nav_f.png: GPL-1.0-or-later -# html/nav_g.png: GPL-1.0-or-later -# html/nav_h.png: GPL-1.0-or-later -# html/open.png: GPL-1.0-or-later +# html/navtree.css: GPL-1.0-or-later # html/search/search.css: GPL-1.0-or-later # html/search/search.js: MIT -# html/search/search_l.png: GPL-1.0-or-later -# html/search/search_m.png: GPL-1.0-or-later -# html/search/search_r.png: GPL-1.0-or-later -# html/splitbar.png: GPL-1.0-or-later -# html/sync_off.png: GPL-1.0-or-later -# html/sync_on.png: GPL-1.0-or-later -# html/tab_a.png: GPL-1.0-or-later -# html/tab_b.png: GPL-1.0-or-later -# html/tab_h.png: GPL-1.0-or-later -# html/tab_s.png: GPL-1.0-or-later # html/tabs.css: GPL-1.0-or-later License: MIT AND GPL-3.0-or-later WITH Bison-exception-2.2 AND GPL-1.0-or-later Summary: API documentation for Z3 -# FIXME: this should be noarch, but we end up with different numbers of inheritance -# graphs on different architectures. Why? +BuildArch: noarch %description doc API documentation for Z3. @@ -149,7 +134,7 @@ Python 3 interface to z3. %prep %autosetup -N -n %{name}-%{name}-%{version} %ifnarch %{ocaml_native_compiler} -%patch -P0 -p1 +%patch 0 -p1 %endif %conf @@ -167,9 +152,8 @@ sed \ -i scripts/mk_util.py # Comply with the Java packaging guidelines and fill in the version for python -majver=$(cut -d. -f-2 <<< %{version}) sed -e '/libz3java/s,\(System\.load\)Library("\(.*\)"),\1("%{_libdir}/z3/\2.so"),' \ - -e "s/'so'/'so.$majver'/" \ + -e "s/'so'/'so.%{majver}'/" \ -i scripts/update_api.py # Turn off HTML timestamps for reproducible builds @@ -192,6 +176,19 @@ export PYTHON=%{python3} %cmake_build +# Remove meaningless memory addresses from the pydoc documentation +# See https://github.com/python/cpython/issues/83572 +sed -ri 's/, handle [0-9a-fA-F]+//' \ + %{_vpath_builddir}/doc/api/html/z3{,.z3{,num,poly,printer,rcf,util}}.html +sed -ri 's/ at 0x[0-9a-fA-F]+//g' \ + %{_vpath_builddir}/doc/api/html/z3.z3core.html +# For unknown reasons, the s390x documentation build has fewer newlines than +# the builds on other architectures. Make the outputs match so the doc +# package can be noarch. +%ifarch s390x +patch -p1 -T -d %{_vpath_builddir} < %{PATCH1} +%endif + # The cmake build system does not build the OCaml interface. Do that manually. # # First, run the configure script to generate several files. From d923002a80a53ed1077159a28ac659d674c2b06a Mon Sep 17 00:00:00 2001 From: Jerry James Date: Thu, 12 Feb 2026 17:59:26 -0700 Subject: [PATCH 23/30] Version 4.15.8 --- sources | 2 +- z3.spec | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/sources b/sources index 4b1ed9a..347a2f1 100644 --- a/sources +++ b/sources @@ -1 +1 @@ -SHA512 (z3-4.15.7.tar.gz) = 7771e762c5413a67434027ef86f06cd7596b1bc187c093ebc63e2abe425374d098d84a169ffdb2ebab6e9af989046dd207e8a21e0e640d7a54003f496d6c30a8 +SHA512 (z3-4.15.8.tar.gz) = e31df90b0edb3fd4a49a1069d78135d03c6b196c2bc8359a67273e02eba7214a7ff8654488f076ce7a0cf6edffdff9afc403799db3a6e5a1585a6d4c99c4df2a diff --git a/z3.spec b/z3.spec index eeb0277..f0f58fe 100644 --- a/z3.spec +++ b/z3.spec @@ -12,7 +12,7 @@ %bcond test 0 Name: z3 -Version: 4.15.7 +Version: 4.15.8 Release: %autorelease Summary: Satisfiability Modulo Theories (SMT) solver From 190ba8bd4a6bb56fae4770260073990e23e79f75 Mon Sep 17 00:00:00 2001 From: "Richard W.M. Jones" Date: Fri, 20 Feb 2026 17:46:07 +0000 Subject: [PATCH 24/30] OCaml 5.4.1 rebuild From d409226999d316cec1727848e401c08ea82e14c7 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Tue, 3 Mar 2026 06:49:05 -0700 Subject: [PATCH 25/30] Version 4.16.0 --- sources | 2 +- z3.spec | 7 +++++-- 2 files changed, 6 insertions(+), 3 deletions(-) diff --git a/sources b/sources index 347a2f1..fcc522d 100644 --- a/sources +++ b/sources @@ -1 +1 @@ -SHA512 (z3-4.15.8.tar.gz) = e31df90b0edb3fd4a49a1069d78135d03c6b196c2bc8359a67273e02eba7214a7ff8654488f076ce7a0cf6edffdff9afc403799db3a6e5a1585a6d4c99c4df2a +SHA512 (z3-4.16.0.tar.gz) = 7dbcdd04a72f46bc3b6cbac2453b2a43f5ae126287b878ffe37f0573f910a1130c474c5edfa622dab09957f106cf425ab0f7cdfd34d41658599ad50a81ae39dd diff --git a/z3.spec b/z3.spec index f0f58fe..f014748 100644 --- a/z3.spec +++ b/z3.spec @@ -7,12 +7,15 @@ # unless somebody is really, really persuasive and available to help fix it # if it breaks. +# A Go interface is now available, but Fedora no longer builds Go library +# packages (https://docs.fedoraproject.org/en-US/packaging-guidelines/Golang/). + # Tests are off by default because some of the tests require more memory than # the koji builders have available. %bcond test 0 Name: z3 -Version: 4.15.8 +Version: 4.16.0 Release: %autorelease Summary: Satisfiability Modulo Theories (SMT) solver @@ -256,7 +259,7 @@ cd - %files libs %license LICENSE.txt -%{_libdir}/libz3.so.4.15{,.*} +%{_libdir}/libz3.so.4.16{,.*} %files devel %{_includedir}/z3/ From 7279f1bd1f6174e141f90d5de0c8b439868605d7 Mon Sep 17 00:00:00 2001 From: Python Maint Date: Wed, 3 Jun 2026 21:19:42 +0200 Subject: [PATCH 26/30] Rebuilt for Python 3.15 From 81f8e8f923c5906a5dc61fbd7c0483848d9735e0 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Thu, 9 Jul 2026 12:05:02 -0600 Subject: [PATCH 27/30] OCaml 5.5.0 rebuild - Use the cmake declarative buildsystem --- z3.spec | 39 ++++++++++++++++----------------------- 1 file changed, 16 insertions(+), 23 deletions(-) diff --git a/z3.spec b/z3.spec index f014748..da82c1f 100644 --- a/z3.spec +++ b/z3.spec @@ -33,8 +33,19 @@ Patch: %{name}-s390x-doc.patch # See https://fedoraproject.org/wiki/Changes/EncourageI686LeafRemoval ExcludeArch: %{ix86} +BuildSystem: cmake +BuildOption(conf): -G Ninja +BuildOption(conf): -DCMAKE_INSTALL_INCLUDEDIR=%{_includedir}/z3 +BuildOption(conf): -DZ3_BUILD_DOCUMENTATION:BOOL=ON +%ifarch %{java_arches} +BuildOption(conf): -DZ3_BUILD_JAVA_BINDINGS:BOOL=ON +%endif +BuildOption(conf): -DZ3_BUILD_PYTHON_BINDINGS:BOOL=ON +BuildOption(conf): -DCMAKE_INSTALL_PYTHON_PKG_DIR=%{python3_sitelib} +BuildOption(conf): -DZ3_INCLUDE_GIT_HASH:BOOL=OFF +BuildOption(conf): -DZ3_INCLUDE_GIT_DESCRIBE:BOOL=OFF +BuildOption(conf): -DZ3_USE_LIB_GMP:BOOL=ON -BuildRequires: cmake BuildRequires: doxygen BuildRequires: gcc-c++ BuildRequires: gmp-devel @@ -48,7 +59,6 @@ BuildRequires: make BuildRequires: ninja-build BuildRequires: ocaml BuildRequires: ocaml-findlib -BuildRequires: ocaml-ocamldoc BuildRequires: ocaml-zarith-devel BuildRequires: python3-devel BuildRequires: %{py3_dist setuptools} @@ -140,7 +150,6 @@ Python 3 interface to z3. %patch 0 -p1 %endif -%conf # Enable verbose builds, use Fedora CFLAGS, preserve timestamps when installing, # include the entire contents of the archives in the library, link the library # with the correct flags, and build the ocaml files with debuginfo. @@ -162,23 +171,10 @@ sed -e '/libz3java/s,\(System\.load\)Library("\(.*\)"),\1("%{_libdir}/z3/\2.so") # Turn off HTML timestamps for reproducible builds sed -i '/HTML_TIMESTAMP/s/YES/NO/' doc/z3api.cfg.in doc/z3code.dox -%build +%build -p export PYTHON=%{python3} -%cmake -G Ninja \ - -DCMAKE_INSTALL_INCLUDEDIR=%{_includedir}/z3 \ - -DZ3_BUILD_DOCUMENTATION:BOOL=ON \ -%ifarch %{java_arches} - -DZ3_BUILD_JAVA_BINDINGS:BOOL=ON \ -%endif - -DZ3_BUILD_PYTHON_BINDINGS:BOOL=ON \ - -DCMAKE_INSTALL_PYTHON_PKG_DIR=%{python3_sitelib} \ - -DZ3_INCLUDE_GIT_HASH:BOOL=OFF \ - -DZ3_INCLUDE_GIT_DESCRIBE:BOOL=OFF \ - -DZ3_USE_LIB_GMP:BOOL=ON - -%cmake_build - +%build -a # Remove meaningless memory addresses from the pydoc documentation # See https://github.com/python/cpython/issues/83572 sed -ri 's/, handle [0-9a-fA-F]+//' \ @@ -209,10 +205,7 @@ sed -i '/^api/s/ libz3\$(SO_EXT)//g' build/Makefile # Fourth, build the OCaml interface %make_build -C build ml -%install -# Install the C++, python3, and Java interfaces -%cmake_install - +%install -a %ifarch %{java_arches} # Move the Java interface to its correct location mkdir -p %{buildroot}%{_libdir}/z3 @@ -244,8 +237,8 @@ help2man -N -o %{buildroot}%{_mandir}/man1/z3.1 \ # Fix the pkgconfig file sed -i 's,//usr,,' %{buildroot}%{_libdir}/pkgconfig/z3.pc -%if %{with test} %check +%if %{with test} cd build make test-z3 ./test-z3 /a From 5bbbab554130dad41e634045c25fe7d807397647 Mon Sep 17 00:00:00 2001 From: Fedora Release Engineering Date: Fri, 17 Jul 2026 09:37:28 +0000 Subject: [PATCH 28/30] Rebuilt for https://fedoraproject.org/wiki/Fedora_45_Mass_Rebuild From f5dee7eebd2f1a2a1f908830febbe3561f184e8b Mon Sep 17 00:00:00 2001 From: Jerry James Date: Fri, 24 Jul 2026 13:50:31 -0600 Subject: [PATCH 29/30] Version 5.0.0 - Drop s390x doc workaround --- sources | 2 +- z3.spec | 18 +++++------------- 2 files changed, 6 insertions(+), 14 deletions(-) diff --git a/sources b/sources index fcc522d..48cb632 100644 --- a/sources +++ b/sources @@ -1 +1 @@ -SHA512 (z3-4.16.0.tar.gz) = 7dbcdd04a72f46bc3b6cbac2453b2a43f5ae126287b878ffe37f0573f910a1130c474c5edfa622dab09957f106cf425ab0f7cdfd34d41658599ad50a81ae39dd +SHA512 (z3-5.0.0.tar.gz) = c6bed41313a643f2bcad6d6cfda241af948d81326bb41a5a18575170f51c1f4f75afc9e01022df9a6122e71fc54ef813ad2ac9745e40da68c892be68b4777baf diff --git a/z3.spec b/z3.spec index da82c1f..10b7f4b 100644 --- a/z3.spec +++ b/z3.spec @@ -15,7 +15,7 @@ %bcond test 0 Name: z3 -Version: 4.16.0 +Version: 5.0.0 Release: %autorelease Summary: Satisfiability Modulo Theories (SMT) solver @@ -28,8 +28,6 @@ VCS : git:%{giturl}.git Source: %{giturl}/archive/%{name}-%{version}.tar.gz # Do not try to build or install native OCaml artifacts on bytecode-only arches Patch: %{name}-ocaml.patch -# Fix up the s390x docs so they look like other arches -Patch: %{name}-s390x-doc.patch # See https://fedoraproject.org/wiki/Changes/EncourageI686LeafRemoval ExcludeArch: %{ix86} @@ -159,7 +157,7 @@ sed \ -e "s/\(['\"]\)cp\([^[:alnum:]]\)/\1cp -p\2/" \ -e "s/\(SLIBEXTRAFLAGS = '\)'/\1-Wl,--no-whole-archive'/" \ -e '/SLIBFLAGS/s|-shared|& %{build_ldflags} -Wl,--whole-archive|' \ - -e 's/\(libz3$(SO_EXT)\)\(\\n\)/\1 -Wl,--no-whole-archive\2/' \ + -e 's/\(libz3$(SO_EXT)\)\( \$(SLINK\)/\1 -Wl,--no-whole-archive\2/' \ -e "s/OCAML_FLAGS = ''/OCAML_FLAGS = '-g'/" \ -i scripts/mk_util.py @@ -181,12 +179,6 @@ sed -ri 's/, handle [0-9a-fA-F]+//' \ %{_vpath_builddir}/doc/api/html/z3{,.z3{,num,poly,printer,rcf,util}}.html sed -ri 's/ at 0x[0-9a-fA-F]+//g' \ %{_vpath_builddir}/doc/api/html/z3.z3core.html -# For unknown reasons, the s390x documentation build has fewer newlines than -# the builds on other architectures. Make the outputs match so the doc -# package can be noarch. -%ifarch s390x -patch -p1 -T -d %{_vpath_builddir} < %{PATCH1} -%endif # The cmake build system does not build the OCaml interface. Do that manually. # @@ -252,7 +244,7 @@ cd - %files libs %license LICENSE.txt -%{_libdir}/libz3.so.4.16{,.*} +%{_libdir}/libz3.so.5.0{,.*} %files devel %{_includedir}/z3/ @@ -267,7 +259,7 @@ cd - %ifarch %{java_arches} %files -n java-z3 %{_libdir}/z3/ -%{_jnidir}/com.microsoft.z3*jar +%{_jnidir}/com.microsoft.z3.jar %endif %files -n ocaml-z3 @@ -278,7 +270,7 @@ cd - %ifarch %{ocaml_native_compiler} %{ocamldir}/Z3/*.cmxs %endif -%{ocamldir}/stublibs/*.so +%{ocamldir}/stublibs/dllz3ml.so %files -n ocaml-z3-devel %{ocamldir}/Z3/*.a From 9e823927c1eac0504dc9b9c2b48b80112e499794 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Sat, 22 Aug 2026 08:06:31 -0600 Subject: [PATCH 30/30] Version 5.1.0 --- sources | 2 +- z3-s390x-doc.patch | 505 --------------------------------------------- z3.spec | 4 +- 3 files changed, 3 insertions(+), 508 deletions(-) delete mode 100644 z3-s390x-doc.patch diff --git a/sources b/sources index 48cb632..949de7f 100644 --- a/sources +++ b/sources @@ -1 +1 @@ -SHA512 (z3-5.0.0.tar.gz) = c6bed41313a643f2bcad6d6cfda241af948d81326bb41a5a18575170f51c1f4f75afc9e01022df9a6122e71fc54ef813ad2ac9745e40da68c892be68b4777baf +SHA512 (z3-5.1.0.tar.gz) = 03a854f720a56484ab99b8a5517150f1c9106400f54ad758cfa58e3ee2f95e349396a64d4f527a5bb9ee37f10ad9ecfa1916d1f5c921f04089deda409374491b diff --git a/z3-s390x-doc.patch b/z3-s390x-doc.patch deleted file mode 100644 index ec9ae91..0000000 --- a/z3-s390x-doc.patch +++ /dev/null @@ -1,505 +0,0 @@ ---- a/doc/api/html/z3.z3core.html -+++ b/doc/api/html/z3.z3core.html -@@ -277,13 +277,21 @@ Data descriptors defined here:
- a3, - _elems=<z3.z3core.Elementaries object> - )
--
Z3_ast_map_keys(a0, a1, _elems=<z3.z3core.Elementaries object>)
-+
Z3_ast_map_keys( -+ a0, -+ a1, -+ _elems=<z3.z3core.Elementaries object> -+)
-
Z3_ast_map_reset( - a0, - a1, - _elems=<z3.z3core.Elementaries object> - )
--
Z3_ast_map_size(a0, a1, _elems=<z3.z3core.Elementaries object>)
-+
Z3_ast_map_size( -+ a0, -+ a1, -+ _elems=<z3.z3core.Elementaries object> -+)
-
Z3_ast_map_to_string( - a0, - a1, -@@ -833,7 +841,11 @@ Data descriptors defined here:
- a2, - _elems=<z3.z3core.Elementaries object> - )
--
Z3_get_app_decl(a0, a1, _elems=<z3.z3core.Elementaries object>)
-+
Z3_get_app_decl( -+ a0, -+ a1, -+ _elems=<z3.z3core.Elementaries object> -+)
-
Z3_get_app_num_args( - a0, - a1, -@@ -866,9 +878,17 @@ Data descriptors defined here:
- a1, - _elems=<z3.z3core.Elementaries object> - )
--
Z3_get_ast_hash(a0, a1, _elems=<z3.z3core.Elementaries object>)
-+
Z3_get_ast_hash( -+ a0, -+ a1, -+ _elems=<z3.z3core.Elementaries object> -+)
-
Z3_get_ast_id(a0, a1, _elems=<z3.z3core.Elementaries object>)
--
Z3_get_ast_kind(a0, a1, _elems=<z3.z3core.Elementaries object>)
-+
Z3_get_ast_kind( -+ a0, -+ a1, -+ _elems=<z3.z3core.Elementaries object> -+)
-
Z3_get_bool_value( - a0, - a1, -@@ -1347,7 +1367,11 @@ Data descriptors defined here:
- a2, - _elems=<z3.z3core.Elementaries object> - )
--
Z3_goal_dec_ref(a0, a1, _elems=<z3.z3core.Elementaries object>)
-+
Z3_goal_dec_ref( -+ a0, -+ a1, -+ _elems=<z3.z3core.Elementaries object> -+)
-
Z3_goal_depth(a0, a1, _elems=<z3.z3core.Elementaries object>)
-
Z3_goal_formula( - a0, -@@ -1355,7 +1379,11 @@ Data descriptors defined here:
- a2, - _elems=<z3.z3core.Elementaries object> - )
--
Z3_goal_inc_ref(a0, a1, _elems=<z3.z3core.Elementaries object>)
-+
Z3_goal_inc_ref( -+ a0, -+ a1, -+ _elems=<z3.z3core.Elementaries object> -+)
-
Z3_goal_inconsistent( - a0, - a1, -@@ -1420,7 +1448,11 @@ Data descriptors defined here:
- )
-
Z3_is_app(a0, a1, _elems=<z3.z3core.Elementaries object>)
-
Z3_is_as_array(a0, a1, _elems=<z3.z3core.Elementaries object>)
--
Z3_is_char_sort(a0, a1, _elems=<z3.z3core.Elementaries object>)
-+
Z3_is_char_sort( -+ a0, -+ a1, -+ _elems=<z3.z3core.Elementaries object> -+)
-
Z3_is_eq_ast( - a0, - a1, -@@ -1532,7 +1564,12 @@ Data descriptors defined here:
- _elems=<z3.z3core.Elementaries object> - )
-
Z3_mk_bool_sort(a0, _elems=<z3.z3core.Elementaries object>)
--
Z3_mk_bound(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)
-+
Z3_mk_bound( -+ a0, -+ a1, -+ a2, -+ _elems=<z3.z3core.Elementaries object> -+)
-
Z3_mk_bv2int( - a0, - a1, -@@ -1546,7 +1583,12 @@ Data descriptors defined here:
- _elems=<z3.z3core.Elementaries object> - )
-
Z3_mk_bv_sort(a0, a1, _elems=<z3.z3core.Elementaries object>)
--
Z3_mk_bvadd(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)
-+
Z3_mk_bvadd( -+ a0, -+ a1, -+ a2, -+ _elems=<z3.z3core.Elementaries object> -+)
-
Z3_mk_bvadd_no_overflow( - a0, - a1, -@@ -1560,7 +1602,12 @@ Data descriptors defined here:
- a2, - _elems=<z3.z3core.Elementaries object> - )
--
Z3_mk_bvand(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)
-+
Z3_mk_bvand( -+ a0, -+ a1, -+ a2, -+ _elems=<z3.z3core.Elementaries object> -+)
-
Z3_mk_bvashr( - a0, - a1, -@@ -1573,7 +1620,12 @@ Data descriptors defined here:
- a2, - _elems=<z3.z3core.Elementaries object> - )
--
Z3_mk_bvmul(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)
-+
Z3_mk_bvmul( -+ a0, -+ a1, -+ a2, -+ _elems=<z3.z3core.Elementaries object> -+)
-
Z3_mk_bvmul_no_overflow( - a0, - a1, -@@ -1599,7 +1651,12 @@ Data descriptors defined here:
- a1, - _elems=<z3.z3core.Elementaries object> - )
--
Z3_mk_bvnor(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)
-+
Z3_mk_bvnor( -+ a0, -+ a1, -+ a2, -+ _elems=<z3.z3core.Elementaries object> -+)
-
Z3_mk_bvnot(a0, a1, _elems=<z3.z3core.Elementaries object>)
-
Z3_mk_bvor(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)
-
Z3_mk_bvredand(a0, a1, _elems=<z3.z3core.Elementaries object>)
-@@ -1616,11 +1673,36 @@ Data descriptors defined here:
- a2, - _elems=<z3.z3core.Elementaries object> - ) --
Z3_mk_bvsge(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)
--
Z3_mk_bvsgt(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)
--
Z3_mk_bvshl(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)
--
Z3_mk_bvsle(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)
--
Z3_mk_bvslt(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)
-+
Z3_mk_bvsge( -+ a0, -+ a1, -+ a2, -+ _elems=<z3.z3core.Elementaries object> -+)
-+
Z3_mk_bvsgt( -+ a0, -+ a1, -+ a2, -+ _elems=<z3.z3core.Elementaries object> -+)
-+
Z3_mk_bvshl( -+ a0, -+ a1, -+ a2, -+ _elems=<z3.z3core.Elementaries object> -+)
-+
Z3_mk_bvsle( -+ a0, -+ a1, -+ a2, -+ _elems=<z3.z3core.Elementaries object> -+)
-+
Z3_mk_bvslt( -+ a0, -+ a1, -+ a2, -+ _elems=<z3.z3core.Elementaries object> -+)
-
Z3_mk_bvsmod( - a0, - a1, -@@ -1633,7 +1715,12 @@ Data descriptors defined here:
- a2, - _elems=<z3.z3core.Elementaries object> - )
--
Z3_mk_bvsub(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)
-+
Z3_mk_bvsub( -+ a0, -+ a1, -+ a2, -+ _elems=<z3.z3core.Elementaries object> -+)
-
Z3_mk_bvsub_no_overflow( - a0, - a1, -@@ -1653,10 +1740,30 @@ Data descriptors defined here:
- a2, - _elems=<z3.z3core.Elementaries object> - )
--
Z3_mk_bvuge(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)
--
Z3_mk_bvugt(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)
--
Z3_mk_bvule(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)
--
Z3_mk_bvult(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)
-+
Z3_mk_bvuge( -+ a0, -+ a1, -+ a2, -+ _elems=<z3.z3core.Elementaries object> -+)
-+
Z3_mk_bvugt( -+ a0, -+ a1, -+ a2, -+ _elems=<z3.z3core.Elementaries object> -+)
-+
Z3_mk_bvule( -+ a0, -+ a1, -+ a2, -+ _elems=<z3.z3core.Elementaries object> -+)
-+
Z3_mk_bvult( -+ a0, -+ a1, -+ a2, -+ _elems=<z3.z3core.Elementaries object> -+)
-
Z3_mk_bvurem( - a0, - a1, -@@ -1669,7 +1776,12 @@ Data descriptors defined here:
- a2, - _elems=<z3.z3core.Elementaries object> - )
--
Z3_mk_bvxor(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)
-+
Z3_mk_bvxor( -+ a0, -+ a1, -+ a2, -+ _elems=<z3.z3core.Elementaries object> -+)
-
Z3_mk_char(a0, a1, _elems=<z3.z3core.Elementaries object>)
-
Z3_mk_char_from_bv( - a0, -@@ -1705,7 +1817,12 @@ Data descriptors defined here:
- _elems=<z3.z3core.Elementaries object> - )
-
Z3_mk_config(_elems=<z3.z3core.Elementaries object>)
--
Z3_mk_const(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)
-+
Z3_mk_const( -+ a0, -+ a1, -+ a2, -+ _elems=<z3.z3core.Elementaries object> -+)
-
Z3_mk_const_array( - a0, - a1, -@@ -1765,7 +1882,11 @@ Data descriptors defined here:
- a2, - _elems=<z3.z3core.Elementaries object> - )
--
Z3_mk_empty_set(a0, a1, _elems=<z3.z3core.Elementaries object>)
-+
Z3_mk_empty_set( -+ a0, -+ a1, -+ _elems=<z3.z3core.Elementaries object> -+)
-
Z3_mk_enumeration_sort( - a0, - a1, -@@ -2056,7 +2177,10 @@ Data descriptors defined here:
- a0, - _elems=<z3.z3core.Elementaries object> - )
--
Z3_mk_fpa_sort_half(a0, _elems=<z3.z3core.Elementaries object>)
-+
Z3_mk_fpa_sort_half( -+ a0, -+ _elems=<z3.z3core.Elementaries object> -+)
-
Z3_mk_fpa_sort_quadruple( - a0, - _elems=<z3.z3core.Elementaries object> -@@ -2197,7 +2321,12 @@ Data descriptors defined here:
- _elems=<z3.z3core.Elementaries object> - )
-
Z3_mk_int2real(a0, a1, _elems=<z3.z3core.Elementaries object>)
--
Z3_mk_int64(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)
-+
Z3_mk_int64( -+ a0, -+ a1, -+ a2, -+ _elems=<z3.z3core.Elementaries object> -+)
-
Z3_mk_int_sort(a0, _elems=<z3.z3core.Elementaries object>)
-
Z3_mk_int_symbol( - a0, -@@ -2333,7 +2462,12 @@ Data descriptors defined here:
- a5, - _elems=<z3.z3core.Elementaries object> - )
--
Z3_mk_power(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)
-+
Z3_mk_power( -+ a0, -+ a1, -+ a2, -+ _elems=<z3.z3core.Elementaries object> -+)
-
Z3_mk_probe(a0, a1, _elems=<z3.z3core.Elementaries object>)
-
Z3_mk_quantifier( - a0, -@@ -2426,7 +2560,11 @@ Data descriptors defined here:
- a3, - _elems=<z3.z3core.Elementaries object> - )
--
Z3_mk_re_option(a0, a1, _elems=<z3.z3core.Elementaries object>)
-+
Z3_mk_re_option( -+ a0, -+ a1, -+ _elems=<z3.z3core.Elementaries object> -+)
-
Z3_mk_re_plus(a0, a1, _elems=<z3.z3core.Elementaries object>)
-
Z3_mk_re_power( - a0, -@@ -2520,7 +2658,11 @@ Data descriptors defined here:
- a2, - _elems=<z3.z3core.Elementaries object> - )
--
Z3_mk_seq_empty(a0, a1, _elems=<z3.z3core.Elementaries object>)
-+
Z3_mk_seq_empty( -+ a0, -+ a1, -+ _elems=<z3.z3core.Elementaries object> -+)
-
Z3_mk_seq_extract( - a0, - a1, -@@ -2627,7 +2769,11 @@ Data descriptors defined here:
- a2, - _elems=<z3.z3core.Elementaries object> - )
--
Z3_mk_seq_to_re(a0, a1, _elems=<z3.z3core.Elementaries object>)
-+
Z3_mk_seq_to_re( -+ a0, -+ a1, -+ _elems=<z3.z3core.Elementaries object> -+)
-
Z3_mk_seq_unit(a0, a1, _elems=<z3.z3core.Elementaries object>)
-
Z3_mk_set_add( - a0, -@@ -2683,7 +2829,10 @@ Data descriptors defined here:
- a2, - _elems=<z3.z3core.Elementaries object> - )
--
Z3_mk_simple_solver(a0, _elems=<z3.z3core.Elementaries object>)
-+
Z3_mk_simple_solver( -+ a0, -+ _elems=<z3.z3core.Elementaries object> -+)
-
Z3_mk_simplifier( - a0, - a1, -@@ -3052,7 +3201,11 @@ Data descriptors defined here:
- a2, - _elems=<z3.z3core.Elementaries object> - )
--
Z3_optimize_pop(a0, a1, _elems=<z3.z3core.Elementaries object>)
-+
Z3_optimize_pop( -+ a0, -+ a1, -+ _elems=<z3.z3core.Elementaries object> -+)
-
Z3_optimize_push( - a0, - a1, -@@ -3288,8 +3441,18 @@ Data descriptors defined here:
- a1, - _elems=<z3.z3core.Elementaries object> - )
--
Z3_probe_eq(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)
--
Z3_probe_ge(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)
-+
Z3_probe_eq( -+ a0, -+ a1, -+ a2, -+ _elems=<z3.z3core.Elementaries object> -+)
-+
Z3_probe_ge( -+ a0, -+ a1, -+ a2, -+ _elems=<z3.z3core.Elementaries object> -+)
-
Z3_probe_get_descr( - a0, - a1, -@@ -3300,16 +3463,36 @@ Data descriptors defined here:
- a1, - _elems=<z3.z3core.Elementaries object> - )
--
Z3_probe_gt(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)
-+
Z3_probe_gt( -+ a0, -+ a1, -+ a2, -+ _elems=<z3.z3core.Elementaries object> -+)
-
Z3_probe_inc_ref( - a0, - a1, - _elems=<z3.z3core.Elementaries object> - )
--
Z3_probe_le(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)
--
Z3_probe_lt(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)
-+
Z3_probe_le( -+ a0, -+ a1, -+ a2, -+ _elems=<z3.z3core.Elementaries object> -+)
-+
Z3_probe_lt( -+ a0, -+ a1, -+ a2, -+ _elems=<z3.z3core.Elementaries object> -+)
-
Z3_probe_not(a0, a1, _elems=<z3.z3core.Elementaries object>)
--
Z3_probe_or(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)
-+
Z3_probe_or( -+ a0, -+ a1, -+ a2, -+ _elems=<z3.z3core.Elementaries object> -+)
-
Z3_qe_lite(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)
-
Z3_qe_model_project( - a0, -@@ -3605,7 +3788,11 @@ Data descriptors defined here:
- a3, - _elems=<z3.z3core.Elementaries object> - )
--
Z3_solver_check(a0, a1, _elems=<z3.z3core.Elementaries object>)
-+
Z3_solver_check( -+ a0, -+ a1, -+ _elems=<z3.z3core.Elementaries object> -+)
-
Z3_solver_check_assumptions( - a0, - a1, -@@ -3862,7 +4049,11 @@ Data descriptors defined here:
- a3, - _elems=<z3.z3core.Elementaries object> - )
--
Z3_solver_reset(a0, a1, _elems=<z3.z3core.Elementaries object>)
-+
Z3_solver_reset( -+ a0, -+ a1, -+ _elems=<z3.z3core.Elementaries object> -+)
-
Z3_solver_set_initial_value( - a0, - a1, -@@ -4118,7 +4309,11 @@ Data descriptors defined here:
- _elems=<z3.z3core.Elementaries object> - )
-
Z3_to_app(a0, a1, _elems=<z3.z3core.Elementaries object>)
--
Z3_to_func_decl(a0, a1, _elems=<z3.z3core.Elementaries object>)
-+
Z3_to_func_decl( -+ a0, -+ a1, -+ _elems=<z3.z3core.Elementaries object> -+)
-
Z3_toggle_warning_messages( - a0, - _elems=<z3.z3core.Elementaries object> diff --git a/z3.spec b/z3.spec index 10b7f4b..3c1df16 100644 --- a/z3.spec +++ b/z3.spec @@ -15,7 +15,7 @@ %bcond test 0 Name: z3 -Version: 5.0.0 +Version: 5.1.0 Release: %autorelease Summary: Satisfiability Modulo Theories (SMT) solver @@ -244,7 +244,7 @@ cd - %files libs %license LICENSE.txt -%{_libdir}/libz3.so.5.0{,.*} +%{_libdir}/libz3.so.5.1{,.*} %files devel %{_includedir}/z3/