From 2a1214c7dc9cf08b04ed588837a72120d8d52e44 Mon Sep 17 00:00:00 2001 From: "Richard W.M. Jones" Date: Mon, 1 Mar 2021 16:57:46 +0000 Subject: [PATCH 01/94] OCaml 4.12.0 build --- z3.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/z3.spec b/z3.spec index ec018e5..0068d0c 100644 --- a/z3.spec +++ b/z3.spec @@ -1,6 +1,6 @@ Name: z3 Version: 4.8.10 -Release: 1%{?dist} +Release: 2%{?dist} Summary: Satisfiability Modulo Theories (SMT) solver License: MIT @@ -231,6 +231,9 @@ help2man -N -o %{buildroot}%{_mandir}/man1/%{name}.1 %{_vpath_builddir}/%{name} %{python3_sitelib}/%{name}/ %changelog +* Mon Mar 1 16:57:45 GMT 2021 Richard W.M. Jones - 4.8.10-2 +- OCaml 4.12.0 build + * Sat Feb 13 2021 Jerry James - 4.8.10-1 - Version 4.8.10 From 813e7005573c742dd214d9e994ccb983c82c97bd Mon Sep 17 00:00:00 2001 From: "Richard W.M. Jones" Date: Mon, 1 Mar 2021 19:41:17 +0000 Subject: [PATCH 02/94] Bump release and rebuild. --- z3.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/z3.spec b/z3.spec index 0068d0c..1fdd413 100644 --- a/z3.spec +++ b/z3.spec @@ -1,6 +1,6 @@ Name: z3 Version: 4.8.10 -Release: 2%{?dist} +Release: 3%{?dist} Summary: Satisfiability Modulo Theories (SMT) solver License: MIT @@ -231,6 +231,9 @@ help2man -N -o %{buildroot}%{_mandir}/man1/%{name}.1 %{_vpath_builddir}/%{name} %{python3_sitelib}/%{name}/ %changelog +* Mon Mar 1 19:41:16 GMT 2021 Richard W.M. Jones - 4.8.10-3 +- Bump release and rebuild. + * Mon Mar 1 16:57:45 GMT 2021 Richard W.M. Jones - 4.8.10-2 - OCaml 4.12.0 build From bad77dc61244d62438ec7835029c9bb835095d84 Mon Sep 17 00:00:00 2001 From: "Richard W.M. Jones" Date: Mon, 1 Mar 2021 20:17:49 +0000 Subject: [PATCH 03/94] Bump release and rebuild. --- z3.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/z3.spec b/z3.spec index 1fdd413..18bc0c4 100644 --- a/z3.spec +++ b/z3.spec @@ -1,6 +1,6 @@ Name: z3 Version: 4.8.10 -Release: 3%{?dist} +Release: 4%{?dist} Summary: Satisfiability Modulo Theories (SMT) solver License: MIT @@ -231,6 +231,9 @@ help2man -N -o %{buildroot}%{_mandir}/man1/%{name}.1 %{_vpath_builddir}/%{name} %{python3_sitelib}/%{name}/ %changelog +* Mon Mar 1 20:17:48 GMT 2021 Richard W.M. Jones - 4.8.10-4 +- Bump release and rebuild. + * Mon Mar 1 19:41:16 GMT 2021 Richard W.M. Jones - 4.8.10-3 - Bump release and rebuild. From b504b06e75c2802f50dc676f32757c22fecc6915 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Wed, 3 Mar 2021 12:11:52 -0700 Subject: [PATCH 04/94] Rebuild for ocaml-zarith 1.12. --- z3.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/z3.spec b/z3.spec index 18bc0c4..0bfff89 100644 --- a/z3.spec +++ b/z3.spec @@ -1,6 +1,6 @@ Name: z3 Version: 4.8.10 -Release: 4%{?dist} +Release: 5%{?dist} Summary: Satisfiability Modulo Theories (SMT) solver License: MIT @@ -231,6 +231,9 @@ help2man -N -o %{buildroot}%{_mandir}/man1/%{name}.1 %{_vpath_builddir}/%{name} %{python3_sitelib}/%{name}/ %changelog +* Wed Mar 3 2021 Jerry James - 4.8.10-5 +- Rebuild for ocaml-zarith 1.12 + * Mon Mar 1 20:17:48 GMT 2021 Richard W.M. Jones - 4.8.10-4 - Bump release and rebuild. From 57bf5789d2ee5160723c28e3362fc5dd67bf3952 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Wed, 3 Mar 2021 12:11:52 -0700 Subject: [PATCH 05/94] Rebuild for ocaml-zarith 1.12. --- z3.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/z3.spec b/z3.spec index ec018e5..d5daf57 100644 --- a/z3.spec +++ b/z3.spec @@ -1,6 +1,6 @@ Name: z3 Version: 4.8.10 -Release: 1%{?dist} +Release: 2%{?dist} Summary: Satisfiability Modulo Theories (SMT) solver License: MIT @@ -231,6 +231,9 @@ help2man -N -o %{buildroot}%{_mandir}/man1/%{name}.1 %{_vpath_builddir}/%{name} %{python3_sitelib}/%{name}/ %changelog +* Wed Mar 3 2021 Jerry James - 4.8.10-2 +- Rebuild for ocaml-zarith 1.12 + * Sat Feb 13 2021 Jerry James - 4.8.10-1 - Version 4.8.10 From 306bdba1f5475f8ef01330599ba5346e8eb33cb8 Mon Sep 17 00:00:00 2001 From: Python Maint Date: Fri, 4 Jun 2021 21:20:40 +0200 Subject: [PATCH 06/94] Rebuilt for Python 3.10 --- z3.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/z3.spec b/z3.spec index 0bfff89..6213fa0 100644 --- a/z3.spec +++ b/z3.spec @@ -1,6 +1,6 @@ Name: z3 Version: 4.8.10 -Release: 5%{?dist} +Release: 6%{?dist} Summary: Satisfiability Modulo Theories (SMT) solver License: MIT @@ -231,6 +231,9 @@ help2man -N -o %{buildroot}%{_mandir}/man1/%{name}.1 %{_vpath_builddir}/%{name} %{python3_sitelib}/%{name}/ %changelog +* Fri Jun 04 2021 Python Maint - 4.8.10-6 +- Rebuilt for Python 3.10 + * Wed Mar 3 2021 Jerry James - 4.8.10-5 - Rebuild for ocaml-zarith 1.12 From 61301a359dd029a4fd1404848de1174661e6954e Mon Sep 17 00:00:00 2001 From: Jerry James Date: Tue, 8 Jun 2021 08:27:35 -0600 Subject: [PATCH 07/94] Version 4.8.11. --- sources | 2 +- z3.spec | 7 +++++-- 2 files changed, 6 insertions(+), 3 deletions(-) diff --git a/sources b/sources index 6e928b0..4762877 100644 --- a/sources +++ b/sources @@ -1 +1 @@ -SHA512 (z3-4.8.10.tar.gz) = d2741d7ad3e1d5ee3fec92095b061a96a700c3327b2eb2090d4162bdcaeaebca8c072ef79c5daac1f6de3456165c2cc38e13f1045bc707779d1027b943837c5b +SHA512 (z3-4.8.11.tar.gz) = ceab703d0413d0135e0f4e6c3ba2bb58d6a4823385edb0bf7ecc96949a3073b687d415a2674c86c9f876adb52823f98f9fbbc107d799ed756dc16292f9864894 diff --git a/z3.spec b/z3.spec index 6213fa0..86ca090 100644 --- a/z3.spec +++ b/z3.spec @@ -1,6 +1,6 @@ Name: z3 -Version: 4.8.10 -Release: 6%{?dist} +Version: 4.8.11 +Release: 1%{?dist} Summary: Satisfiability Modulo Theories (SMT) solver License: MIT @@ -231,6 +231,9 @@ help2man -N -o %{buildroot}%{_mandir}/man1/%{name}.1 %{_vpath_builddir}/%{name} %{python3_sitelib}/%{name}/ %changelog +* Sun Jun 6 2021 Jerry James - 4.8.11-1 +- Version 4.8.11 + * Fri Jun 04 2021 Python Maint - 4.8.10-6 - Rebuilt for Python 3.10 From f68e634694abddd3f1c36f014162f0c49e757762 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Tue, 8 Jun 2021 08:27:35 -0600 Subject: [PATCH 08/94] Version 4.8.11. --- sources | 2 +- z3.spec | 7 +++++-- 2 files changed, 6 insertions(+), 3 deletions(-) diff --git a/sources b/sources index 6e928b0..4762877 100644 --- a/sources +++ b/sources @@ -1 +1 @@ -SHA512 (z3-4.8.10.tar.gz) = d2741d7ad3e1d5ee3fec92095b061a96a700c3327b2eb2090d4162bdcaeaebca8c072ef79c5daac1f6de3456165c2cc38e13f1045bc707779d1027b943837c5b +SHA512 (z3-4.8.11.tar.gz) = ceab703d0413d0135e0f4e6c3ba2bb58d6a4823385edb0bf7ecc96949a3073b687d415a2674c86c9f876adb52823f98f9fbbc107d799ed756dc16292f9864894 diff --git a/z3.spec b/z3.spec index d5daf57..ca162cb 100644 --- a/z3.spec +++ b/z3.spec @@ -1,6 +1,6 @@ Name: z3 -Version: 4.8.10 -Release: 2%{?dist} +Version: 4.8.11 +Release: 1%{?dist} Summary: Satisfiability Modulo Theories (SMT) solver License: MIT @@ -231,6 +231,9 @@ help2man -N -o %{buildroot}%{_mandir}/man1/%{name}.1 %{_vpath_builddir}/%{name} %{python3_sitelib}/%{name}/ %changelog +* Tue Jun 8 2021 Jerry James - 4.8.11-1 +- Version 4.8.11 + * Wed Mar 3 2021 Jerry James - 4.8.10-2 - Rebuild for ocaml-zarith 1.12 From 1db6cfa63f654406274f61aaa1b2804a66796c7c Mon Sep 17 00:00:00 2001 From: Jerry James Date: Tue, 13 Jul 2021 13:11:43 -0600 Subject: [PATCH 09/94] Version 4.8.12. --- sources | 2 +- z3.spec | 5 ++++- 2 files changed, 5 insertions(+), 2 deletions(-) diff --git a/sources b/sources index 4762877..6d9a0b2 100644 --- a/sources +++ b/sources @@ -1 +1 @@ -SHA512 (z3-4.8.11.tar.gz) = ceab703d0413d0135e0f4e6c3ba2bb58d6a4823385edb0bf7ecc96949a3073b687d415a2674c86c9f876adb52823f98f9fbbc107d799ed756dc16292f9864894 +SHA512 (z3-4.8.12.tar.gz) = 0b377923bdaffaca1846aa2abd61003bbecadfcdfc908ed3097d0aac8f32028ac39d93fb4a9c2e2c2bfffbdbee80aa415875f17de6c2ee2ae8e2b7921f788c6e diff --git a/z3.spec b/z3.spec index 86ca090..f670063 100644 --- a/z3.spec +++ b/z3.spec @@ -1,5 +1,5 @@ Name: z3 -Version: 4.8.11 +Version: 4.8.12 Release: 1%{?dist} Summary: Satisfiability Modulo Theories (SMT) solver @@ -231,6 +231,9 @@ help2man -N -o %{buildroot}%{_mandir}/man1/%{name}.1 %{_vpath_builddir}/%{name} %{python3_sitelib}/%{name}/ %changelog +* Tue Jul 13 2021 Jerry James - 4.8.12-1 +- Version 4.8.12 + * Sun Jun 6 2021 Jerry James - 4.8.11-1 - Version 4.8.11 From c5deed3cea715cb14eb90f04d2ea33b0cd3a6cd9 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Tue, 13 Jul 2021 13:11:43 -0600 Subject: [PATCH 10/94] Version 4.8.12. --- sources | 2 +- z3.spec | 5 ++++- 2 files changed, 5 insertions(+), 2 deletions(-) diff --git a/sources b/sources index 4762877..6d9a0b2 100644 --- a/sources +++ b/sources @@ -1 +1 @@ -SHA512 (z3-4.8.11.tar.gz) = ceab703d0413d0135e0f4e6c3ba2bb58d6a4823385edb0bf7ecc96949a3073b687d415a2674c86c9f876adb52823f98f9fbbc107d799ed756dc16292f9864894 +SHA512 (z3-4.8.12.tar.gz) = 0b377923bdaffaca1846aa2abd61003bbecadfcdfc908ed3097d0aac8f32028ac39d93fb4a9c2e2c2bfffbdbee80aa415875f17de6c2ee2ae8e2b7921f788c6e diff --git a/z3.spec b/z3.spec index ca162cb..a277c7d 100644 --- a/z3.spec +++ b/z3.spec @@ -1,5 +1,5 @@ Name: z3 -Version: 4.8.11 +Version: 4.8.12 Release: 1%{?dist} Summary: Satisfiability Modulo Theories (SMT) solver @@ -231,6 +231,9 @@ help2man -N -o %{buildroot}%{_mandir}/man1/%{name}.1 %{_vpath_builddir}/%{name} %{python3_sitelib}/%{name}/ %changelog +* Tue Jul 13 2021 Jerry James - 4.8.12-1 +- Version 4.8.12 + * Tue Jun 8 2021 Jerry James - 4.8.11-1 - Version 4.8.11 From 969a5ffd2198154c54e041b7b4c72ae12fafd6ab Mon Sep 17 00:00:00 2001 From: Fedora Release Engineering Date: Fri, 23 Jul 2021 22:12:33 +0000 Subject: [PATCH 11/94] - Rebuilt for https://fedoraproject.org/wiki/Fedora_35_Mass_Rebuild Signed-off-by: Fedora Release Engineering --- z3.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/z3.spec b/z3.spec index f670063..8317af8 100644 --- a/z3.spec +++ b/z3.spec @@ -1,6 +1,6 @@ Name: z3 Version: 4.8.12 -Release: 1%{?dist} +Release: 2%{?dist} Summary: Satisfiability Modulo Theories (SMT) solver License: MIT @@ -231,6 +231,9 @@ help2man -N -o %{buildroot}%{_mandir}/man1/%{name}.1 %{_vpath_builddir}/%{name} %{python3_sitelib}/%{name}/ %changelog +* Fri Jul 23 2021 Fedora Release Engineering - 4.8.12-2 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_35_Mass_Rebuild + * Tue Jul 13 2021 Jerry James - 4.8.12-1 - Version 4.8.12 From 25c7a7705b7e389b5cd28b35c759bc33470bf430 Mon Sep 17 00:00:00 2001 From: "Richard W.M. Jones" Date: Mon, 4 Oct 2021 20:45:36 +0100 Subject: [PATCH 12/94] OCaml 4.13.1 build --- z3.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/z3.spec b/z3.spec index 8317af8..cbe65a9 100644 --- a/z3.spec +++ b/z3.spec @@ -1,6 +1,6 @@ Name: z3 Version: 4.8.12 -Release: 2%{?dist} +Release: 3%{?dist} Summary: Satisfiability Modulo Theories (SMT) solver License: MIT @@ -231,6 +231,9 @@ help2man -N -o %{buildroot}%{_mandir}/man1/%{name}.1 %{_vpath_builddir}/%{name} %{python3_sitelib}/%{name}/ %changelog +* Mon Oct 04 2021 Richard W.M. Jones - 4.8.12-3 +- OCaml 4.13.1 build + * Fri Jul 23 2021 Fedora Release Engineering - 4.8.12-2 - Rebuilt for https://fedoraproject.org/wiki/Fedora_35_Mass_Rebuild From 533bf73c99a719a38e1eaf1e33645480f485327b Mon Sep 17 00:00:00 2001 From: Jerry James Date: Fri, 19 Nov 2021 12:28:26 -0700 Subject: [PATCH 13/94] Version 4.8.13. --- README.md | 5 +++++ sources | 2 +- z3.spec | 14 +++++++------- 3 files changed, 13 insertions(+), 8 deletions(-) create mode 100644 README.md diff --git a/README.md b/README.md new file mode 100644 index 0000000..fcd0204 --- /dev/null +++ b/README.md @@ -0,0 +1,5 @@ +# z3 + +[Z3](https://github.com/Z3Prover/z3) is a theorem prover from Microsoft +Research. If you are not familiar with Z3, you can start +[here](https://github.com/Z3Prover/z3/wiki#background). diff --git a/sources b/sources index 6d9a0b2..9e39523 100644 --- a/sources +++ b/sources @@ -1 +1 @@ -SHA512 (z3-4.8.12.tar.gz) = 0b377923bdaffaca1846aa2abd61003bbecadfcdfc908ed3097d0aac8f32028ac39d93fb4a9c2e2c2bfffbdbee80aa415875f17de6c2ee2ae8e2b7921f788c6e +SHA512 (z3-4.8.13.tar.gz) = c5e8f34525ed3b6b2935d7f01ce2f90f5dd99b4cdd035664b36c967fb1c7f3b05abed45c7288e2261723e73d68728ee91a0f67d92012d86b04598d7b54369c30 diff --git a/z3.spec b/z3.spec index cbe65a9..c5e9523 100644 --- a/z3.spec +++ b/z3.spec @@ -1,6 +1,6 @@ Name: z3 -Version: 4.8.12 -Release: 3%{?dist} +Version: 4.8.13 +Release: 1%{?dist} Summary: Satisfiability Modulo Theories (SMT) solver License: MIT @@ -97,7 +97,7 @@ sed \ -e '/O3/d' \ -e "s/\(['\"]\)cp\([^[:alnum:]]\)/\1cp -p\2/" \ -e "s/\(SLIBEXTRAFLAGS = '\)'/\1-Wl,--no-whole-archive -Wl,--as-needed'/" \ - -e "/SLIBFLAGS/s|-shared|& $RPM_LD_FLAGS -Wl,--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/OCAML_FLAGS = ''/OCAML_FLAGS = '-g'/" \ -i scripts/mk_util.py @@ -111,16 +111,13 @@ sed -e '/libz3java/s,\(System\.load\)Library("\(.*\)"),\1("%{_libdir}/z3/\2.so") # Update an OCaml interface sed -i 's/Pervasives/Stdlib/' src/api/ml/z3.ml -# FIXME: For unknown reasons, cmake replaces the version with nothing at all -sed -i 's/@VERSION@/%{version}/' z3.pc.cmake.in - # Fix character encoding iconv -f iso8859-1 -t utf-8 RELEASE_NOTES > RELEASE_NOTES.utf8 touch -r RELEASE_NOTES RELEASE_NOTES.utf8 mv -f RELEASE_NOTES.utf8 RELEASE_NOTES %build -export CXXFLAGS="$RPM_OPT_FLAGS" +export CXXFLAGS="%{build_cxxflags}" export LANG="C.UTF-8" export PYTHON="%{python3}" @@ -231,6 +228,9 @@ help2man -N -o %{buildroot}%{_mandir}/man1/%{name}.1 %{_vpath_builddir}/%{name} %{python3_sitelib}/%{name}/ %changelog +* Fri Nov 19 2021 Jerry James - 4.8.13-1 +- Version 4.8.13 + * Mon Oct 04 2021 Richard W.M. Jones - 4.8.12-3 - OCaml 4.13.1 build From cd0cb0d441f0f4ba866004ef796d09ffe75fdf89 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Fri, 19 Nov 2021 12:28:26 -0700 Subject: [PATCH 14/94] Version 4.8.13. --- README.md | 5 +++++ sources | 2 +- z3.spec | 12 ++++++------ 3 files changed, 12 insertions(+), 7 deletions(-) create mode 100644 README.md diff --git a/README.md b/README.md new file mode 100644 index 0000000..fcd0204 --- /dev/null +++ b/README.md @@ -0,0 +1,5 @@ +# z3 + +[Z3](https://github.com/Z3Prover/z3) is a theorem prover from Microsoft +Research. If you are not familiar with Z3, you can start +[here](https://github.com/Z3Prover/z3/wiki#background). diff --git a/sources b/sources index 6d9a0b2..9e39523 100644 --- a/sources +++ b/sources @@ -1 +1 @@ -SHA512 (z3-4.8.12.tar.gz) = 0b377923bdaffaca1846aa2abd61003bbecadfcdfc908ed3097d0aac8f32028ac39d93fb4a9c2e2c2bfffbdbee80aa415875f17de6c2ee2ae8e2b7921f788c6e +SHA512 (z3-4.8.13.tar.gz) = c5e8f34525ed3b6b2935d7f01ce2f90f5dd99b4cdd035664b36c967fb1c7f3b05abed45c7288e2261723e73d68728ee91a0f67d92012d86b04598d7b54369c30 diff --git a/z3.spec b/z3.spec index a277c7d..d5b5caf 100644 --- a/z3.spec +++ b/z3.spec @@ -1,5 +1,5 @@ Name: z3 -Version: 4.8.12 +Version: 4.8.13 Release: 1%{?dist} Summary: Satisfiability Modulo Theories (SMT) solver @@ -97,7 +97,7 @@ sed \ -e '/O3/d' \ -e "s/\(['\"]\)cp\([^[:alnum:]]\)/\1cp -p\2/" \ -e "s/\(SLIBEXTRAFLAGS = '\)'/\1-Wl,--no-whole-archive -Wl,--as-needed'/" \ - -e "/SLIBFLAGS/s|-shared|& $RPM_LD_FLAGS -Wl,--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/OCAML_FLAGS = ''/OCAML_FLAGS = '-g'/" \ -i scripts/mk_util.py @@ -111,16 +111,13 @@ sed -e '/libz3java/s,\(System\.load\)Library("\(.*\)"),\1("%{_libdir}/z3/\2.so") # Update an OCaml interface sed -i 's/Pervasives/Stdlib/' src/api/ml/z3.ml -# FIXME: For unknown reasons, cmake replaces the version with nothing at all -sed -i 's/@VERSION@/%{version}/' z3.pc.cmake.in - # Fix character encoding iconv -f iso8859-1 -t utf-8 RELEASE_NOTES > RELEASE_NOTES.utf8 touch -r RELEASE_NOTES RELEASE_NOTES.utf8 mv -f RELEASE_NOTES.utf8 RELEASE_NOTES %build -export CXXFLAGS="$RPM_OPT_FLAGS" +export CXXFLAGS="%{build_cxxflags}" export LANG="C.UTF-8" export PYTHON="%{python3}" @@ -231,6 +228,9 @@ help2man -N -o %{buildroot}%{_mandir}/man1/%{name}.1 %{_vpath_builddir}/%{name} %{python3_sitelib}/%{name}/ %changelog +* Fri Nov 19 2021 Jerry James - 4.8.13-1 +- Version 4.8.13 + * Tue Jul 13 2021 Jerry James - 4.8.12-1 - Version 4.8.12 From 6ffdbbf84343337c661e2be295caf139c29137e4 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Fri, 24 Dec 2021 11:30:57 -0700 Subject: [PATCH 15/94] Version 4.8.14. Conditionalize the %check script. --- sources | 2 +- z3.spec | 29 +++++++++++++++++------------ 2 files changed, 18 insertions(+), 13 deletions(-) diff --git a/sources b/sources index 9e39523..d3aac3a 100644 --- a/sources +++ b/sources @@ -1 +1 @@ -SHA512 (z3-4.8.13.tar.gz) = c5e8f34525ed3b6b2935d7f01ce2f90f5dd99b4cdd035664b36c967fb1c7f3b05abed45c7288e2261723e73d68728ee91a0f67d92012d86b04598d7b54369c30 +SHA512 (z3-4.8.14.tar.gz) = 10170516ca472258d2f9df28cd036e43023a76a25f1e1670290c62f3890d935bf82770970054a5fd3a0f02559409e7ed4b18fb08347c040ff2f9e0918e152aab diff --git a/z3.spec b/z3.spec index c5e9523..9cde9a2 100644 --- a/z3.spec +++ b/z3.spec @@ -1,5 +1,9 @@ +# Tests are off by default because some of the tests require more memory than +# the koji builders have available. +%bcond_with test + Name: z3 -Version: 4.8.13 +Version: 4.8.14 Release: 1%{?dist} Summary: Satisfiability Modulo Theories (SMT) solver @@ -108,9 +112,6 @@ sed -e '/libz3java/s,\(System\.load\)Library("\(.*\)"),\1("%{_libdir}/z3/\2.so") -e "s/@MAJVER@/$majver/" \ -i scripts/update_api.py -# Update an OCaml interface -sed -i 's/Pervasives/Stdlib/' src/api/ml/z3.ml - # Fix character encoding iconv -f iso8859-1 -t utf-8 RELEASE_NOTES > RELEASE_NOTES.utf8 touch -r RELEASE_NOTES RELEASE_NOTES.utf8 @@ -178,14 +179,14 @@ rm -rf %{buildroot}%{_docdir}/Z3 mkdir -p %{buildroot}%{_mandir}/man1 help2man -N -o %{buildroot}%{_mandir}/man1/%{name}.1 %{_vpath_builddir}/%{name} -#%%check -# Some of the tests require more memory than the koji builders have available. -# -#export LANG="C.UTF-8" -#pushd build -#make test-z3 -#./test-z3 /a -#popd +%if %{with test} +%check +export LANG="C.UTF-8" +cd build +make test-z3 +./test-z3 /a +cd - +%endif %files %doc README.md RELEASE_NOTES @@ -228,6 +229,10 @@ help2man -N -o %{buildroot}%{_mandir}/man1/%{name}.1 %{_vpath_builddir}/%{name} %{python3_sitelib}/%{name}/ %changelog +* Fri Dec 24 2021 Jerry James - 4.8.14-1 +- Version 4.8.14 +- Conditionalize the %%check script + * Fri Nov 19 2021 Jerry James - 4.8.13-1 - Version 4.8.13 From a41041377d554a995159adf7ea620ed37bc708d3 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Fri, 24 Dec 2021 11:30:57 -0700 Subject: [PATCH 16/94] Version 4.8.14. Conditionalize the %check script. --- sources | 2 +- z3.spec | 29 +++++++++++++++++------------ 2 files changed, 18 insertions(+), 13 deletions(-) diff --git a/sources b/sources index 9e39523..d3aac3a 100644 --- a/sources +++ b/sources @@ -1 +1 @@ -SHA512 (z3-4.8.13.tar.gz) = c5e8f34525ed3b6b2935d7f01ce2f90f5dd99b4cdd035664b36c967fb1c7f3b05abed45c7288e2261723e73d68728ee91a0f67d92012d86b04598d7b54369c30 +SHA512 (z3-4.8.14.tar.gz) = 10170516ca472258d2f9df28cd036e43023a76a25f1e1670290c62f3890d935bf82770970054a5fd3a0f02559409e7ed4b18fb08347c040ff2f9e0918e152aab diff --git a/z3.spec b/z3.spec index d5b5caf..110df81 100644 --- a/z3.spec +++ b/z3.spec @@ -1,5 +1,9 @@ +# Tests are off by default because some of the tests require more memory than +# the koji builders have available. +%bcond_with test + Name: z3 -Version: 4.8.13 +Version: 4.8.14 Release: 1%{?dist} Summary: Satisfiability Modulo Theories (SMT) solver @@ -108,9 +112,6 @@ sed -e '/libz3java/s,\(System\.load\)Library("\(.*\)"),\1("%{_libdir}/z3/\2.so") -e "s/@MAJVER@/$majver/" \ -i scripts/update_api.py -# Update an OCaml interface -sed -i 's/Pervasives/Stdlib/' src/api/ml/z3.ml - # Fix character encoding iconv -f iso8859-1 -t utf-8 RELEASE_NOTES > RELEASE_NOTES.utf8 touch -r RELEASE_NOTES RELEASE_NOTES.utf8 @@ -178,14 +179,14 @@ rm -rf %{buildroot}%{_docdir}/Z3 mkdir -p %{buildroot}%{_mandir}/man1 help2man -N -o %{buildroot}%{_mandir}/man1/%{name}.1 %{_vpath_builddir}/%{name} -#%%check -# Some of the tests require more memory than the koji builders have available. -# -#export LANG="C.UTF-8" -#pushd build -#make test-z3 -#./test-z3 /a -#popd +%if %{with test} +%check +export LANG="C.UTF-8" +cd build +make test-z3 +./test-z3 /a +cd - +%endif %files %doc README.md RELEASE_NOTES @@ -228,6 +229,10 @@ help2man -N -o %{buildroot}%{_mandir}/man1/%{name}.1 %{_vpath_builddir}/%{name} %{python3_sitelib}/%{name}/ %changelog +* Fri Dec 24 2021 Jerry James - 4.8.14-1 +- Version 4.8.14 +- Conditionalize the %%check script + * Fri Nov 19 2021 Jerry James - 4.8.13-1 - Version 4.8.13 From 4a9d6bf0fd0db5f3821bae66d3515994602fa7a2 Mon Sep 17 00:00:00 2001 From: Fedora Release Engineering Date: Sat, 22 Jan 2022 05:46:08 +0000 Subject: [PATCH 17/94] - Rebuilt for https://fedoraproject.org/wiki/Fedora_36_Mass_Rebuild Signed-off-by: Fedora Release Engineering --- z3.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/z3.spec b/z3.spec index 9cde9a2..e197c84 100644 --- a/z3.spec +++ b/z3.spec @@ -4,7 +4,7 @@ Name: z3 Version: 4.8.14 -Release: 1%{?dist} +Release: 2%{?dist} Summary: Satisfiability Modulo Theories (SMT) solver License: MIT @@ -229,6 +229,9 @@ cd - %{python3_sitelib}/%{name}/ %changelog +* Sat Jan 22 2022 Fedora Release Engineering - 4.8.14-2 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_36_Mass_Rebuild + * Fri Dec 24 2021 Jerry James - 4.8.14-1 - Version 4.8.14 - Conditionalize the %%check script From cea5f750e34373de7ce7686af639ab546ed627a3 Mon Sep 17 00:00:00 2001 From: "Richard W.M. Jones" Date: Fri, 4 Feb 2022 13:29:49 +0000 Subject: [PATCH 18/94] OCaml 4.13.1 rebuild to remove package notes --- z3.spec | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/z3.spec b/z3.spec index e197c84..ac4727b 100644 --- a/z3.spec +++ b/z3.spec @@ -1,10 +1,11 @@ +%undefine _package_note_flags # Tests are off by default because some of the tests require more memory than # the koji builders have available. %bcond_with test Name: z3 Version: 4.8.14 -Release: 2%{?dist} +Release: 3%{?dist} Summary: Satisfiability Modulo Theories (SMT) solver License: MIT @@ -229,6 +230,9 @@ cd - %{python3_sitelib}/%{name}/ %changelog +* Fri Feb 04 2022 Richard W.M. Jones - 4.8.14-3 +- OCaml 4.13.1 rebuild to remove package notes + * Sat Jan 22 2022 Fedora Release Engineering - 4.8.14-2 - Rebuilt for https://fedoraproject.org/wiki/Fedora_36_Mass_Rebuild From d4a35ac7196a3e22d0e4b3ac62ff2bb912da1e5e Mon Sep 17 00:00:00 2001 From: Jiri Date: Sun, 6 Feb 2022 00:53:17 +0100 Subject: [PATCH 19/94] Rebuilt for java-17-openjdk as system jdk https://fedoraproject.org/wiki/Changes/Java17 --- z3.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/z3.spec b/z3.spec index ac4727b..e0619fd 100644 --- a/z3.spec +++ b/z3.spec @@ -5,7 +5,7 @@ Name: z3 Version: 4.8.14 -Release: 3%{?dist} +Release: 4%{?dist} Summary: Satisfiability Modulo Theories (SMT) solver License: MIT @@ -230,6 +230,9 @@ cd - %{python3_sitelib}/%{name}/ %changelog +* Sat Feb 05 2022 Jiri Vanek - 4.8.14-4 +- Rebuilt for java-17-openjdk as system jdk + * Fri Feb 04 2022 Richard W.M. Jones - 4.8.14-3 - OCaml 4.13.1 rebuild to remove package notes From 0d4eb3e8f9c71a2bc657c542e7c9af9fbac798d8 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Mon, 21 Mar 2022 12:04:45 -0600 Subject: [PATCH 20/94] Version 4.8.15. --- sources | 2 +- z3.rpmlintrc | 25 ------------------------- z3.spec | 7 +++++-- 3 files changed, 6 insertions(+), 28 deletions(-) delete mode 100644 z3.rpmlintrc diff --git a/sources b/sources index d3aac3a..5ead29f 100644 --- a/sources +++ b/sources @@ -1 +1 @@ -SHA512 (z3-4.8.14.tar.gz) = 10170516ca472258d2f9df28cd036e43023a76a25f1e1670290c62f3890d935bf82770970054a5fd3a0f02559409e7ed4b18fb08347c040ff2f9e0918e152aab +SHA512 (z3-4.8.15.tar.gz) = 7b08dec5b035a38edc90c4c491f508fd9ed227357de94400169db53d4c59382bd6a81ae6615771023a06534a3aa92668844f0ebfcc2a3b5ef4bba957426a0c6c diff --git a/z3.rpmlintrc b/z3.rpmlintrc deleted file mode 100644 index 872eb7a..0000000 --- a/z3.rpmlintrc +++ /dev/null @@ -1,25 +0,0 @@ -# THIS FILE IS FOR WHITELISTING RPMLINT ERRORS AND WARNINGS IN TASKOTRON -# https://fedoraproject.org/wiki/Taskotron/Tasks/dist.rpmlint#Whitelisting_errors - -# The dictionary is missing some technical terms -addFilter(r'W: spelling-error .* ((S|s)atisfiability|datatypes)') - -# Shared objects in the python arch directory are not devel files -addFilter(r'python3-z3\.[^:]+: W: devel-file-in-non-devel-package .*libz3\.so') - -# The documentation is in the -doc subpackage -addFilter(r'W: no-documentation') - -# Oh yes, we have no manual page -addFilter(r'W: no-manual-page-for-binary z3') - -# The configure script is not an autotools-generated script -addFilter(r'z3\.spec:[^:]*: W: configure-without-libdir-spec') - -# The spec file moves the shared object from /usr/lib to /usr/lib64 on 64-bit -# systems, the opposite of the problem this warning is intended to catch. -addFilter(r'z3\.spec:[^:]+: E: hardcoded-library-path in %{_prefix}/lib/libz3\.so\*') - -# This is where JAR files are supposed to go when there is a binary interface. -addFilter(r'z3\.spec:[^:]+: E: hardcoded-library-path in %{_prefix}/lib/\*\.jar') -addFilter(r'z3\.spec:[^:]+: E: hardcoded-library-path in %{_prefix}/lib/lib%{name}java\.so') diff --git a/z3.spec b/z3.spec index e0619fd..e5cb053 100644 --- a/z3.spec +++ b/z3.spec @@ -4,8 +4,8 @@ %bcond_with test Name: z3 -Version: 4.8.14 -Release: 4%{?dist} +Version: 4.8.15 +Release: 1%{?dist} Summary: Satisfiability Modulo Theories (SMT) solver License: MIT @@ -230,6 +230,9 @@ cd - %{python3_sitelib}/%{name}/ %changelog +* Mon Mar 21 2022 Jerry James - 4.8.15-1 +- Version 4.8.15 + * Sat Feb 05 2022 Jiri Vanek - 4.8.14-4 - Rebuilt for java-17-openjdk as system jdk From d44508e7e33405407ea4222566f8a82e8e3108da Mon Sep 17 00:00:00 2001 From: Jerry James Date: Thu, 24 Mar 2022 13:58:33 -0600 Subject: [PATCH 21/94] Add -ambiguous-overload patch to fix cppcheck build failure. --- z3-ambiguous-overload.patch | 111 ++++++++++++++++++++++++++++++++++++ z3.spec | 8 ++- 2 files changed, 118 insertions(+), 1 deletion(-) create mode 100644 z3-ambiguous-overload.patch diff --git a/z3-ambiguous-overload.patch b/z3-ambiguous-overload.patch new file mode 100644 index 0000000..f50e3f4 --- /dev/null +++ b/z3-ambiguous-overload.patch @@ -0,0 +1,111 @@ +--- a/src/api/c++/z3++.h 2022-03-20 14:25:44.000000000 -0600 ++++ b/src/api/c++/z3++.h 2022-03-24 10:17:57.270766287 -0600 +@@ -2333,7 +2333,7 @@ namespace z3 { + + inline expr pble(expr_vector const& es, int const* coeffs, int bound) { + assert(es.size() > 0); +- context& ctx = es[0].ctx(); ++ context& ctx = es[0U].ctx(); + array _es(es); + Z3_ast r = Z3_mk_pble(ctx, _es.size(), _es.ptr(), coeffs, bound); + ctx.check_error(); +@@ -2341,7 +2341,7 @@ namespace z3 { + } + inline expr pbge(expr_vector const& es, int const* coeffs, int bound) { + assert(es.size() > 0); +- context& ctx = es[0].ctx(); ++ context& ctx = es[0U].ctx(); + array _es(es); + Z3_ast r = Z3_mk_pbge(ctx, _es.size(), _es.ptr(), coeffs, bound); + ctx.check_error(); +@@ -2349,7 +2349,7 @@ namespace z3 { + } + inline expr pbeq(expr_vector const& es, int const* coeffs, int bound) { + assert(es.size() > 0); +- context& ctx = es[0].ctx(); ++ context& ctx = es[0U].ctx(); + array _es(es); + Z3_ast r = Z3_mk_pbeq(ctx, _es.size(), _es.ptr(), coeffs, bound); + ctx.check_error(); +@@ -2357,7 +2357,7 @@ namespace z3 { + } + inline expr atmost(expr_vector const& es, unsigned bound) { + assert(es.size() > 0); +- context& ctx = es[0].ctx(); ++ context& ctx = es[0U].ctx(); + array _es(es); + Z3_ast r = Z3_mk_atmost(ctx, _es.size(), _es.ptr(), bound); + ctx.check_error(); +@@ -2365,7 +2365,7 @@ namespace z3 { + } + inline expr atleast(expr_vector const& es, unsigned bound) { + assert(es.size() > 0); +- context& ctx = es[0].ctx(); ++ context& ctx = es[0U].ctx(); + array _es(es); + Z3_ast r = Z3_mk_atleast(ctx, _es.size(), _es.ptr(), bound); + ctx.check_error(); +@@ -2373,7 +2373,7 @@ namespace z3 { + } + inline expr sum(expr_vector const& args) { + assert(args.size() > 0); +- context& ctx = args[0].ctx(); ++ context& ctx = args[0U].ctx(); + array _args(args); + Z3_ast r = Z3_mk_add(ctx, _args.size(), _args.ptr()); + ctx.check_error(); +@@ -2382,7 +2382,7 @@ namespace z3 { + + inline expr distinct(expr_vector const& args) { + assert(args.size() > 0); +- context& ctx = args[0].ctx(); ++ context& ctx = args[0U].ctx(); + array _args(args); + Z3_ast r = Z3_mk_distinct(ctx, _args.size(), _args.ptr()); + ctx.check_error(); +@@ -2411,14 +2411,14 @@ namespace z3 { + Z3_ast r; + assert(args.size() > 0); + if (args.size() == 1) { +- return args[0]; ++ return args[0U]; + } +- context& ctx = args[0].ctx(); ++ context& ctx = args[0U].ctx(); + array _args(args); +- if (Z3_is_seq_sort(ctx, args[0].get_sort())) { ++ if (Z3_is_seq_sort(ctx, args[0U].get_sort())) { + r = Z3_mk_seq_concat(ctx, _args.size(), _args.ptr()); + } +- else if (Z3_is_re_sort(ctx, args[0].get_sort())) { ++ else if (Z3_is_re_sort(ctx, args[0U].get_sort())) { + r = Z3_mk_re_concat(ctx, _args.size(), _args.ptr()); + } + else { +@@ -2448,7 +2448,7 @@ namespace z3 { + inline expr mk_xor(expr_vector const& args) { + if (args.empty()) + return args.ctx().bool_val(false); +- expr r = args[0]; ++ expr r = args[0U]; + for (unsigned i = 1; i < args.size(); ++i) + r = r ^ args[i]; + return r; +@@ -2771,7 +2771,7 @@ namespace z3 { + assert(!m_end && !m_empty); + m_cube = m_solver.cube(m_vars, m_cutoff); + m_cutoff = 0xFFFFFFFF; +- if (m_cube.size() == 1 && m_cube[0].is_false()) { ++ if (m_cube.size() == 1 && m_cube[0U].is_false()) { + m_cube = z3::expr_vector(m_solver.ctx()); + m_end = true; + } +@@ -3804,7 +3804,7 @@ namespace z3 { + } + inline expr re_intersect(expr_vector const& args) { + assert(args.size() > 0); +- context& ctx = args[0].ctx(); ++ context& ctx = args[0U].ctx(); + array _args(args); + Z3_ast r = Z3_mk_re_intersect(ctx, _args.size(), _args.ptr()); + ctx.check_error(); diff --git a/z3.spec b/z3.spec index e5cb053..decc836 100644 --- a/z3.spec +++ b/z3.spec @@ -5,7 +5,7 @@ Name: z3 Version: 4.8.15 -Release: 1%{?dist} +Release: 2%{?dist} Summary: Satisfiability Modulo Theories (SMT) solver License: MIT @@ -13,6 +13,9 @@ URL: https://github.com/Z3Prover/z3 Source0: https://github.com/Z3Prover/z3/archive/%{name}-%{version}.tar.gz # Change the way python finds the shared object; see bz 1910923 Patch0: %{name}-python.patch +# Resolve ambiguous overloads that prevent cppcheck from building +# See https://github.com/Z3Prover/z3/issues/5922 +Patch1: %{name}-ambiguous-overload.patch BuildRequires: cmake BuildRequires: doxygen @@ -230,6 +233,9 @@ cd - %{python3_sitelib}/%{name}/ %changelog +* Thu Mar 24 2022 Jerry James - 4.8.15-2 +- Add -ambiguous-overload patch to fix cppcheck build failure + * Mon Mar 21 2022 Jerry James - 4.8.15-1 - Version 4.8.15 From d11a9bc22b9be4a86ace3a9029abef9fdee005c2 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Thu, 19 May 2022 11:32:13 -0600 Subject: [PATCH 22/94] Version 4.8.17. Drop upstreamed -ambiguous-overload patch. --- sources | 2 +- z3-ambiguous-overload.patch | 111 ------------------------------------ z3.spec | 15 +++-- 3 files changed, 10 insertions(+), 118 deletions(-) delete mode 100644 z3-ambiguous-overload.patch diff --git a/sources b/sources index 5ead29f..957cc32 100644 --- a/sources +++ b/sources @@ -1 +1 @@ -SHA512 (z3-4.8.15.tar.gz) = 7b08dec5b035a38edc90c4c491f508fd9ed227357de94400169db53d4c59382bd6a81ae6615771023a06534a3aa92668844f0ebfcc2a3b5ef4bba957426a0c6c +SHA512 (z3-4.8.17.tar.gz) = 95517014ec1798c2552253dd5cde6f955896ab297a4f56294f4bc6f2c5428069015f513c6eb9a090a809cfcf4cb1cc38cc83818f19b5b1051e4e6c06f973747d diff --git a/z3-ambiguous-overload.patch b/z3-ambiguous-overload.patch deleted file mode 100644 index f50e3f4..0000000 --- a/z3-ambiguous-overload.patch +++ /dev/null @@ -1,111 +0,0 @@ ---- a/src/api/c++/z3++.h 2022-03-20 14:25:44.000000000 -0600 -+++ b/src/api/c++/z3++.h 2022-03-24 10:17:57.270766287 -0600 -@@ -2333,7 +2333,7 @@ namespace z3 { - - inline expr pble(expr_vector const& es, int const* coeffs, int bound) { - assert(es.size() > 0); -- context& ctx = es[0].ctx(); -+ context& ctx = es[0U].ctx(); - array _es(es); - Z3_ast r = Z3_mk_pble(ctx, _es.size(), _es.ptr(), coeffs, bound); - ctx.check_error(); -@@ -2341,7 +2341,7 @@ namespace z3 { - } - inline expr pbge(expr_vector const& es, int const* coeffs, int bound) { - assert(es.size() > 0); -- context& ctx = es[0].ctx(); -+ context& ctx = es[0U].ctx(); - array _es(es); - Z3_ast r = Z3_mk_pbge(ctx, _es.size(), _es.ptr(), coeffs, bound); - ctx.check_error(); -@@ -2349,7 +2349,7 @@ namespace z3 { - } - inline expr pbeq(expr_vector const& es, int const* coeffs, int bound) { - assert(es.size() > 0); -- context& ctx = es[0].ctx(); -+ context& ctx = es[0U].ctx(); - array _es(es); - Z3_ast r = Z3_mk_pbeq(ctx, _es.size(), _es.ptr(), coeffs, bound); - ctx.check_error(); -@@ -2357,7 +2357,7 @@ namespace z3 { - } - inline expr atmost(expr_vector const& es, unsigned bound) { - assert(es.size() > 0); -- context& ctx = es[0].ctx(); -+ context& ctx = es[0U].ctx(); - array _es(es); - Z3_ast r = Z3_mk_atmost(ctx, _es.size(), _es.ptr(), bound); - ctx.check_error(); -@@ -2365,7 +2365,7 @@ namespace z3 { - } - inline expr atleast(expr_vector const& es, unsigned bound) { - assert(es.size() > 0); -- context& ctx = es[0].ctx(); -+ context& ctx = es[0U].ctx(); - array _es(es); - Z3_ast r = Z3_mk_atleast(ctx, _es.size(), _es.ptr(), bound); - ctx.check_error(); -@@ -2373,7 +2373,7 @@ namespace z3 { - } - inline expr sum(expr_vector const& args) { - assert(args.size() > 0); -- context& ctx = args[0].ctx(); -+ context& ctx = args[0U].ctx(); - array _args(args); - Z3_ast r = Z3_mk_add(ctx, _args.size(), _args.ptr()); - ctx.check_error(); -@@ -2382,7 +2382,7 @@ namespace z3 { - - inline expr distinct(expr_vector const& args) { - assert(args.size() > 0); -- context& ctx = args[0].ctx(); -+ context& ctx = args[0U].ctx(); - array _args(args); - Z3_ast r = Z3_mk_distinct(ctx, _args.size(), _args.ptr()); - ctx.check_error(); -@@ -2411,14 +2411,14 @@ namespace z3 { - Z3_ast r; - assert(args.size() > 0); - if (args.size() == 1) { -- return args[0]; -+ return args[0U]; - } -- context& ctx = args[0].ctx(); -+ context& ctx = args[0U].ctx(); - array _args(args); -- if (Z3_is_seq_sort(ctx, args[0].get_sort())) { -+ if (Z3_is_seq_sort(ctx, args[0U].get_sort())) { - r = Z3_mk_seq_concat(ctx, _args.size(), _args.ptr()); - } -- else if (Z3_is_re_sort(ctx, args[0].get_sort())) { -+ else if (Z3_is_re_sort(ctx, args[0U].get_sort())) { - r = Z3_mk_re_concat(ctx, _args.size(), _args.ptr()); - } - else { -@@ -2448,7 +2448,7 @@ namespace z3 { - inline expr mk_xor(expr_vector const& args) { - if (args.empty()) - return args.ctx().bool_val(false); -- expr r = args[0]; -+ expr r = args[0U]; - for (unsigned i = 1; i < args.size(); ++i) - r = r ^ args[i]; - return r; -@@ -2771,7 +2771,7 @@ namespace z3 { - assert(!m_end && !m_empty); - m_cube = m_solver.cube(m_vars, m_cutoff); - m_cutoff = 0xFFFFFFFF; -- if (m_cube.size() == 1 && m_cube[0].is_false()) { -+ if (m_cube.size() == 1 && m_cube[0U].is_false()) { - m_cube = z3::expr_vector(m_solver.ctx()); - m_end = true; - } -@@ -3804,7 +3804,7 @@ namespace z3 { - } - inline expr re_intersect(expr_vector const& args) { - assert(args.size() > 0); -- context& ctx = args[0].ctx(); -+ context& ctx = args[0U].ctx(); - array _args(args); - Z3_ast r = Z3_mk_re_intersect(ctx, _args.size(), _args.ptr()); - ctx.check_error(); diff --git a/z3.spec b/z3.spec index decc836..7286398 100644 --- a/z3.spec +++ b/z3.spec @@ -1,11 +1,13 @@ +# Do not embed bad package note paths in the OCaml files. %undefine _package_note_flags + # Tests are off by default because some of the tests require more memory than # the koji builders have available. %bcond_with test Name: z3 -Version: 4.8.15 -Release: 2%{?dist} +Version: 4.8.17 +Release: 1%{?dist} Summary: Satisfiability Modulo Theories (SMT) solver License: MIT @@ -13,9 +15,6 @@ URL: https://github.com/Z3Prover/z3 Source0: https://github.com/Z3Prover/z3/archive/%{name}-%{version}.tar.gz # Change the way python finds the shared object; see bz 1910923 Patch0: %{name}-python.patch -# Resolve ambiguous overloads that prevent cppcheck from building -# See https://github.com/Z3Prover/z3/issues/5922 -Patch1: %{name}-ambiguous-overload.patch BuildRequires: cmake BuildRequires: doxygen @@ -82,6 +81,7 @@ Ocaml interface to z3. %package -n ocaml-%{name}-devel Summary: Files for building ocaml applications that use z3 Requires: ocaml-%{name}%{?_isa} = %{version}-%{release} +Requires: ocaml-zarith-devel%{?_isa} %description -n ocaml-%{name}-devel Files for building ocaml applications that use z3. @@ -122,7 +122,6 @@ touch -r RELEASE_NOTES RELEASE_NOTES.utf8 mv -f RELEASE_NOTES.utf8 RELEASE_NOTES %build -export CXXFLAGS="%{build_cxxflags}" export LANG="C.UTF-8" export PYTHON="%{python3}" @@ -233,6 +232,10 @@ cd - %{python3_sitelib}/%{name}/ %changelog +* Mon May 16 2022 Jerry James - 4.8.17-1 +- Version 4.8.17 +- Drop upstreamed -ambiguous-overload patch + * Thu Mar 24 2022 Jerry James - 4.8.15-2 - Add -ambiguous-overload patch to fix cppcheck build failure From 6bc7033f70a24a49fdbdc5adf49a948e966c8a56 Mon Sep 17 00:00:00 2001 From: Python Maint Date: Mon, 13 Jun 2022 17:27:26 +0200 Subject: [PATCH 23/94] Rebuilt for Python 3.11 --- z3.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/z3.spec b/z3.spec index 7286398..637bb7b 100644 --- a/z3.spec +++ b/z3.spec @@ -7,7 +7,7 @@ Name: z3 Version: 4.8.17 -Release: 1%{?dist} +Release: 2%{?dist} Summary: Satisfiability Modulo Theories (SMT) solver License: MIT @@ -232,6 +232,9 @@ cd - %{python3_sitelib}/%{name}/ %changelog +* Mon Jun 13 2022 Python Maint - 4.8.17-2 +- Rebuilt for Python 3.11 + * Mon May 16 2022 Jerry James - 4.8.17-1 - Version 4.8.17 - Drop upstreamed -ambiguous-overload patch From c6dc115d0d10d0338f3e7e7ecf4654663c304697 Mon Sep 17 00:00:00 2001 From: "Richard W.M. Jones" Date: Sat, 18 Jun 2022 15:25:55 +0100 Subject: [PATCH 24/94] OCaml 4.14.0 rebuild --- z3.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/z3.spec b/z3.spec index 637bb7b..c2a8592 100644 --- a/z3.spec +++ b/z3.spec @@ -7,7 +7,7 @@ Name: z3 Version: 4.8.17 -Release: 2%{?dist} +Release: 3%{?dist} Summary: Satisfiability Modulo Theories (SMT) solver License: MIT @@ -232,6 +232,9 @@ cd - %{python3_sitelib}/%{name}/ %changelog +* Sat Jun 18 2022 Richard W.M. Jones - 4.8.17-3 +- OCaml 4.14.0 rebuild + * Mon Jun 13 2022 Python Maint - 4.8.17-2 - Rebuilt for Python 3.11 From d607dff55498dbee5e731ff975911f3e27895431 Mon Sep 17 00:00:00 2001 From: Python Maint Date: Mon, 20 Jun 2022 10:45:53 +0200 Subject: [PATCH 25/94] Rebuilt for Python 3.11 --- z3.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/z3.spec b/z3.spec index c2a8592..789968d 100644 --- a/z3.spec +++ b/z3.spec @@ -7,7 +7,7 @@ Name: z3 Version: 4.8.17 -Release: 3%{?dist} +Release: 4%{?dist} Summary: Satisfiability Modulo Theories (SMT) solver License: MIT @@ -232,6 +232,9 @@ cd - %{python3_sitelib}/%{name}/ %changelog +* Mon Jun 20 2022 Python Maint - 4.8.17-4 +- Rebuilt for Python 3.11 + * Sat Jun 18 2022 Richard W.M. Jones - 4.8.17-3 - OCaml 4.14.0 rebuild From 013801252ff50cecfbf1b8ed132d60c8fad25a7f Mon Sep 17 00:00:00 2001 From: Jerry James Date: Tue, 5 Jul 2022 13:23:31 -0600 Subject: [PATCH 26/94] Do not support Java on i686 (rhbz#2104112). Use new OCaml macros. --- z3.spec | 51 ++++++++++++++++++++++++++++++++++++--------------- 1 file changed, 36 insertions(+), 15 deletions(-) diff --git a/z3.spec b/z3.spec index 789968d..797888c 100644 --- a/z3.spec +++ b/z3.spec @@ -7,7 +7,7 @@ Name: z3 Version: 4.8.17 -Release: 4%{?dist} +Release: 5%{?dist} Summary: Satisfiability Modulo Theories (SMT) solver License: MIT @@ -22,8 +22,10 @@ BuildRequires: gcc-c++ BuildRequires: gmp-devel BuildRequires: graphviz BuildRequires: help2man +%ifarch %{java_arches} BuildRequires: java-devel BuildRequires: javapackages-tools +%endif BuildRequires: make BuildRequires: ninja-build BuildRequires: ocaml @@ -44,6 +46,11 @@ 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-%{name} < 4.8.17-5 +%endif + %description libs Library for applications that use z3 functionality. @@ -62,6 +69,7 @@ Summary: API documentation for Z3 %description doc API documentation for Z3. +%ifarch %{java_arches} %package -n java-%{name} Summary: Java interface to z3 Requires: %{name}-libs%{?_isa} = %{version}-%{release} @@ -70,6 +78,7 @@ Requires: javapackages-tools %description -n java-%{name} Java interface to z3. +%endif %package -n ocaml-%{name} Summary: Ocaml interface to z3 @@ -129,7 +138,11 @@ export PYTHON="%{python3}" -DCMAKE_INSTALL_INCLUDEDIR=%{_includedir}/%{name} \ -DCMAKE_JAVA_COMPILE_FLAGS="-source;1.8;-target;1.8" \ -DZ3_BUILD_DOCUMENTATION:BOOL=ON \ +%ifarch %{java_arches} -DZ3_BUILD_JAVA_BINDINGS:BOOL=ON \ +%else + -DZ3_BUILD_JAVA_BINDINGS:BOOL=OFF \ +%endif -DZ3_BUILD_PYTHON_BINDINGS:BOOL=ON \ -DZ3_INCLUDE_GIT_HASH:BOOL=OFF \ -DZ3_INCLUDE_GIT_DESCRIBE:BOOL=OFF \ @@ -160,19 +173,21 @@ export LANG="C.UTF-8" # Install the C++, python3, and Java interfaces %cmake_install +%ifarch %{java_arches} # Move the Java interface to its correct location mkdir -p %{buildroot}%{_libdir}/%{name} mkdir -p %{buildroot}%{_jnidir} mv %{buildroot}%{_javadir}/*.jar %{buildroot}%{_jnidir} ln -s %{_jnidir}/com.microsoft.z3.jar %{buildroot}%{_libdir}/%{name} mv %{buildroot}%{_libdir}/lib%{name}java.so %{buildroot}%{_libdir}/%{name} +%endif # Install the OCaml interface pushd build/api/ml -mkdir -p %{buildroot}%{_libdir}/ocaml/Z3 -cp -p META *.{a,cma,cmi,cmx,cmxa,cmxs,mli} %{buildroot}%{_libdir}/ocaml/Z3 -mkdir -p %{buildroot}%{_libdir}/ocaml/stublibs -cp -p *.so %{buildroot}%{_libdir}/ocaml/stublibs +mkdir -p %{buildroot}%{ocamldir}/Z3 +cp -p META *.{a,cma,cmi,cmx,cmxa,cmxs,mli} %{buildroot}%{ocamldir}/Z3 +mkdir -p %{buildroot}%{ocamldir}/stublibs +cp -p *.so %{buildroot}%{ocamldir}/stublibs popd # We handle the documentation files below @@ -210,28 +225,34 @@ cd - %doc %{_vpath_builddir}/doc/api/html examples %license LICENSE.txt +%ifarch %{java_arches} %files -n java-%{name} %{_libdir}/%{name}/ %{_jnidir}/com.microsoft.z3*jar +%endif %files -n ocaml-%{name} -%dir %{_libdir}/ocaml/Z3/ -%{_libdir}/ocaml/Z3/META -%{_libdir}/ocaml/Z3/*.cma -%{_libdir}/ocaml/Z3/*.cmi -%{_libdir}/ocaml/Z3/*.cmxs -%{_libdir}/ocaml/stublibs/*.so +%dir %{ocamldir}/Z3/ +%{ocamldir}/Z3/META +%{ocamldir}/Z3/*.cma +%{ocamldir}/Z3/*.cmi +%{ocamldir}/Z3/*.cmxs +%{ocamldir}/stublibs/*.so %files -n ocaml-%{name}-devel -%{_libdir}/ocaml/Z3/*.a -%{_libdir}/ocaml/Z3/*.cmx -%{_libdir}/ocaml/Z3/*.cmxa -%{_libdir}/ocaml/Z3/*.mli +%{ocamldir}/Z3/*.a +%{ocamldir}/Z3/*.cmx +%{ocamldir}/Z3/*.cmxa +%{ocamldir}/Z3/*.mli %files -n python3-%{name} %{python3_sitelib}/%{name}/ %changelog +* Tue Jun 28 2022 Jerry James - 4.8.17-5 +- Do not support Java on i686 (rhbz#2104112) +- Use new OCaml macros + * Mon Jun 20 2022 Python Maint - 4.8.17-4 - Rebuilt for Python 3.11 From 700febff68c0c7b1d1d96e9bb008a442f071c6ff Mon Sep 17 00:00:00 2001 From: Fedora Release Engineering Date: Sat, 23 Jul 2022 13:49:24 +0000 Subject: [PATCH 27/94] Rebuilt for https://fedoraproject.org/wiki/Fedora_37_Mass_Rebuild Signed-off-by: Fedora Release Engineering --- z3.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/z3.spec b/z3.spec index 797888c..549023d 100644 --- a/z3.spec +++ b/z3.spec @@ -7,7 +7,7 @@ Name: z3 Version: 4.8.17 -Release: 5%{?dist} +Release: 6%{?dist} Summary: Satisfiability Modulo Theories (SMT) solver License: MIT @@ -249,6 +249,9 @@ cd - %{python3_sitelib}/%{name}/ %changelog +* Sat Jul 23 2022 Fedora Release Engineering - 4.8.17-6 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_37_Mass_Rebuild + * Tue Jun 28 2022 Jerry James - 4.8.17-5 - Do not support Java on i686 (rhbz#2104112) - Use new OCaml macros From 52e2a85d5e58be04a18f9cbdcd0a636aabe0f429 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Mon, 8 Aug 2022 06:33:35 -0600 Subject: [PATCH 28/94] Version 4.10.2. --- sources | 2 +- z3.spec | 93 ++++++++++++++++++++++++++++++--------------------------- 2 files changed, 50 insertions(+), 45 deletions(-) diff --git a/sources b/sources index 957cc32..11e3338 100644 --- a/sources +++ b/sources @@ -1 +1 @@ -SHA512 (z3-4.8.17.tar.gz) = 95517014ec1798c2552253dd5cde6f955896ab297a4f56294f4bc6f2c5428069015f513c6eb9a090a809cfcf4cb1cc38cc83818f19b5b1051e4e6c06f973747d +SHA512 (z3-4.10.2.tar.gz) = d0e54036d403d124a7bbf4cf8de9fd9159bab5151f875b546474563811dfb259bc46650df950802031a180375745fb589acbc79d0065944f0631df378dd6d0c3 diff --git a/z3.spec b/z3.spec index 549023d..d4fe24b 100644 --- a/z3.spec +++ b/z3.spec @@ -1,3 +1,12 @@ +# TODO: A Julia interface is now available, but requires +# https://github.com/JuliaInterop/libcxxwrap-julia, which is not currently +# available in Fedora. + +# TODO: A JavaScript interface is now available. Given the generally poor +# state of JavaScript in Fedora, I do not plan to add a subpackage for it +# unless somebody is really, really persuasive and available to help fix it +# if it breaks. + # Do not embed bad package note paths in the OCaml files. %undefine _package_note_flags @@ -6,8 +15,8 @@ %bcond_with test Name: z3 -Version: 4.8.17 -Release: 6%{?dist} +Version: 4.10.2 +Release: 1%{?dist} Summary: Satisfiability Modulo Theories (SMT) solver License: MIT @@ -48,7 +57,7 @@ Summary: Library for applications that use z3 functionality # This can be removed when F40 reaches EOL %ifnarch %{java_arches} -Obsoletes: java-%{name} < 4.8.17-5 +Obsoletes: java-z3 < 4.8.17-5 %endif %description libs @@ -56,7 +65,7 @@ Library for applications that use z3 functionality. %package devel Summary: Header files for build applications that use z3 -Requires: %{name}-libs%{?_isa} = %{version}-%{release} +Requires: z3-libs%{?_isa} = %{version}-%{release} %description devel Header files for build applications that use z3. @@ -70,37 +79,37 @@ Summary: API documentation for Z3 API documentation for Z3. %ifarch %{java_arches} -%package -n java-%{name} +%package -n java-z3 Summary: Java interface to z3 -Requires: %{name}-libs%{?_isa} = %{version}-%{release} +Requires: z3-libs%{?_isa} = %{version}-%{release} Requires: java Requires: javapackages-tools -%description -n java-%{name} +%description -n java-z3 Java interface to z3. %endif -%package -n ocaml-%{name} +%package -n ocaml-z3 Summary: Ocaml interface to z3 -Requires: %{name}-libs%{?_isa} = %{version}-%{release} +Requires: z3-libs%{?_isa} = %{version}-%{release} -%description -n ocaml-%{name} +%description -n ocaml-z3 Ocaml interface to z3. -%package -n ocaml-%{name}-devel +%package -n ocaml-z3-devel Summary: Files for building ocaml applications that use z3 -Requires: ocaml-%{name}%{?_isa} = %{version}-%{release} +Requires: ocaml-z3%{?_isa} = %{version}-%{release} Requires: ocaml-zarith-devel%{?_isa} -%description -n ocaml-%{name}-devel +%description -n ocaml-z3-devel Files for building ocaml applications that use z3. -%package -n python3-%{name} +%package -n python3-z3 Summary: Python 3 interface to z3 BuildArch: noarch -Requires: %{name}-libs = %{version}-%{release} +Requires: z3-libs = %{version}-%{release} -%description -n python3-%{name} +%description -n python3-z3 Python 3 interface to z3. %prep @@ -113,8 +122,8 @@ sed \ -e 's/@$(CXX)/$(CXX)/' \ -e '/O3/d' \ -e "s/\(['\"]\)cp\([^[:alnum:]]\)/\1cp -p\2/" \ - -e "s/\(SLIBEXTRAFLAGS = '\)'/\1-Wl,--no-whole-archive -Wl,--as-needed'/" \ - -e "/SLIBFLAGS/s|-shared|& %{build_ldflags} -Wl,--whole-archive|" \ + -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/OCAML_FLAGS = ''/OCAML_FLAGS = '-g'/" \ -i scripts/mk_util.py @@ -125,23 +134,16 @@ sed -e '/libz3java/s,\(System\.load\)Library("\(.*\)"),\1("%{_libdir}/z3/\2.so") -e "s/@MAJVER@/$majver/" \ -i scripts/update_api.py -# Fix character encoding -iconv -f iso8859-1 -t utf-8 RELEASE_NOTES > RELEASE_NOTES.utf8 -touch -r RELEASE_NOTES RELEASE_NOTES.utf8 -mv -f RELEASE_NOTES.utf8 RELEASE_NOTES - %build export LANG="C.UTF-8" export PYTHON="%{python3}" %cmake -G Ninja \ - -DCMAKE_INSTALL_INCLUDEDIR=%{_includedir}/%{name} \ + -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 \ -%else - -DZ3_BUILD_JAVA_BINDINGS:BOOL=OFF \ %endif -DZ3_BUILD_PYTHON_BINDINGS:BOOL=ON \ -DZ3_INCLUDE_GIT_HASH:BOOL=OFF \ @@ -175,11 +177,11 @@ export LANG="C.UTF-8" %ifarch %{java_arches} # Move the Java interface to its correct location -mkdir -p %{buildroot}%{_libdir}/%{name} +mkdir -p %{buildroot}%{_libdir}/z3 mkdir -p %{buildroot}%{_jnidir} mv %{buildroot}%{_javadir}/*.jar %{buildroot}%{_jnidir} -ln -s %{_jnidir}/com.microsoft.z3.jar %{buildroot}%{_libdir}/%{name} -mv %{buildroot}%{_libdir}/lib%{name}java.so %{buildroot}%{_libdir}/%{name} +ln -s %{_jnidir}/com.microsoft.z3.jar %{buildroot}%{_libdir}/z3 +mv %{buildroot}%{_libdir}/libz3java.so %{buildroot}%{_libdir}/z3 %endif # Install the OCaml interface @@ -195,7 +197,7 @@ rm -rf %{buildroot}%{_docdir}/Z3 # Make a man page mkdir -p %{buildroot}%{_mandir}/man1 -help2man -N -o %{buildroot}%{_mandir}/man1/%{name}.1 %{_vpath_builddir}/%{name} +help2man -N -o %{buildroot}%{_mandir}/man1/z3.1 %{_vpath_builddir}/z3 %if %{with test} %check @@ -207,31 +209,31 @@ cd - %endif %files -%doc README.md RELEASE_NOTES -%{_bindir}/%{name} -%{_mandir}/man1/%{name}.1* +%doc README.md RELEASE_NOTES.md +%{_bindir}/z3 +%{_mandir}/man1/z3.1* %files libs %license LICENSE.txt -%{_libdir}/lib%{name}.so.4* +%{_libdir}/libz3.so.4.10* %files devel -%{_includedir}/%{name}/ -%{_libdir}/lib%{name}.so -%{_libdir}/cmake/%{name}/ -%{_libdir}/pkgconfig/%{name}.pc +%{_includedir}/z3/ +%{_libdir}/libz3.so +%{_libdir}/cmake/z3/ +%{_libdir}/pkgconfig/z3.pc %files doc %doc %{_vpath_builddir}/doc/api/html examples %license LICENSE.txt %ifarch %{java_arches} -%files -n java-%{name} -%{_libdir}/%{name}/ +%files -n java-z3 +%{_libdir}/z3/ %{_jnidir}/com.microsoft.z3*jar %endif -%files -n ocaml-%{name} +%files -n ocaml-z3 %dir %{ocamldir}/Z3/ %{ocamldir}/Z3/META %{ocamldir}/Z3/*.cma @@ -239,16 +241,19 @@ cd - %{ocamldir}/Z3/*.cmxs %{ocamldir}/stublibs/*.so -%files -n ocaml-%{name}-devel +%files -n ocaml-z3-devel %{ocamldir}/Z3/*.a %{ocamldir}/Z3/*.cmx %{ocamldir}/Z3/*.cmxa %{ocamldir}/Z3/*.mli -%files -n python3-%{name} -%{python3_sitelib}/%{name}/ +%files -n python3-z3 +%{python3_sitelib}/z3/ %changelog +* Mon Aug 8 2022 Jerry James - 4.10.2-1 +- Version 4.10.2 + * Sat Jul 23 2022 Fedora Release Engineering - 4.8.17-6 - Rebuilt for https://fedoraproject.org/wiki/Fedora_37_Mass_Rebuild From 1b84535f23b240227403533f360500023ef67b81 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Fri, 19 Aug 2022 13:32:07 -0600 Subject: [PATCH 29/94] Version 4.11.0. Clarify license of the doc subpackage. --- sources | 2 +- z3.spec | 12 ++++++++++-- 2 files changed, 11 insertions(+), 3 deletions(-) diff --git a/sources b/sources index 11e3338..b7e20d2 100644 --- a/sources +++ b/sources @@ -1 +1 @@ -SHA512 (z3-4.10.2.tar.gz) = d0e54036d403d124a7bbf4cf8de9fd9159bab5151f875b546474563811dfb259bc46650df950802031a180375745fb589acbc79d0065944f0631df378dd6d0c3 +SHA512 (z3-4.11.0.tar.gz) = a3fd7e013948de6683b16aca03641bb845d02187152bebdee8c62c2a3f80a7710a1d3b9aef9c1490c2340571bb225f457928ac57a2ed28c0084ced34bcf3e905 diff --git a/z3.spec b/z3.spec index d4fe24b..a538c8e 100644 --- a/z3.spec +++ b/z3.spec @@ -15,7 +15,7 @@ %bcond_with test Name: z3 -Version: 4.10.2 +Version: 4.11.0 Release: 1%{?dist} Summary: Satisfiability Modulo Theories (SMT) solver @@ -72,6 +72,10 @@ Header files for build applications that use z3. %package doc Summary: API documentation for Z3 +# Two files in examples are GPL-3.0-or-later WITH Bison-exception 2.2: +# examples/tptp/tptp5.tab.c +# examples/tptp/tptp5.tab.c +License: MIT AND GPL-3.0-or-later WITH Bison-exception-2.2 # FIXME: this should be noarch, but we end up with different numbers of inheritance # graphs on different architectures. Why? @@ -215,7 +219,7 @@ cd - %files libs %license LICENSE.txt -%{_libdir}/libz3.so.4.10* +%{_libdir}/libz3.so.4.11* %files devel %{_includedir}/z3/ @@ -251,6 +255,10 @@ cd - %{python3_sitelib}/z3/ %changelog +* Fri Aug 19 2022 Jerry James - 4.11.0-1 +- Version 4.11.0 +- Clarify license of the doc subpackage + * Mon Aug 8 2022 Jerry James - 4.10.2-1 - Version 4.10.2 From 6bc865dcfc1d0b137862b9f8d8443d640800de38 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Sun, 4 Sep 2022 13:17:38 -0600 Subject: [PATCH 30/94] Version 4.11.2. --- sources | 2 +- z3.spec | 5 ++++- 2 files changed, 5 insertions(+), 2 deletions(-) diff --git a/sources b/sources index b7e20d2..8afe937 100644 --- a/sources +++ b/sources @@ -1 +1 @@ -SHA512 (z3-4.11.0.tar.gz) = a3fd7e013948de6683b16aca03641bb845d02187152bebdee8c62c2a3f80a7710a1d3b9aef9c1490c2340571bb225f457928ac57a2ed28c0084ced34bcf3e905 +SHA512 (z3-4.11.2.tar.gz) = be2573d38c0e50b46fcb025d50335e016769fdeab3c26f5dc2a13102fae889d23039258ea8d38de3f53daa4cf073704d8639ac291e781a74633194adedaae21a diff --git a/z3.spec b/z3.spec index a538c8e..f7171af 100644 --- a/z3.spec +++ b/z3.spec @@ -15,7 +15,7 @@ %bcond_with test Name: z3 -Version: 4.11.0 +Version: 4.11.2 Release: 1%{?dist} Summary: Satisfiability Modulo Theories (SMT) solver @@ -255,6 +255,9 @@ cd - %{python3_sitelib}/z3/ %changelog +* Sun Sep 4 2022 Jerry James - 4.11.2-1 +- Version 4.11.2 + * Fri Aug 19 2022 Jerry James - 4.11.0-1 - Version 4.11.0 - Clarify license of the doc subpackage From 6264c50021f5f714d493601b6ca5917bf271b091 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Wed, 14 Dec 2022 16:15:48 -0700 Subject: [PATCH 31/94] Further clarify license of the doc subpackage (SPDX). --- z3.spec | 36 ++++++++++++++++++++++++++++++++++-- 1 file changed, 34 insertions(+), 2 deletions(-) diff --git a/z3.spec b/z3.spec index f7171af..1803e4a 100644 --- a/z3.spec +++ b/z3.spec @@ -71,11 +71,40 @@ Requires: z3-libs%{?_isa} = %{version}-%{release} Header files for build applications that use z3. %package doc -Summary: API documentation for Z3 +# The content is MIT. # Two files in examples are GPL-3.0-or-later WITH Bison-exception 2.2: # examples/tptp/tptp5.tab.c # examples/tptp/tptp5.tab.c -License: MIT AND GPL-3.0-or-later WITH Bison-exception-2.2 +# 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/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/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? @@ -255,6 +284,9 @@ cd - %{python3_sitelib}/z3/ %changelog +* Wed Dec 14 2022 Jerry James - 4.11.2-1 +- Further clarify license of the doc subpackage (SPDX) + * Sun Sep 4 2022 Jerry James - 4.11.2-1 - Version 4.11.2 From aca6b5306f4f5479147e06742d1a853fe260ed8d Mon Sep 17 00:00:00 2001 From: Jerry James Date: Sun, 8 Jan 2023 21:56:34 -0700 Subject: [PATCH 32/94] Add -data-race patch to fix segfault (bz 2157972). Add -uninit patch to fix use of an uninitialized value. --- z3-data-race.patch | 10 ++++++++++ z3-uninit.patch | 10 ++++++++++ z3.spec | 14 +++++++++++--- 3 files changed, 31 insertions(+), 3 deletions(-) create mode 100644 z3-data-race.patch create mode 100644 z3-uninit.patch diff --git a/z3-data-race.patch b/z3-data-race.patch new file mode 100644 index 0000000..547b48c --- /dev/null +++ b/z3-data-race.patch @@ -0,0 +1,10 @@ +--- z3-z3-4.11.2/src/solver/parallel_tactic.cpp.orig 2022-09-03 16:47:12.000000000 -0600 ++++ z3-z3-4.11.2/src/solver/parallel_tactic.cpp 2023-01-08 21:39:29.169670155 -0700 +@@ -460,6 +460,7 @@ private: + conquer->get_model(mdl); + } + else { ++ std::lock_guard lock(m_mutex); + s.get_solver().get_model(mdl); + } + if (mdl) { diff --git a/z3-uninit.patch b/z3-uninit.patch new file mode 100644 index 0000000..fc3623c --- /dev/null +++ b/z3-uninit.patch @@ -0,0 +1,10 @@ +--- z3-z3-4.11.2/src/sat/sat_lookahead.cpp.orig 2022-09-03 16:47:12.000000000 -0600 ++++ z3-z3-4.11.2/src/sat/sat_lookahead.cpp 2023-01-06 15:09:19.198322817 -0700 +@@ -1001,6 +1001,7 @@ namespace sat { + m_inconsistent = false; + m_qhead = 0; + m_bstamp_id = 0; ++ m_istamp_id = 0; + + for (unsigned i = 0; i < m_num_vars; ++i) { + init_var(i); diff --git a/z3.spec b/z3.spec index 1803e4a..9328599 100644 --- a/z3.spec +++ b/z3.spec @@ -16,7 +16,7 @@ Name: z3 Version: 4.11.2 -Release: 1%{?dist} +Release: 2%{?dist} Summary: Satisfiability Modulo Theories (SMT) solver License: MIT @@ -24,6 +24,10 @@ URL: https://github.com/Z3Prover/z3 Source0: https://github.com/Z3Prover/z3/archive/%{name}-%{version}.tar.gz # Change the way python finds the shared object; see bz 1910923 Patch0: %{name}-python.patch +# Fix use of an uninitialized variable +Patch1: %{name}-uninit.patch +# Fix a data race that can cause a segfault; see bz 2157972 +Patch2: %{name}-data-race.patch BuildRequires: cmake BuildRequires: doxygen @@ -168,8 +172,8 @@ sed -e '/libz3java/s,\(System\.load\)Library("\(.*\)"),\1("%{_libdir}/z3/\2.so") -i scripts/update_api.py %build -export LANG="C.UTF-8" -export PYTHON="%{python3}" +export LANG=C.UTF-8 +export PYTHON=%{python3} %cmake -G Ninja \ -DCMAKE_INSTALL_INCLUDEDIR=%{_includedir}/z3 \ @@ -284,6 +288,10 @@ cd - %{python3_sitelib}/z3/ %changelog +* Sun Jan 8 2023 Jerry James - 4.11.2-2 +- Add -data-race patch to fix segfault (bz 2157972) +- Add -uninit patch to fix use of an uninitialized value + * Wed Dec 14 2022 Jerry James - 4.11.2-1 - Further clarify license of the doc subpackage (SPDX) From 70124da6df0e07d9fd2351e4a27d5438a3ef834a Mon Sep 17 00:00:00 2001 From: Jerry James Date: Tue, 17 Jan 2023 15:01:03 -0700 Subject: [PATCH 33/94] Version 4.12.0. Drop upstreamed -data-race and -uninit patches. --- sources | 2 +- z3-data-race.patch | 10 ---------- z3-uninit.patch | 10 ---------- z3.spec | 20 +++++++++++++------- 4 files changed, 14 insertions(+), 28 deletions(-) delete mode 100644 z3-data-race.patch delete mode 100644 z3-uninit.patch diff --git a/sources b/sources index 8afe937..e96d62e 100644 --- a/sources +++ b/sources @@ -1 +1 @@ -SHA512 (z3-4.11.2.tar.gz) = be2573d38c0e50b46fcb025d50335e016769fdeab3c26f5dc2a13102fae889d23039258ea8d38de3f53daa4cf073704d8639ac291e781a74633194adedaae21a +SHA512 (z3-4.12.0.tar.gz) = 53a51c8304fa4356d13293f68b14d9d9eef57a0771c6698d38aea5fac62c4e52c41ff003cb6d771a32645d2aa4ef59be5f792f2efbee927d06ac8280094976e5 diff --git a/z3-data-race.patch b/z3-data-race.patch deleted file mode 100644 index 547b48c..0000000 --- a/z3-data-race.patch +++ /dev/null @@ -1,10 +0,0 @@ ---- z3-z3-4.11.2/src/solver/parallel_tactic.cpp.orig 2022-09-03 16:47:12.000000000 -0600 -+++ z3-z3-4.11.2/src/solver/parallel_tactic.cpp 2023-01-08 21:39:29.169670155 -0700 -@@ -460,6 +460,7 @@ private: - conquer->get_model(mdl); - } - else { -+ std::lock_guard lock(m_mutex); - s.get_solver().get_model(mdl); - } - if (mdl) { diff --git a/z3-uninit.patch b/z3-uninit.patch deleted file mode 100644 index fc3623c..0000000 --- a/z3-uninit.patch +++ /dev/null @@ -1,10 +0,0 @@ ---- z3-z3-4.11.2/src/sat/sat_lookahead.cpp.orig 2022-09-03 16:47:12.000000000 -0600 -+++ z3-z3-4.11.2/src/sat/sat_lookahead.cpp 2023-01-06 15:09:19.198322817 -0700 -@@ -1001,6 +1001,7 @@ namespace sat { - m_inconsistent = false; - m_qhead = 0; - m_bstamp_id = 0; -+ m_istamp_id = 0; - - for (unsigned i = 0; i < m_num_vars; ++i) { - init_var(i); diff --git a/z3.spec b/z3.spec index 9328599..67526af 100644 --- a/z3.spec +++ b/z3.spec @@ -15,8 +15,8 @@ %bcond_with test Name: z3 -Version: 4.11.2 -Release: 2%{?dist} +Version: 4.12.0 +Release: 1%{?dist} Summary: Satisfiability Modulo Theories (SMT) solver License: MIT @@ -24,10 +24,6 @@ URL: https://github.com/Z3Prover/z3 Source0: https://github.com/Z3Prover/z3/archive/%{name}-%{version}.tar.gz # Change the way python finds the shared object; see bz 1910923 Patch0: %{name}-python.patch -# Fix use of an uninitialized variable -Patch1: %{name}-uninit.patch -# Fix a data race that can cause a segfault; see bz 2157972 -Patch2: %{name}-data-race.patch BuildRequires: cmake BuildRequires: doxygen @@ -171,6 +167,9 @@ sed -e '/libz3java/s,\(System\.load\)Library("\(.*\)"),\1("%{_libdir}/z3/\2.so") -e "s/@MAJVER@/$majver/" \ -i scripts/update_api.py +# Turn off HTML timestamps for reproducible builds +sed -i '/HTML_TIMESTAMP/s/YES/NO/' doc/z3api.cfg.in doc/z3code.dox + %build export LANG=C.UTF-8 export PYTHON=%{python3} @@ -236,6 +235,9 @@ rm -rf %{buildroot}%{_docdir}/Z3 mkdir -p %{buildroot}%{_mandir}/man1 help2man -N -o %{buildroot}%{_mandir}/man1/z3.1 %{_vpath_builddir}/z3 +# Fix the pkgconfig file +sed -i 's,//usr,,' %{buildroot}%{_libdir}/pkgconfig/z3.pc + %if %{with test} %check export LANG="C.UTF-8" @@ -252,7 +254,7 @@ cd - %files libs %license LICENSE.txt -%{_libdir}/libz3.so.4.11* +%{_libdir}/libz3.so.4.12* %files devel %{_includedir}/z3/ @@ -288,6 +290,10 @@ cd - %{python3_sitelib}/z3/ %changelog +* Tue Jan 17 2023 Jerry James - 4.12.0-1 +- Version 4.12.0 +- Drop upstreamed -data-race and -uninit patches + * Sun Jan 8 2023 Jerry James - 4.11.2-2 - Add -data-race patch to fix segfault (bz 2157972) - Add -uninit patch to fix use of an uninitialized value From fed39e8c56f422919bc2670e91e3a7066ca89c68 Mon Sep 17 00:00:00 2001 From: Fedora Release Engineering Date: Sat, 21 Jan 2023 08:09:46 +0000 Subject: [PATCH 34/94] Rebuilt for https://fedoraproject.org/wiki/Fedora_38_Mass_Rebuild Signed-off-by: Fedora Release Engineering --- z3.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/z3.spec b/z3.spec index 67526af..49c5fb7 100644 --- a/z3.spec +++ b/z3.spec @@ -16,7 +16,7 @@ Name: z3 Version: 4.12.0 -Release: 1%{?dist} +Release: 2%{?dist} Summary: Satisfiability Modulo Theories (SMT) solver License: MIT @@ -290,6 +290,9 @@ cd - %{python3_sitelib}/z3/ %changelog +* Sat Jan 21 2023 Fedora Release Engineering - 4.12.0-2 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_38_Mass_Rebuild + * Tue Jan 17 2023 Jerry James - 4.12.0-1 - Version 4.12.0 - Drop upstreamed -data-race and -uninit patches From 42e82b1a863a9e0583c251f830260ce07c0db156 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Sat, 21 Jan 2023 10:25:11 -0700 Subject: [PATCH 35/94] Version 4.12.1. --- sources | 2 +- z3.spec | 7 +++++-- 2 files changed, 6 insertions(+), 3 deletions(-) diff --git a/sources b/sources index e96d62e..50bef42 100644 --- a/sources +++ b/sources @@ -1 +1 @@ -SHA512 (z3-4.12.0.tar.gz) = 53a51c8304fa4356d13293f68b14d9d9eef57a0771c6698d38aea5fac62c4e52c41ff003cb6d771a32645d2aa4ef59be5f792f2efbee927d06ac8280094976e5 +SHA512 (z3-4.12.1.tar.gz) = 031fba9cc000a8da0025f95fa3f1c7519071d1b7775b377ff3192c505bb4c7e3d267da246c9ae68c940224e055a3c30571d2c0d7fbb042ec9a3d5849543a385c diff --git a/z3.spec b/z3.spec index 49c5fb7..d2354cf 100644 --- a/z3.spec +++ b/z3.spec @@ -15,8 +15,8 @@ %bcond_with test Name: z3 -Version: 4.12.0 -Release: 2%{?dist} +Version: 4.12.1 +Release: 1%{?dist} Summary: Satisfiability Modulo Theories (SMT) solver License: MIT @@ -290,6 +290,9 @@ cd - %{python3_sitelib}/z3/ %changelog +* Sat Jan 21 2023 Jerry James - 4.12.1-1 +- Version 4.12.1 + * Sat Jan 21 2023 Fedora Release Engineering - 4.12.0-2 - Rebuilt for https://fedoraproject.org/wiki/Fedora_38_Mass_Rebuild From 0c0af7bf22da085cd6466301cc4c58ddaabe0a40 Mon Sep 17 00:00:00 2001 From: "Richard W.M. Jones" Date: Tue, 24 Jan 2023 09:20:14 +0000 Subject: [PATCH 36/94] Rebuild OCaml packages for F38 --- z3.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/z3.spec b/z3.spec index d2354cf..4ae68d9 100644 --- a/z3.spec +++ b/z3.spec @@ -16,7 +16,7 @@ Name: z3 Version: 4.12.1 -Release: 1%{?dist} +Release: 2%{?dist} Summary: Satisfiability Modulo Theories (SMT) solver License: MIT @@ -290,6 +290,9 @@ cd - %{python3_sitelib}/z3/ %changelog +* Tue Jan 24 2023 Richard W.M. Jones - 4.12.1-2 +- Rebuild OCaml packages for F38 + * Sat Jan 21 2023 Jerry James - 4.12.1-1 - Version 4.12.1 From ee66c97a959698e817bac965fe3b1f009f2ac0f8 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Mon, 15 May 2023 08:44:33 -0600 Subject: [PATCH 37/94] Version 4.12.2 --- sources | 2 +- z3-stdint.patch | 25 +++++++++++++++++++++++++ z3.spec | 10 ++++++++-- 3 files changed, 34 insertions(+), 3 deletions(-) create mode 100644 z3-stdint.patch diff --git a/sources b/sources index 50bef42..3d592ee 100644 --- a/sources +++ b/sources @@ -1 +1 @@ -SHA512 (z3-4.12.1.tar.gz) = 031fba9cc000a8da0025f95fa3f1c7519071d1b7775b377ff3192c505bb4c7e3d267da246c9ae68c940224e055a3c30571d2c0d7fbb042ec9a3d5849543a385c +SHA512 (z3-4.12.2.tar.gz) = 375477cbbc9837b44e752c89916409d07bf6a73830b52878aab4f376f08b37dd5ab485da225744d394ab15f2a7e1014edc3be5eb9962934c440a8d55259317e2 diff --git a/z3-stdint.patch b/z3-stdint.patch new file mode 100644 index 0000000..c0874f2 --- /dev/null +++ b/z3-stdint.patch @@ -0,0 +1,25 @@ +Fixes errors such as these: + +In file included from /builddir/build/BUILD/z3-z3-4.12.2/src/util/region.cpp:53: +/builddir/build/BUILD/z3-z3-4.12.2/src/util/region.cpp: In member function ‘void* region::allocate(size_t)’: +/builddir/build/BUILD/z3-z3-4.12.2/src/util/tptr.h:29:62: error: ‘uintptr_t’ does not name a type + 29 | #define ALIGN(T, PTR) reinterpret_cast(((reinterpret_cast(PTR) >> PTR_ALIGNMENT) + \ + | ^~~~~~~~~ +/builddir/build/BUILD/z3-z3-4.12.2/src/util/region.cpp:82:22: note: in expansion of macro ‘ALIGN’ + 82 | m_curr_ptr = ALIGN(char *, new_curr_ptr); + | ^~~~~ +/builddir/build/BUILD/z3-z3-4.12.2/src/util/region.cpp:57:1: note: ‘uintptr_t’ is defined in header ‘’; did you forget to ‘#include ’? + 56 | #include "util/page.h" + +++ |+#include + 57 | + +--- z3-z3-4.12.2/src/util/tptr.h.orig 2023-05-12 13:59:04.000000000 -0600 ++++ z3-z3-4.12.2/src/util/tptr.h 2023-05-13 07:04:48.389716628 -0600 +@@ -19,6 +19,7 @@ Revision History: + + #pragma once + ++#include + #include "util/machine.h" + + #define TAG_SHIFT PTR_ALIGNMENT diff --git a/z3.spec b/z3.spec index 4ae68d9..2f1e838 100644 --- a/z3.spec +++ b/z3.spec @@ -15,8 +15,8 @@ %bcond_with test Name: z3 -Version: 4.12.1 -Release: 2%{?dist} +Version: 4.12.2 +Release: 1%{?dist} Summary: Satisfiability Modulo Theories (SMT) solver License: MIT @@ -24,6 +24,9 @@ URL: https://github.com/Z3Prover/z3 Source0: https://github.com/Z3Prover/z3/archive/%{name}-%{version}.tar.gz # Change the way python finds the shared object; see bz 1910923 Patch0: %{name}-python.patch +# Add a missing include of cstdint +# https://github.com/Z3Prover/z3/pull/6720 +Patch1: %{name}-stdint.patch BuildRequires: cmake BuildRequires: doxygen @@ -290,6 +293,9 @@ cd - %{python3_sitelib}/z3/ %changelog +* Mon May 15 2023 Jerry James - 4.12.2-1 +- Version 4.12.2 + * Tue Jan 24 2023 Richard W.M. Jones - 4.12.1-2 - Rebuild OCaml packages for F38 From 647df7bf04ca3c564bcd8c899637e1f3f5db50f1 Mon Sep 17 00:00:00 2001 From: Python Maint Date: Thu, 15 Jun 2023 14:41:58 +0200 Subject: [PATCH 38/94] Rebuilt for Python 3.12 --- z3.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/z3.spec b/z3.spec index 2f1e838..1df2e55 100644 --- a/z3.spec +++ b/z3.spec @@ -16,7 +16,7 @@ Name: z3 Version: 4.12.2 -Release: 1%{?dist} +Release: 2%{?dist} Summary: Satisfiability Modulo Theories (SMT) solver License: MIT @@ -293,6 +293,9 @@ cd - %{python3_sitelib}/z3/ %changelog +* Thu Jun 15 2023 Python Maint - 4.12.2-2 +- Rebuilt for Python 3.12 + * Mon May 15 2023 Jerry James - 4.12.2-1 - Version 4.12.2 From 67bb880db86e57f4c036c33946d759dc801a403d Mon Sep 17 00:00:00 2001 From: Jerry James Date: Wed, 21 Jun 2023 13:39:46 -0600 Subject: [PATCH 39/94] Rebuild for OCaml 5.0 --- z3.spec | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/z3.spec b/z3.spec index 1df2e55..ca3ac91 100644 --- a/z3.spec +++ b/z3.spec @@ -7,16 +7,13 @@ # unless somebody is really, really persuasive and available to help fix it # if it breaks. -# Do not embed bad package note paths in the OCaml files. -%undefine _package_note_flags - # Tests are off by default because some of the tests require more memory than # the koji builders have available. %bcond_with test Name: z3 Version: 4.12.2 -Release: 2%{?dist} +Release: 3%{?dist} Summary: Satisfiability Modulo Theories (SMT) solver License: MIT @@ -293,6 +290,9 @@ cd - %{python3_sitelib}/z3/ %changelog +* Wed Jun 21 2023 Jerry James - 4.12.2-3 +- Rebuild for OCaml 5.0 + * Thu Jun 15 2023 Python Maint - 4.12.2-2 - Rebuilt for Python 3.12 From b4c9000b463a090b40ccb4112e2928fe1bb24141 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Mon, 10 Jul 2023 16:55:13 -0600 Subject: [PATCH 40/94] OCaml 5.0.0 rebuild --- z3-escapes.patch | 205 +++++++++++++++++++++++++++++++++++++++++++++++ z3-ocaml.patch | 56 +++++++++++++ z3.spec | 32 ++++++-- 3 files changed, 285 insertions(+), 8 deletions(-) create mode 100644 z3-escapes.patch create mode 100644 z3-ocaml.patch diff --git a/z3-escapes.patch b/z3-escapes.patch new file mode 100644 index 0000000..8d1e0c7 --- /dev/null +++ b/z3-escapes.patch @@ -0,0 +1,205 @@ +Fixes warnings such as these: + +/builddir/build/BUILD/z3-z3-4.12.2/scripts/mk_genfile_common.py:142: SyntaxWarning: invalid escape sequence '\-' + words = re.split('[^\-a-zA-Z0-9_]+', line) +/builddir/build/BUILD/z3-z3-4.12.2/scripts/mk_genfile_common.py:577: SyntaxWarning: invalid escape sequence '\W' + words = re.split('\W+', line) + +--- z3-z3-4.12.2/scripts/mk_genfile_common.py.orig 2023-05-12 13:59:04.000000000 -0600 ++++ z3-z3-4.12.2/scripts/mk_genfile_common.py 2023-07-06 10:52:08.477210179 -0600 +@@ -139,7 +139,7 @@ def mk_z3consts_py_internal(api_files, o + assert False, "Invalid %s, line: %s" % (api_file, linenum) + else: + assert mode == IN_ENUM +- words = re.split('[^\-a-zA-Z0-9_]+', line) ++ words = re.split('[^-a-zA-Z0-9_]+', line) + m = closebrace_pat.match(line) + if m: + name = words[1] +@@ -227,7 +227,7 @@ def mk_z3consts_dotnet_internal(api_file + assert False, "Invalid %s, line: %s" % (api_file, linenum) + else: + assert mode == IN_ENUM +- words = re.split('[^\-a-zA-Z0-9_]+', line) ++ words = re.split('[^-a-zA-Z0-9_]+', line) + m = closebrace_pat.match(line) + if m: + name = words[1] +@@ -315,7 +315,7 @@ def mk_z3consts_java_internal(api_files, + assert False, "Invalid %s, line: %s" % (api_file, linenum) + else: + assert mode == IN_ENUM +- words = re.split('[^\-a-zA-Z0-9_]+', line) ++ words = re.split('[^-a-zA-Z0-9_]+', line) + m = closebrace_pat.match(line) + if m: + name = words[1] +@@ -441,7 +441,7 @@ def mk_z3consts_ml_internal(api_files, o + assert False, "Invalid %s, line: %s" % (api_file, linenum) + else: + assert mode == IN_ENUM +- words = re.split('[^\-a-zA-Z0-9_]+', line) ++ words = re.split('[^-a-zA-Z0-9_]+', line) + m = closebrace_pat.match(line) + if m: + name = words[1] +@@ -574,7 +574,7 @@ def mk_def_file_internal(defname, dll_na + for line in api: + m = pat1.match(line) + if m: +- words = re.split('\W+', line) ++ words = re.split(r'\W+', line) + i = 0 + for w in words: + if w == 'Z3_API': +@@ -618,9 +618,9 @@ def mk_gparams_register_modules_internal + fout = open(fullname, 'w') + fout.write('// Automatically generated file.\n') + fout.write('#include "util/gparams.h"\n') +- reg_pat = re.compile('[ \t]*REG_PARAMS\(\'([^\']*)\'\)') +- reg_mod_pat = re.compile('[ \t]*REG_MODULE_PARAMS\(\'([^\']*)\', *\'([^\']*)\'\)') +- reg_mod_descr_pat = re.compile('[ \t]*REG_MODULE_DESCRIPTION\(\'([^\']*)\', *\'([^\']*)\'\)') ++ reg_pat = re.compile(r'[ \t]*REG_PARAMS\(\'([^\']*)\'\)') ++ reg_mod_pat = re.compile(r'[ \t]*REG_MODULE_PARAMS\(\'([^\']*)\', *\'([^\']*)\'\)') ++ reg_mod_descr_pat = re.compile(r'[ \t]*REG_MODULE_DESCRIPTION\(\'([^\']*)\', *\'([^\']*)\'\)') + for h_file in sorted_headers_by_component(h_files_full_path): + added_include = False + with io.open(h_file, encoding='utf-8', mode='r') as fin: +@@ -698,9 +698,9 @@ def mk_install_tactic_cpp_internal(h_fil + fout.write('#include "cmd_context/tactic_cmds.h"\n') + fout.write('#include "cmd_context/simplifier_cmds.h"\n') + fout.write('#include "cmd_context/cmd_context.h"\n') +- tactic_pat = re.compile('[ \t]*ADD_TACTIC\(.*\)') +- probe_pat = re.compile('[ \t]*ADD_PROBE\(.*\)') +- simplifier_pat = re.compile('[ \t]*ADD_SIMPLIFIER\(.*\)') ++ tactic_pat = re.compile(r'[ \t]*ADD_TACTIC\(.*\)') ++ probe_pat = re.compile(r'[ \t]*ADD_PROBE\(.*\)') ++ simplifier_pat = re.compile(r'[ \t]*ADD_SIMPLIFIER\(.*\)') + for h_file in sorted_headers_by_component(h_files_full_path): + added_include = False + try: +@@ -780,10 +780,10 @@ def mk_mem_initializer_cpp_internal(h_fi + fullname = os.path.join(path, 'mem_initializer.cpp') + fout = open(fullname, 'w') + fout.write('// Automatically generated file.\n') +- initializer_pat = re.compile('[ \t]*ADD_INITIALIZER\(\'([^\']*)\'\)') ++ initializer_pat = re.compile(r'[ \t]*ADD_INITIALIZER\(\'([^\']*)\'\)') + # ADD_INITIALIZER with priority +- initializer_prio_pat = re.compile('[ \t]*ADD_INITIALIZER\(\'([^\']*)\',[ \t]*(-?[0-9]*)\)') +- finalizer_pat = re.compile('[ \t]*ADD_FINALIZER\(\'([^\']*)\'\)') ++ initializer_prio_pat = re.compile(r'[ \t]*ADD_INITIALIZER\(\'([^\']*)\',[ \t]*(-?[0-9]*)\)') ++ finalizer_pat = re.compile(r'[ \t]*ADD_FINALIZER\(\'([^\']*)\'\)') + for h_file in sorted_headers_by_component(h_files_full_path): + added_include = False + with io.open(h_file, encoding='utf-8', mode='r') as fin: +--- z3-z3-4.12.2/scripts/mk_util.py.orig 2023-07-06 11:53:06.045350565 -0600 ++++ z3-z3-4.12.2/scripts/mk_util.py 2023-07-06 12:02:59.686951602 -0600 +@@ -395,7 +395,7 @@ def check_java(): + else: + # Search for jni.h in the library directories... + t = open('errout', 'r') +- open_pat = re.compile("\[search path for class files: (.*)\]") ++ open_pat = re.compile(r"\[search path for class files: (.*)\]") + cdirs = [] + for line in t: + m = open_pat.match(line) +@@ -808,8 +808,8 @@ def parse_options(): + def extract_c_includes(fname): + result = {} + # We look for well behaved #include directives +- std_inc_pat = re.compile("[ \t]*#include[ \t]*\"(.*)\"[ \t]*") +- system_inc_pat = re.compile("[ \t]*#include[ \t]*\<.*\>[ \t]*") ++ std_inc_pat = re.compile(r"[ \t]*#include[ \t]*\"(.*)\"[ \t]*") ++ system_inc_pat = re.compile(r"[ \t]*#include[ \t]*\<.*\>[ \t]*") + # We should generate and error for any occurrence of #include that does not match the previous pattern. + non_std_inc_pat = re.compile(".*#include.*") + +@@ -1716,7 +1716,7 @@ class DotNetDLLComponent(Component): + + print("Version output to csproj:", version) + +- core_csproj_str = """ ++ core_csproj_str = r""" + + + netstandard1.4 +@@ -2237,7 +2237,7 @@ class DotNetExampleComponent(ExampleComp + else: + platform = 'x86' + +- dotnet_proj_str = """ ++ dotnet_proj_str = r""" + + Exe + netcoreapp2.0 +@@ -3153,7 +3153,7 @@ def mk_vs_proj_property_groups(f, name, + f.write(' Win32Proj\n') + f.write(' %s\n' % get_platform_toolset_str()) + f.write(' \n') +- f.write(' \n') ++ f.write(' \n') + f.write(' \n') + f.write(' %s\n' % type) + f.write(' Unicode\n') +@@ -3164,24 +3164,24 @@ def mk_vs_proj_property_groups(f, name, + f.write(' Unicode\n') + f.write(' false\n') + f.write(' \n') +- f.write(' \n') ++ f.write(' \n') + f.write(' \n') + f.write(' \n') +- f.write(' \n') ++ f.write(' \n') + f.write(' \n') + f.write(' \n') +- f.write(' $(SolutionDir)\$(ProjectName)\$(Configuration)\\n') ++ f.write(' $(SolutionDir)\\$(ProjectName)\\$(Configuration)\\\n') + f.write(' %s\n' % name) + f.write(' .%s\n' % target_ext) +- f.write(' $(SolutionDir)\$(ProjectName)\$(Configuration)\\n') ++ f.write(' $(SolutionDir)\\$(ProjectName)\\$(Configuration)\\\n') + f.write(' %s\n' % name) + f.write(' .%s\n' % target_ext) + f.write(' \n') + f.write(' \n') +- f.write(' $(ProjectName)\$(Configuration)\\n') ++ f.write(' $(ProjectName)\\$(Configuration)\\\n') + f.write(' \n') + f.write(' \n') +- f.write(' $(ProjectName)\$(Configuration)\\n') ++ f.write(' $(ProjectName)\\$(Configuration)\\\n') + f.write(' \n') + + +@@ -3258,7 +3258,7 @@ def mk_vs_proj(name, components): + mk_vs_proj_link_exe(f, name, debug=False) + f.write(' \n') + mk_vs_proj_dep_groups(f, name, components) +- f.write(' \n') ++ f.write(' \n') + f.write(' \n') + f.write(' \n') + f.write('\n') +@@ -3299,7 +3299,7 @@ def mk_vs_proj_dll(name, components): + mk_vs_proj_link_dll(f, name, debug=False) + f.write(' \n') + mk_vs_proj_dep_groups(f, name, components) +- f.write(' \n') ++ f.write(' \n') + f.write(' \n') + f.write(' \n') + f.write('\n') +--- z3-z3-4.12.2/scripts/update_api.py.orig 2023-07-06 12:02:07.510504547 -0600 ++++ z3-z3-4.12.2/scripts/update_api.py 2023-07-06 12:02:19.399378554 -0600 +@@ -116,8 +116,8 @@ class APITypes: + + def def_Types(self, api_files): + global Closures +- pat1 = re.compile(" *def_Type\(\'(.*)\',[^\']*\'(.*)\',[^\']*\'(.*)\'\)[ \t]*") +- pat2 = re.compile("Z3_DECLARE_CLOSURE\((.*),(.*), \((.*)\)\)") ++ pat1 = re.compile(r" *def_Type\(\'(.*)\',[^\']*\'(.*)\',[^\']*\'(.*)\'\)[ \t]*") ++ pat2 = re.compile(r"Z3_DECLARE_CLOSURE\((.*),(.*), \((.*)\)\)") + for api_file in api_files: + with open(api_file, 'r') as api: + for line in api: diff --git a/z3-ocaml.patch b/z3-ocaml.patch new file mode 100644 index 0000000..32e0857 --- /dev/null +++ b/z3-ocaml.patch @@ -0,0 +1,56 @@ +--- z3-z3-4.12.2/scripts/mk_util.py.orig 2023-05-12 13:59:04.000000000 -0600 ++++ z3-z3-4.12.2/scripts/mk_util.py 2023-07-06 11:53:06.045350565 -0600 +@@ -34,7 +34,7 @@ EXAMP_DEBUG_FLAG='' + LDFLAGS=getenv("LDFLAGS", "") + JNI_HOME=getenv("JNI_HOME", None) + OCAMLC=getenv("OCAMLC", "ocamlc") +-OCAMLOPT=getenv("OCAMLOPT", "ocamlopt") ++OCAMLOPT=getenv("OCAMLOPT", None) + OCAML_LIB=getenv("OCAML_LIB", None) + OCAMLFIND=getenv("OCAMLFIND", "ocamlfind") + DOTNET="dotnet" +@@ -460,13 +460,9 @@ def check_ml(): + raise MKException('Failed testing ocamlc compiler. Set environment variable OCAMLC with the path to the Ocaml compiler') + if is_verbose(): + print ('Testing %s...' % OCAMLOPT) +- r = exec_cmd([OCAMLOPT, '-o', 'a.out', 'hello.ml']) +- if r != 0: +- raise MKException('Failed testing ocamlopt compiler. Set environment variable OCAMLOPT with the path to the Ocaml native compiler. Note that ocamlopt may require flexlink to be in your path.') + try: + rmf('hello.cmi') + rmf('hello.cmo') +- rmf('hello.cmx') + rmf('a.out') + rmf('hello.o') + except: +@@ -2069,7 +2065,7 @@ class MLComponent(Component): + out.write('\t%s -linkall -shared -o %s.cmxs -I . -I %s %s.cmxa\n' % (OCAMLOPTF, z3mls, self.sub_dir, z3mls)) + + out.write('\n') +- out.write('ml: %s.cma %s.cmxa %s.cmxs\n' % (z3mls, z3mls, z3mls)) ++ out.write('ml: %s.cma\n' % z3mls) + if IS_OSX: + out.write('\tinstall_name_tool -id %s/libz3.dylib libz3.dylib\n' % (stubs_install_path)) + out.write('\tinstall_name_tool -change libz3.dylib %s/libz3.dylib api/ml/dllz3ml.so\n' % (stubs_install_path)) +@@ -2091,8 +2087,6 @@ class MLComponent(Component): + out.write(get_component(Z3_DLL_COMPONENT).dll_name + '$(SO_EXT) ') + out.write(os.path.join(self.sub_dir, 'META ')) + out.write(os.path.join(self.sub_dir, 'z3ml.cma ')) +- out.write(os.path.join(self.sub_dir, 'z3ml.cmxa ')) +- out.write(os.path.join(self.sub_dir, 'z3ml.cmxs ')) + + def mk_install(self, out): + if is_ml_enabled() and self._install_bindings(): +@@ -2119,12 +2113,9 @@ class MLComponent(Component): + else: + out.write(' ' + os.path.join(self.sub_dir, m) + '.mli') + out.write(' ' + os.path.join(self.sub_dir, m) + '.cmi') +- out.write(' ' + os.path.join(self.sub_dir, m) + '.cmx') + out.write(' %s' % ((os.path.join(self.sub_dir, 'libz3ml$(LIB_EXT)')))) + out.write(' %s' % ((os.path.join(self.sub_dir, 'z3ml$(LIB_EXT)')))) + out.write(' %s' % ((os.path.join(self.sub_dir, 'z3ml.cma')))) +- out.write(' %s' % ((os.path.join(self.sub_dir, 'z3ml.cmxa')))) +- out.write(' %s' % ((os.path.join(self.sub_dir, 'z3ml.cmxs')))) + out.write(' %s' % ((os.path.join(self.sub_dir, 'dllz3ml')))) + if is_windows() or is_cygwin_mingw() or is_msys2(): + out.write('.dll') diff --git a/z3.spec b/z3.spec index ca3ac91..78e4b3e 100644 --- a/z3.spec +++ b/z3.spec @@ -19,11 +19,16 @@ Summary: Satisfiability Modulo Theories (SMT) solver License: MIT URL: https://github.com/Z3Prover/z3 Source0: https://github.com/Z3Prover/z3/archive/%{name}-%{version}.tar.gz +# Do not try to build or install native OCaml artifacts on bytecode-only arches +Patch0: %{name}-ocaml.patch # Change the way python finds the shared object; see bz 1910923 -Patch0: %{name}-python.patch +Patch1: %{name}-python.patch # Add a missing include of cstdint # https://github.com/Z3Prover/z3/pull/6720 -Patch1: %{name}-stdint.patch +Patch2: %{name}-stdint.patch +# Fix malformed python escape sequences +# https://github.com/Z3Prover/z3/pull/6797 +Patch3: %{name}-escapes.patch BuildRequires: cmake BuildRequires: doxygen @@ -146,7 +151,11 @@ Requires: z3-libs = %{version}-%{release} Python 3 interface to z3. %prep -%autosetup -p1 -n %{name}-%{name}-%{version} +%autosetup -N -n %{name}-%{name}-%{version} +%ifnarch %{ocaml_native_compiler} +%patch -P0 -p1 +%endif +%autopatch -m 1 -p1 # Enable verbose builds, use Fedora CFLAGS, preserve timestamps when installing, # include the entire contents of the archives in the library, link the library @@ -221,12 +230,15 @@ mv %{buildroot}%{_libdir}/libz3java.so %{buildroot}%{_libdir}/z3 %endif # Install the OCaml interface -pushd build/api/ml +cd build/api/ml mkdir -p %{buildroot}%{ocamldir}/Z3 -cp -p META *.{a,cma,cmi,cmx,cmxa,cmxs,mli} %{buildroot}%{ocamldir}/Z3 +%ifarch %{ocaml_native_compiler} +cp -p *.cmx{,a,s} %{buildroot}%{ocamldir}/Z3 +%endif +cp -p META *.{a,cma,cmi,mli} %{buildroot}%{ocamldir}/Z3 mkdir -p %{buildroot}%{ocamldir}/stublibs cp -p *.so %{buildroot}%{ocamldir}/stublibs -popd +cd - # We handle the documentation files below rm -rf %{buildroot}%{_docdir}/Z3 @@ -277,21 +289,25 @@ cd - %{ocamldir}/Z3/META %{ocamldir}/Z3/*.cma %{ocamldir}/Z3/*.cmi +%ifarch %{ocaml_native_compiler} %{ocamldir}/Z3/*.cmxs +%endif %{ocamldir}/stublibs/*.so %files -n ocaml-z3-devel %{ocamldir}/Z3/*.a +%ifarch %{ocaml_native_compiler} %{ocamldir}/Z3/*.cmx %{ocamldir}/Z3/*.cmxa +%endif %{ocamldir}/Z3/*.mli %files -n python3-z3 %{python3_sitelib}/z3/ %changelog -* Wed Jun 21 2023 Jerry James - 4.12.2-3 -- Rebuild for OCaml 5.0 +* Mon Jul 10 2023 Jerry James - 4.12.2-3 +- OCaml 5.0.0 rebuild * Thu Jun 15 2023 Python Maint - 4.12.2-2 - Rebuilt for Python 3.12 From a9a7082547f8f5bb86eaaefb4b202ea8209dd482 Mon Sep 17 00:00:00 2001 From: "Richard W.M. Jones" Date: Tue, 11 Jul 2023 11:36:26 +0100 Subject: [PATCH 41/94] ExcludeArch i686 (https://lists.fedoraproject.org/archives/list/devel@lists.fedoraproject.org/message/SPML7CUBSZNI36NLXGVHEG7DNHU3EWOJ/) --- z3.spec | 3 +++ 1 file changed, 3 insertions(+) diff --git a/z3.spec b/z3.spec index 78e4b3e..77421d1 100644 --- a/z3.spec +++ b/z3.spec @@ -1,3 +1,6 @@ +# OCaml packages not built on i686 since OCaml 5 / Fedora 39. +ExcludeArch: %{ix86} + # TODO: A Julia interface is now available, but requires # https://github.com/JuliaInterop/libcxxwrap-julia, which is not currently # available in Fedora. From 332c05596ab38db859763f79c826c929978887f3 Mon Sep 17 00:00:00 2001 From: "Richard W.M. Jones" Date: Wed, 12 Jul 2023 15:30:38 +0100 Subject: [PATCH 42/94] OCaml 5.0 rebuild for Fedora 39 --- z3.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/z3.spec b/z3.spec index 77421d1..282d535 100644 --- a/z3.spec +++ b/z3.spec @@ -16,7 +16,7 @@ ExcludeArch: %{ix86} Name: z3 Version: 4.12.2 -Release: 3%{?dist} +Release: 4%{?dist} Summary: Satisfiability Modulo Theories (SMT) solver License: MIT @@ -309,6 +309,9 @@ cd - %{python3_sitelib}/z3/ %changelog +* Wed Jul 12 2023 Richard W.M. Jones - 4.12.2-4 +- OCaml 5.0 rebuild for Fedora 39 + * Mon Jul 10 2023 Jerry James - 4.12.2-3 - OCaml 5.0.0 rebuild From 7fe18e3f96ae9af89ce3586a2a922e07802641e5 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Fri, 21 Jul 2023 08:41:35 -0600 Subject: [PATCH 43/94] Exclude the OCaml and Java subpackages only on i386 --- z3.spec | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) diff --git a/z3.spec b/z3.spec index 282d535..9555569 100644 --- a/z3.spec +++ b/z3.spec @@ -1,6 +1,3 @@ -# OCaml packages not built on i686 since OCaml 5 / Fedora 39. -ExcludeArch: %{ix86} - # TODO: A Julia interface is now available, but requires # https://github.com/JuliaInterop/libcxxwrap-julia, which is not currently # available in Fedora. @@ -130,6 +127,8 @@ 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} @@ -144,6 +143,7 @@ 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 @@ -287,6 +287,7 @@ cd - %{_jnidir}/com.microsoft.z3*jar %endif +%ifnarch %{ix86} %files -n ocaml-z3 %dir %{ocamldir}/Z3/ %{ocamldir}/Z3/META @@ -304,11 +305,15 @@ cd - %{ocamldir}/Z3/*.cmxa %endif %{ocamldir}/Z3/*.mli +%endif %files -n python3-z3 %{python3_sitelib}/z3/ %changelog +* Fri Jul 21 2023 Jerry James - 4.12.2-4 +- Exclude the OCaml and Java subpackages only on i386 + * Wed Jul 12 2023 Richard W.M. Jones - 4.12.2-4 - OCaml 5.0 rebuild for Fedora 39 From 8f4eee15042fb8e2c394065a50a190463837a668 Mon Sep 17 00:00:00 2001 From: Fedora Release Engineering Date: Sat, 22 Jul 2023 19:35:07 +0000 Subject: [PATCH 44/94] Rebuilt for https://fedoraproject.org/wiki/Fedora_39_Mass_Rebuild Signed-off-by: Fedora Release Engineering --- z3.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/z3.spec b/z3.spec index 9555569..9be6587 100644 --- a/z3.spec +++ b/z3.spec @@ -13,7 +13,7 @@ Name: z3 Version: 4.12.2 -Release: 4%{?dist} +Release: 5%{?dist} Summary: Satisfiability Modulo Theories (SMT) solver License: MIT @@ -311,6 +311,9 @@ cd - %{python3_sitelib}/z3/ %changelog +* Sat Jul 22 2023 Fedora Release Engineering - 4.12.2-5 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_39_Mass_Rebuild + * Fri Jul 21 2023 Jerry James - 4.12.2-4 - Exclude the OCaml and Java subpackages only on i386 From 7ce32a5a195a9b50798a5fb4396a2a3ee5a68c3b Mon Sep 17 00:00:00 2001 From: Jerry James Date: Sun, 23 Jul 2023 08:41:01 -0600 Subject: [PATCH 45/94] Do not build or install the i386 OCaml interface --- z3.spec | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/z3.spec b/z3.spec index 9be6587..12e97a6 100644 --- a/z3.spec +++ b/z3.spec @@ -200,6 +200,7 @@ 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. @@ -216,6 +217,7 @@ sed -i '/^api/s/ libz3\$(SO_EXT)//g' build/Makefile # Fourth, build the OCaml interface %make_build -C build ml +%endif %install export LANG="C.UTF-8" @@ -232,6 +234,7 @@ 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 @@ -242,6 +245,7 @@ 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 From e32772559e0caab4937e9df2983816f8d12dab2c Mon Sep 17 00:00:00 2001 From: Jerry James Date: Sun, 23 Jul 2023 10:03:32 -0600 Subject: [PATCH 46/94] Exclude OCaml BRs on i386 --- z3.spec | 2 ++ 1 file changed, 2 insertions(+) diff --git a/z3.spec b/z3.spec index 12e97a6..f7522b8 100644 --- a/z3.spec +++ b/z3.spec @@ -42,10 +42,12 @@ 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} From 75819831d1d9fda18d2a2184cb8fb2aadb3df6db Mon Sep 17 00:00:00 2001 From: Jerry James Date: Thu, 27 Jul 2023 10:28:07 -0600 Subject: [PATCH 47/94] Rebuild for ocaml-zarith 1.13 --- z3.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/z3.spec b/z3.spec index f7522b8..bcd4392 100644 --- a/z3.spec +++ b/z3.spec @@ -13,7 +13,7 @@ Name: z3 Version: 4.12.2 -Release: 5%{?dist} +Release: 6%{?dist} Summary: Satisfiability Modulo Theories (SMT) solver License: MIT @@ -317,6 +317,9 @@ cd - %{python3_sitelib}/z3/ %changelog +* Thu Jul 27 2023 Jerry James - 4.12.2-6 +- Rebuild for ocaml-zarith 1.13 + * Sat Jul 22 2023 Fedora Release Engineering - 4.12.2-5 - Rebuilt for https://fedoraproject.org/wiki/Fedora_39_Mass_Rebuild From 6e97219e4f68420b197ae8ea54a8ecdcf15470dc Mon Sep 17 00:00:00 2001 From: "Richard W.M. Jones" Date: Thu, 5 Oct 2023 20:46:07 +0100 Subject: [PATCH 48/94] OCaml 5.1 rebuild for Fedora 40 --- z3.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/z3.spec b/z3.spec index bcd4392..501ce62 100644 --- a/z3.spec +++ b/z3.spec @@ -13,7 +13,7 @@ Name: z3 Version: 4.12.2 -Release: 6%{?dist} +Release: 7%{?dist} Summary: Satisfiability Modulo Theories (SMT) solver License: MIT @@ -317,6 +317,9 @@ cd - %{python3_sitelib}/z3/ %changelog +* Thu Oct 05 2023 Richard W.M. Jones - 4.12.2-7 +- OCaml 5.1 rebuild for Fedora 40 + * Thu Jul 27 2023 Jerry James - 4.12.2-6 - Rebuild for ocaml-zarith 1.13 From 69a9e69b2450ba2c4e3eedb4b80c47a24bbc7197 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Sun, 10 Dec 2023 10:31:57 -0700 Subject: [PATCH 49/94] Version 4.12.4 Drop upstreamed patches: python, stdint, escapes --- sources | 2 +- z3-escapes.patch | 205 ----------------------------------------------- z3-python.patch | 21 ----- z3-stdint.patch | 25 ------ z3.spec | 16 ++-- 5 files changed, 7 insertions(+), 262 deletions(-) delete mode 100644 z3-escapes.patch delete mode 100644 z3-python.patch delete mode 100644 z3-stdint.patch diff --git a/sources b/sources index 3d592ee..5c660ed 100644 --- a/sources +++ b/sources @@ -1 +1 @@ -SHA512 (z3-4.12.2.tar.gz) = 375477cbbc9837b44e752c89916409d07bf6a73830b52878aab4f376f08b37dd5ab485da225744d394ab15f2a7e1014edc3be5eb9962934c440a8d55259317e2 +SHA512 (z3-4.12.4.tar.gz) = fcb778d2e3e0d13fc68afcd8724548279f9edbbb4aac1bbb93e00959c33330ab2fd84f2c2e4b0b78f767819725a90b845fc606a9adc931ae1f0a11f4deae433b diff --git a/z3-escapes.patch b/z3-escapes.patch deleted file mode 100644 index 8d1e0c7..0000000 --- a/z3-escapes.patch +++ /dev/null @@ -1,205 +0,0 @@ -Fixes warnings such as these: - -/builddir/build/BUILD/z3-z3-4.12.2/scripts/mk_genfile_common.py:142: SyntaxWarning: invalid escape sequence '\-' - words = re.split('[^\-a-zA-Z0-9_]+', line) -/builddir/build/BUILD/z3-z3-4.12.2/scripts/mk_genfile_common.py:577: SyntaxWarning: invalid escape sequence '\W' - words = re.split('\W+', line) - ---- z3-z3-4.12.2/scripts/mk_genfile_common.py.orig 2023-05-12 13:59:04.000000000 -0600 -+++ z3-z3-4.12.2/scripts/mk_genfile_common.py 2023-07-06 10:52:08.477210179 -0600 -@@ -139,7 +139,7 @@ def mk_z3consts_py_internal(api_files, o - assert False, "Invalid %s, line: %s" % (api_file, linenum) - else: - assert mode == IN_ENUM -- words = re.split('[^\-a-zA-Z0-9_]+', line) -+ words = re.split('[^-a-zA-Z0-9_]+', line) - m = closebrace_pat.match(line) - if m: - name = words[1] -@@ -227,7 +227,7 @@ def mk_z3consts_dotnet_internal(api_file - assert False, "Invalid %s, line: %s" % (api_file, linenum) - else: - assert mode == IN_ENUM -- words = re.split('[^\-a-zA-Z0-9_]+', line) -+ words = re.split('[^-a-zA-Z0-9_]+', line) - m = closebrace_pat.match(line) - if m: - name = words[1] -@@ -315,7 +315,7 @@ def mk_z3consts_java_internal(api_files, - assert False, "Invalid %s, line: %s" % (api_file, linenum) - else: - assert mode == IN_ENUM -- words = re.split('[^\-a-zA-Z0-9_]+', line) -+ words = re.split('[^-a-zA-Z0-9_]+', line) - m = closebrace_pat.match(line) - if m: - name = words[1] -@@ -441,7 +441,7 @@ def mk_z3consts_ml_internal(api_files, o - assert False, "Invalid %s, line: %s" % (api_file, linenum) - else: - assert mode == IN_ENUM -- words = re.split('[^\-a-zA-Z0-9_]+', line) -+ words = re.split('[^-a-zA-Z0-9_]+', line) - m = closebrace_pat.match(line) - if m: - name = words[1] -@@ -574,7 +574,7 @@ def mk_def_file_internal(defname, dll_na - for line in api: - m = pat1.match(line) - if m: -- words = re.split('\W+', line) -+ words = re.split(r'\W+', line) - i = 0 - for w in words: - if w == 'Z3_API': -@@ -618,9 +618,9 @@ def mk_gparams_register_modules_internal - fout = open(fullname, 'w') - fout.write('// Automatically generated file.\n') - fout.write('#include "util/gparams.h"\n') -- reg_pat = re.compile('[ \t]*REG_PARAMS\(\'([^\']*)\'\)') -- reg_mod_pat = re.compile('[ \t]*REG_MODULE_PARAMS\(\'([^\']*)\', *\'([^\']*)\'\)') -- reg_mod_descr_pat = re.compile('[ \t]*REG_MODULE_DESCRIPTION\(\'([^\']*)\', *\'([^\']*)\'\)') -+ reg_pat = re.compile(r'[ \t]*REG_PARAMS\(\'([^\']*)\'\)') -+ reg_mod_pat = re.compile(r'[ \t]*REG_MODULE_PARAMS\(\'([^\']*)\', *\'([^\']*)\'\)') -+ reg_mod_descr_pat = re.compile(r'[ \t]*REG_MODULE_DESCRIPTION\(\'([^\']*)\', *\'([^\']*)\'\)') - for h_file in sorted_headers_by_component(h_files_full_path): - added_include = False - with io.open(h_file, encoding='utf-8', mode='r') as fin: -@@ -698,9 +698,9 @@ def mk_install_tactic_cpp_internal(h_fil - fout.write('#include "cmd_context/tactic_cmds.h"\n') - fout.write('#include "cmd_context/simplifier_cmds.h"\n') - fout.write('#include "cmd_context/cmd_context.h"\n') -- tactic_pat = re.compile('[ \t]*ADD_TACTIC\(.*\)') -- probe_pat = re.compile('[ \t]*ADD_PROBE\(.*\)') -- simplifier_pat = re.compile('[ \t]*ADD_SIMPLIFIER\(.*\)') -+ tactic_pat = re.compile(r'[ \t]*ADD_TACTIC\(.*\)') -+ probe_pat = re.compile(r'[ \t]*ADD_PROBE\(.*\)') -+ simplifier_pat = re.compile(r'[ \t]*ADD_SIMPLIFIER\(.*\)') - for h_file in sorted_headers_by_component(h_files_full_path): - added_include = False - try: -@@ -780,10 +780,10 @@ def mk_mem_initializer_cpp_internal(h_fi - fullname = os.path.join(path, 'mem_initializer.cpp') - fout = open(fullname, 'w') - fout.write('// Automatically generated file.\n') -- initializer_pat = re.compile('[ \t]*ADD_INITIALIZER\(\'([^\']*)\'\)') -+ initializer_pat = re.compile(r'[ \t]*ADD_INITIALIZER\(\'([^\']*)\'\)') - # ADD_INITIALIZER with priority -- initializer_prio_pat = re.compile('[ \t]*ADD_INITIALIZER\(\'([^\']*)\',[ \t]*(-?[0-9]*)\)') -- finalizer_pat = re.compile('[ \t]*ADD_FINALIZER\(\'([^\']*)\'\)') -+ initializer_prio_pat = re.compile(r'[ \t]*ADD_INITIALIZER\(\'([^\']*)\',[ \t]*(-?[0-9]*)\)') -+ finalizer_pat = re.compile(r'[ \t]*ADD_FINALIZER\(\'([^\']*)\'\)') - for h_file in sorted_headers_by_component(h_files_full_path): - added_include = False - with io.open(h_file, encoding='utf-8', mode='r') as fin: ---- z3-z3-4.12.2/scripts/mk_util.py.orig 2023-07-06 11:53:06.045350565 -0600 -+++ z3-z3-4.12.2/scripts/mk_util.py 2023-07-06 12:02:59.686951602 -0600 -@@ -395,7 +395,7 @@ def check_java(): - else: - # Search for jni.h in the library directories... - t = open('errout', 'r') -- open_pat = re.compile("\[search path for class files: (.*)\]") -+ open_pat = re.compile(r"\[search path for class files: (.*)\]") - cdirs = [] - for line in t: - m = open_pat.match(line) -@@ -808,8 +808,8 @@ def parse_options(): - def extract_c_includes(fname): - result = {} - # We look for well behaved #include directives -- std_inc_pat = re.compile("[ \t]*#include[ \t]*\"(.*)\"[ \t]*") -- system_inc_pat = re.compile("[ \t]*#include[ \t]*\<.*\>[ \t]*") -+ std_inc_pat = re.compile(r"[ \t]*#include[ \t]*\"(.*)\"[ \t]*") -+ system_inc_pat = re.compile(r"[ \t]*#include[ \t]*\<.*\>[ \t]*") - # We should generate and error for any occurrence of #include that does not match the previous pattern. - non_std_inc_pat = re.compile(".*#include.*") - -@@ -1716,7 +1716,7 @@ class DotNetDLLComponent(Component): - - print("Version output to csproj:", version) - -- core_csproj_str = """ -+ core_csproj_str = r""" - - - netstandard1.4 -@@ -2237,7 +2237,7 @@ class DotNetExampleComponent(ExampleComp - else: - platform = 'x86' - -- dotnet_proj_str = """ -+ dotnet_proj_str = r""" - - Exe - netcoreapp2.0 -@@ -3153,7 +3153,7 @@ def mk_vs_proj_property_groups(f, name, - f.write(' Win32Proj\n') - f.write(' %s\n' % get_platform_toolset_str()) - f.write(' \n') -- f.write(' \n') -+ f.write(' \n') - f.write(' \n') - f.write(' %s\n' % type) - f.write(' Unicode\n') -@@ -3164,24 +3164,24 @@ def mk_vs_proj_property_groups(f, name, - f.write(' Unicode\n') - f.write(' false\n') - f.write(' \n') -- f.write(' \n') -+ f.write(' \n') - f.write(' \n') - f.write(' \n') -- f.write(' \n') -+ f.write(' \n') - f.write(' \n') - f.write(' \n') -- f.write(' $(SolutionDir)\$(ProjectName)\$(Configuration)\\n') -+ f.write(' $(SolutionDir)\\$(ProjectName)\\$(Configuration)\\\n') - f.write(' %s\n' % name) - f.write(' .%s\n' % target_ext) -- f.write(' $(SolutionDir)\$(ProjectName)\$(Configuration)\\n') -+ f.write(' $(SolutionDir)\\$(ProjectName)\\$(Configuration)\\\n') - f.write(' %s\n' % name) - f.write(' .%s\n' % target_ext) - f.write(' \n') - f.write(' \n') -- f.write(' $(ProjectName)\$(Configuration)\\n') -+ f.write(' $(ProjectName)\\$(Configuration)\\\n') - f.write(' \n') - f.write(' \n') -- f.write(' $(ProjectName)\$(Configuration)\\n') -+ f.write(' $(ProjectName)\\$(Configuration)\\\n') - f.write(' \n') - - -@@ -3258,7 +3258,7 @@ def mk_vs_proj(name, components): - mk_vs_proj_link_exe(f, name, debug=False) - f.write(' \n') - mk_vs_proj_dep_groups(f, name, components) -- f.write(' \n') -+ f.write(' \n') - f.write(' \n') - f.write(' \n') - f.write('\n') -@@ -3299,7 +3299,7 @@ def mk_vs_proj_dll(name, components): - mk_vs_proj_link_dll(f, name, debug=False) - f.write(' \n') - mk_vs_proj_dep_groups(f, name, components) -- f.write(' \n') -+ f.write(' \n') - f.write(' \n') - f.write(' \n') - f.write('\n') ---- z3-z3-4.12.2/scripts/update_api.py.orig 2023-07-06 12:02:07.510504547 -0600 -+++ z3-z3-4.12.2/scripts/update_api.py 2023-07-06 12:02:19.399378554 -0600 -@@ -116,8 +116,8 @@ class APITypes: - - def def_Types(self, api_files): - global Closures -- pat1 = re.compile(" *def_Type\(\'(.*)\',[^\']*\'(.*)\',[^\']*\'(.*)\'\)[ \t]*") -- pat2 = re.compile("Z3_DECLARE_CLOSURE\((.*),(.*), \((.*)\)\)") -+ pat1 = re.compile(r" *def_Type\(\'(.*)\',[^\']*\'(.*)\',[^\']*\'(.*)\'\)[ \t]*") -+ pat2 = re.compile(r"Z3_DECLARE_CLOSURE\((.*),(.*), \((.*)\)\)") - for api_file in api_files: - with open(api_file, 'r') as api: - for line in api: diff --git a/z3-python.patch b/z3-python.patch deleted file mode 100644 index c26dd68..0000000 --- a/z3-python.patch +++ /dev/null @@ -1,21 +0,0 @@ ---- a/scripts/update_api.py 2020-09-10 12:51:28.000000000 -0600 -+++ b/scripts/update_api.py 2020-12-25 17:03:00.196777823 -0700 -@@ -1755,15 +1755,15 @@ def write_core_py_preamble(core_py): - # Automatically generated file - import sys, os - import ctypes --import pkg_resources -+import sysconfig - from .z3types import * - from .z3consts import * - --_ext = 'dll' if sys.platform in ('win32', 'cygwin') else 'dylib' if sys.platform == 'darwin' else 'so' -+_ext = 'dll' if sys.platform in ('win32', 'cygwin') else 'dylib' if sys.platform == 'darwin' else 'so.@MAJVER@' - _lib = None - _default_dirs = ['.', - os.path.dirname(os.path.abspath(__file__)), -- pkg_resources.resource_filename('z3', 'lib'), -+ sysconfig.get_config_var('LIBDIR'), - os.path.join(sys.prefix, 'lib'), - None] - _all_dirs = [] diff --git a/z3-stdint.patch b/z3-stdint.patch deleted file mode 100644 index c0874f2..0000000 --- a/z3-stdint.patch +++ /dev/null @@ -1,25 +0,0 @@ -Fixes errors such as these: - -In file included from /builddir/build/BUILD/z3-z3-4.12.2/src/util/region.cpp:53: -/builddir/build/BUILD/z3-z3-4.12.2/src/util/region.cpp: In member function ‘void* region::allocate(size_t)’: -/builddir/build/BUILD/z3-z3-4.12.2/src/util/tptr.h:29:62: error: ‘uintptr_t’ does not name a type - 29 | #define ALIGN(T, PTR) reinterpret_cast(((reinterpret_cast(PTR) >> PTR_ALIGNMENT) + \ - | ^~~~~~~~~ -/builddir/build/BUILD/z3-z3-4.12.2/src/util/region.cpp:82:22: note: in expansion of macro ‘ALIGN’ - 82 | m_curr_ptr = ALIGN(char *, new_curr_ptr); - | ^~~~~ -/builddir/build/BUILD/z3-z3-4.12.2/src/util/region.cpp:57:1: note: ‘uintptr_t’ is defined in header ‘’; did you forget to ‘#include ’? - 56 | #include "util/page.h" - +++ |+#include - 57 | - ---- z3-z3-4.12.2/src/util/tptr.h.orig 2023-05-12 13:59:04.000000000 -0600 -+++ z3-z3-4.12.2/src/util/tptr.h 2023-05-13 07:04:48.389716628 -0600 -@@ -19,6 +19,7 @@ Revision History: - - #pragma once - -+#include - #include "util/machine.h" - - #define TAG_SHIFT PTR_ALIGNMENT diff --git a/z3.spec b/z3.spec index 501ce62..1c1163b 100644 --- a/z3.spec +++ b/z3.spec @@ -12,8 +12,8 @@ %bcond_with test Name: z3 -Version: 4.12.2 -Release: 7%{?dist} +Version: 4.12.4 +Release: 1%{?dist} Summary: Satisfiability Modulo Theories (SMT) solver License: MIT @@ -21,14 +21,6 @@ URL: https://github.com/Z3Prover/z3 Source0: https://github.com/Z3Prover/z3/archive/%{name}-%{version}.tar.gz # Do not try to build or install native OCaml artifacts on bytecode-only arches Patch0: %{name}-ocaml.patch -# Change the way python finds the shared object; see bz 1910923 -Patch1: %{name}-python.patch -# Add a missing include of cstdint -# https://github.com/Z3Prover/z3/pull/6720 -Patch2: %{name}-stdint.patch -# Fix malformed python escape sequences -# https://github.com/Z3Prover/z3/pull/6797 -Patch3: %{name}-escapes.patch BuildRequires: cmake BuildRequires: doxygen @@ -317,6 +309,10 @@ cd - %{python3_sitelib}/z3/ %changelog +* Sat Dec 9 2023 Jerry James - 4.12.4-1 +- Version 4.12.4 +- Drop upstreamed patches: python, stdint, escapes + * Thu Oct 05 2023 Richard W.M. Jones - 4.12.2-7 - OCaml 5.1 rebuild for Fedora 40 From 28838627dec7f97a0f2027d7129dd3aa02527f8b Mon Sep 17 00:00:00 2001 From: "Richard W.M. Jones" Date: Tue, 12 Dec 2023 16:17:08 +0000 Subject: [PATCH 50/94] OCaml 5.1.1 rebuild for Fedora 40 --- z3.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/z3.spec b/z3.spec index 1c1163b..dcb57a9 100644 --- a/z3.spec +++ b/z3.spec @@ -13,7 +13,7 @@ Name: z3 Version: 4.12.4 -Release: 1%{?dist} +Release: 2%{?dist} Summary: Satisfiability Modulo Theories (SMT) solver License: MIT @@ -309,6 +309,9 @@ cd - %{python3_sitelib}/z3/ %changelog +* Tue Dec 12 2023 Richard W.M. Jones - 4.12.4-2 +- OCaml 5.1.1 rebuild for Fedora 40 + * Sat Dec 9 2023 Jerry James - 4.12.4-1 - Version 4.12.4 - Drop upstreamed patches: python, stdint, escapes From 4b6c6d8a09b900a24c687a599d03839cb8c53bd5 Mon Sep 17 00:00:00 2001 From: "Richard W.M. Jones" Date: Mon, 18 Dec 2023 17:56:01 +0000 Subject: [PATCH 51/94] OCaml 5.1.1 + s390x code gen fix for Fedora 40 --- z3.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/z3.spec b/z3.spec index dcb57a9..535b6dd 100644 --- a/z3.spec +++ b/z3.spec @@ -13,7 +13,7 @@ Name: z3 Version: 4.12.4 -Release: 2%{?dist} +Release: 3%{?dist} Summary: Satisfiability Modulo Theories (SMT) solver License: MIT @@ -309,6 +309,9 @@ cd - %{python3_sitelib}/z3/ %changelog +* Mon Dec 18 2023 Richard W.M. Jones - 4.12.4-3 +- OCaml 5.1.1 + s390x code gen fix for Fedora 40 + * Tue Dec 12 2023 Richard W.M. Jones - 4.12.4-2 - OCaml 5.1.1 rebuild for Fedora 40 From 7e13c112079c11617e21642f3925b25a61ce62bf Mon Sep 17 00:00:00 2001 From: Jerry James Date: Thu, 21 Dec 2023 09:06:18 -0700 Subject: [PATCH 52/94] Fix python package library load name (bz 2255464) --- z3.spec | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/z3.spec b/z3.spec index 535b6dd..b7bc47a 100644 --- a/z3.spec +++ b/z3.spec @@ -13,7 +13,7 @@ Name: z3 Version: 4.12.4 -Release: 3%{?dist} +Release: 4%{?dist} Summary: Satisfiability Modulo Theories (SMT) solver License: MIT @@ -170,7 +170,7 @@ sed \ # 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/@MAJVER@/$majver/" \ + -e "s/'so'/'so.$majver'/" \ -i scripts/update_api.py # Turn off HTML timestamps for reproducible builds @@ -309,6 +309,9 @@ cd - %{python3_sitelib}/z3/ %changelog +* Thu Dec 21 2023 Jerry James - 4.12.4-4 +- Fix python package library load name (bz 2255464) + * Mon Dec 18 2023 Richard W.M. Jones - 4.12.4-3 - OCaml 5.1.1 + s390x code gen fix for Fedora 40 From a4add3eaf2eb41427ff3ee5d999e05cd01e9de4c Mon Sep 17 00:00:00 2001 From: Fedora Release Engineering Date: Sat, 27 Jan 2024 10:55:07 +0000 Subject: [PATCH 53/94] Rebuilt for https://fedoraproject.org/wiki/Fedora_40_Mass_Rebuild --- z3.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/z3.spec b/z3.spec index b7bc47a..7bd0a66 100644 --- a/z3.spec +++ b/z3.spec @@ -13,7 +13,7 @@ Name: z3 Version: 4.12.4 -Release: 4%{?dist} +Release: 5%{?dist} Summary: Satisfiability Modulo Theories (SMT) solver License: MIT @@ -309,6 +309,9 @@ cd - %{python3_sitelib}/z3/ %changelog +* Sat Jan 27 2024 Fedora Release Engineering - 4.12.4-5 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_40_Mass_Rebuild + * Thu Dec 21 2023 Jerry James - 4.12.4-4 - Fix python package library load name (bz 2255464) From cf507c8fcc64614dcc63b05275790146eec22ea2 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Sat, 27 Jan 2024 21:04:05 -0700 Subject: [PATCH 54/94] Version 4.12.5 --- sources | 2 +- z3.spec | 7 +++++-- 2 files changed, 6 insertions(+), 3 deletions(-) diff --git a/sources b/sources index 5c660ed..107125f 100644 --- a/sources +++ b/sources @@ -1 +1 @@ -SHA512 (z3-4.12.4.tar.gz) = fcb778d2e3e0d13fc68afcd8724548279f9edbbb4aac1bbb93e00959c33330ab2fd84f2c2e4b0b78f767819725a90b845fc606a9adc931ae1f0a11f4deae433b +SHA512 (z3-4.12.5.tar.gz) = b5055468d1380c54b959f826e10846c323c0ef73cf6bba0970e187c38cabd5869786261cd9b89a89d8369144417180870627782bf705e5494286dfe75053c9a7 diff --git a/z3.spec b/z3.spec index 7bd0a66..af945cd 100644 --- a/z3.spec +++ b/z3.spec @@ -12,8 +12,8 @@ %bcond_with test Name: z3 -Version: 4.12.4 -Release: 5%{?dist} +Version: 4.12.5 +Release: 1%{?dist} Summary: Satisfiability Modulo Theories (SMT) solver License: MIT @@ -309,6 +309,9 @@ cd - %{python3_sitelib}/z3/ %changelog +* Sat Jan 27 2024 Jerry James - 4.12.5-1 +- Version 4.12.5 + * Sat Jan 27 2024 Fedora Release Engineering - 4.12.4-5 - Rebuilt for https://fedoraproject.org/wiki/Fedora_40_Mass_Rebuild From 31d363f3eca890651a1e7b83c09b409025770163 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Sun, 25 Feb 2024 11:49:38 -0700 Subject: [PATCH 55/94] Version 4.12.6 --- sources | 2 +- z3.spec | 12 ++++++++---- 2 files changed, 9 insertions(+), 5 deletions(-) diff --git a/sources b/sources index 107125f..8c0844b 100644 --- a/sources +++ b/sources @@ -1 +1 @@ -SHA512 (z3-4.12.5.tar.gz) = b5055468d1380c54b959f826e10846c323c0ef73cf6bba0970e187c38cabd5869786261cd9b89a89d8369144417180870627782bf705e5494286dfe75053c9a7 +SHA512 (z3-4.12.6.tar.gz) = 10883877d20adbd229ad4bf65a9b50660d93d85514f933865f06920efd697f51ce34e502fbe451d4c1b2251f13d597050b8277036d4011d9c0f196111d681f8f diff --git a/z3.spec b/z3.spec index af945cd..1c21a6d 100644 --- a/z3.spec +++ b/z3.spec @@ -9,16 +9,17 @@ # Tests are off by default because some of the tests require more memory than # the koji builders have available. -%bcond_with test +%bcond test 0 Name: z3 -Version: 4.12.5 +Version: 4.12.6 Release: 1%{?dist} Summary: Satisfiability Modulo Theories (SMT) solver License: MIT -URL: https://github.com/Z3Prover/z3 -Source0: https://github.com/Z3Prover/z3/archive/%{name}-%{version}.tar.gz +URL: https://github.com/Z3Prover/z3/wiki +VCS: https://github.com/Z3Prover/z3 +Source0: %{vcs}/archive/%{name}-%{version}.tar.gz # Do not try to build or install native OCaml artifacts on bytecode-only arches Patch0: %{name}-ocaml.patch @@ -309,6 +310,9 @@ cd - %{python3_sitelib}/z3/ %changelog +* Sun Feb 25 2024 Jerry James - 4.12.6-1 +- Version 4.12.6 + * Sat Jan 27 2024 Jerry James - 4.12.5-1 - Version 4.12.5 From d8b406fe9c052d327b7e547e59c9f38d554a66ec Mon Sep 17 00:00:00 2001 From: Jerry James Date: Thu, 14 Mar 2024 14:37:41 -0600 Subject: [PATCH 56/94] Version 4.13.0 --- sources | 2 +- z3.spec | 7 +++++-- 2 files changed, 6 insertions(+), 3 deletions(-) diff --git a/sources b/sources index 8c0844b..5cc3163 100644 --- a/sources +++ b/sources @@ -1 +1 @@ -SHA512 (z3-4.12.6.tar.gz) = 10883877d20adbd229ad4bf65a9b50660d93d85514f933865f06920efd697f51ce34e502fbe451d4c1b2251f13d597050b8277036d4011d9c0f196111d681f8f +SHA512 (z3-4.13.0.tar.gz) = 8503787fe0b18592b5a131bcec2cacfa5f5096d76386a1c4fda7a836e472924b154433306d27600ff0d0758ddb710c965901fbfc2e5605919b624b9d4d1bc4fd diff --git a/z3.spec b/z3.spec index 1c21a6d..3c41c3d 100644 --- a/z3.spec +++ b/z3.spec @@ -12,7 +12,7 @@ %bcond test 0 Name: z3 -Version: 4.12.6 +Version: 4.13.0 Release: 1%{?dist} Summary: Satisfiability Modulo Theories (SMT) solver @@ -268,7 +268,7 @@ cd - %files libs %license LICENSE.txt -%{_libdir}/libz3.so.4.12* +%{_libdir}/libz3.so.4.13* %files devel %{_includedir}/z3/ @@ -310,6 +310,9 @@ cd - %{python3_sitelib}/z3/ %changelog +* Thu Mar 14 2024 Jerry James - 4.13.0-1 +- Version 4.13.0 + * Sun Feb 25 2024 Jerry James - 4.12.6-1 - Version 4.12.6 From a44dc82abc9ea1c45cf446545384ac9e0f8796e6 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Thu, 23 May 2024 10:52:23 -0600 Subject: [PATCH 57/94] Improve the generated man page --- z3.spec | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/z3.spec b/z3.spec index 3c41c3d..87d7f79 100644 --- a/z3.spec +++ b/z3.spec @@ -247,7 +247,8 @@ rm -rf %{buildroot}%{_docdir}/Z3 # Make a man page mkdir -p %{buildroot}%{_mandir}/man1 -help2man -N -o %{buildroot}%{_mandir}/man1/z3.1 %{_vpath_builddir}/z3 +help2man -N -o %{buildroot}%{_mandir}/man1/z3.1 \ + -n 'Satisfiability Modulo Theories (SMT) solver' %{_vpath_builddir}/z3 # Fix the pkgconfig file sed -i 's,//usr,,' %{buildroot}%{_libdir}/pkgconfig/z3.pc From f6c7a66d3df7970db8a8bd069fc9fa1bfbd76d80 Mon Sep 17 00:00:00 2001 From: "Richard W.M. Jones" Date: Wed, 29 May 2024 18:36:51 +0100 Subject: [PATCH 58/94] OCaml 5.2.0 for Fedora 41 --- z3.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/z3.spec b/z3.spec index 87d7f79..1cbbb5d 100644 --- a/z3.spec +++ b/z3.spec @@ -13,7 +13,7 @@ Name: z3 Version: 4.13.0 -Release: 1%{?dist} +Release: 2%{?dist} Summary: Satisfiability Modulo Theories (SMT) solver License: MIT @@ -311,6 +311,9 @@ cd - %{python3_sitelib}/z3/ %changelog +* Wed May 29 2024 Richard W.M. Jones - 4.13.0-2 +- OCaml 5.2.0 for Fedora 41 + * Thu Mar 14 2024 Jerry James - 4.13.0-1 - Version 4.13.0 From 16e38e17b295a4bd4a58034d9d1188a5c95e8b48 Mon Sep 17 00:00:00 2001 From: Python Maint Date: Fri, 7 Jun 2024 10:33:09 +0200 Subject: [PATCH 59/94] Rebuilt for Python 3.13 --- z3.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/z3.spec b/z3.spec index 1cbbb5d..33aaf28 100644 --- a/z3.spec +++ b/z3.spec @@ -13,7 +13,7 @@ Name: z3 Version: 4.13.0 -Release: 2%{?dist} +Release: 3%{?dist} Summary: Satisfiability Modulo Theories (SMT) solver License: MIT @@ -311,6 +311,9 @@ cd - %{python3_sitelib}/z3/ %changelog +* Fri Jun 07 2024 Python Maint - 4.13.0-3 +- Rebuilt for Python 3.13 + * Wed May 29 2024 Richard W.M. Jones - 4.13.0-2 - OCaml 5.2.0 for Fedora 41 From bed9a8e94c432e749debbbccdad20c94a1349dd5 Mon Sep 17 00:00:00 2001 From: "Richard W.M. Jones" Date: Wed, 19 Jun 2024 14:06:51 +0100 Subject: [PATCH 60/94] OCaml 5.2.0 ppc64le fix --- z3.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/z3.spec b/z3.spec index 33aaf28..466e69c 100644 --- a/z3.spec +++ b/z3.spec @@ -13,7 +13,7 @@ Name: z3 Version: 4.13.0 -Release: 3%{?dist} +Release: 4%{?dist} Summary: Satisfiability Modulo Theories (SMT) solver License: MIT @@ -311,6 +311,9 @@ cd - %{python3_sitelib}/z3/ %changelog +* Wed Jun 19 2024 Richard W.M. Jones - 4.13.0-4 +- OCaml 5.2.0 ppc64le fix + * Fri Jun 07 2024 Python Maint - 4.13.0-3 - Rebuilt for Python 3.13 From 7fa958b88af494381e5972c23824d82b42fccc1b Mon Sep 17 00:00:00 2001 From: Jerry James Date: Tue, 16 Jul 2024 08:42:38 -0600 Subject: [PATCH 61/94] Rebuild for ocaml-zarith 1.14 --- z3.spec | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) diff --git a/z3.spec b/z3.spec index 466e69c..4679f46 100644 --- a/z3.spec +++ b/z3.spec @@ -11,17 +11,19 @@ # the koji builders have available. %bcond test 0 +%global giturl https://github.com/Z3Prover/z3 + Name: z3 Version: 4.13.0 -Release: 4%{?dist} +Release: 5%{?dist} Summary: Satisfiability Modulo Theories (SMT) solver License: MIT URL: https://github.com/Z3Prover/z3/wiki -VCS: https://github.com/Z3Prover/z3 -Source0: %{vcs}/archive/%{name}-%{version}.tar.gz +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 -Patch0: %{name}-ocaml.patch +Patch: %{name}-ocaml.patch BuildRequires: cmake BuildRequires: doxygen @@ -311,6 +313,9 @@ cd - %{python3_sitelib}/z3/ %changelog +* Tue Jul 16 2024 Jerry James - 4.13.0-5 +- Rebuild for ocaml-zarith 1.14 + * Wed Jun 19 2024 Richard W.M. Jones - 4.13.0-4 - OCaml 5.2.0 ppc64le fix From 38a5e05a253bfb0f0cb637f9015387c6ef51a805 Mon Sep 17 00:00:00 2001 From: Fedora Release Engineering Date: Sat, 20 Jul 2024 10:46:27 +0000 Subject: [PATCH 62/94] Rebuilt for https://fedoraproject.org/wiki/Fedora_41_Mass_Rebuild --- z3.spec | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/z3.spec b/z3.spec index 4679f46..d6a7651 100644 --- a/z3.spec +++ b/z3.spec @@ -15,7 +15,7 @@ Name: z3 Version: 4.13.0 -Release: 5%{?dist} +Release: 6%{?dist} Summary: Satisfiability Modulo Theories (SMT) solver License: MIT @@ -313,6 +313,9 @@ cd - %{python3_sitelib}/z3/ %changelog +* Sat Jul 20 2024 Fedora Release Engineering - 4.13.0-6 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_41_Mass_Rebuild + * Tue Jul 16 2024 Jerry James - 4.13.0-5 - Rebuild for ocaml-zarith 1.14 From 2ff3fe8839d3bf162c7683f967c9dd30e36ef370 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Fri, 27 Sep 2024 16:53:39 -0600 Subject: [PATCH 63/94] Convert to %autorelease and %autochangelog [skip changelog] --- changelog | 387 +++++++++++++++++++++++++++++++++++++++++++++++++++++ z3.spec | 390 +----------------------------------------------------- 2 files changed, 389 insertions(+), 388 deletions(-) create mode 100644 changelog diff --git a/changelog b/changelog new file mode 100644 index 0000000..a2b32bb --- /dev/null +++ b/changelog @@ -0,0 +1,387 @@ +* Sat Jul 20 2024 Fedora Release Engineering - 4.13.0-6 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_41_Mass_Rebuild + +* Tue Jul 16 2024 Jerry James - 4.13.0-5 +- Rebuild for ocaml-zarith 1.14 + +* Wed Jun 19 2024 Richard W.M. Jones - 4.13.0-4 +- OCaml 5.2.0 ppc64le fix + +* Fri Jun 07 2024 Python Maint - 4.13.0-3 +- Rebuilt for Python 3.13 + +* Wed May 29 2024 Richard W.M. Jones - 4.13.0-2 +- OCaml 5.2.0 for Fedora 41 + +* Thu Mar 14 2024 Jerry James - 4.13.0-1 +- Version 4.13.0 + +* Sun Feb 25 2024 Jerry James - 4.12.6-1 +- Version 4.12.6 + +* Sat Jan 27 2024 Jerry James - 4.12.5-1 +- Version 4.12.5 + +* Sat Jan 27 2024 Fedora Release Engineering - 4.12.4-5 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_40_Mass_Rebuild + +* Thu Dec 21 2023 Jerry James - 4.12.4-4 +- Fix python package library load name (bz 2255464) + +* Mon Dec 18 2023 Richard W.M. Jones - 4.12.4-3 +- OCaml 5.1.1 + s390x code gen fix for Fedora 40 + +* Tue Dec 12 2023 Richard W.M. Jones - 4.12.4-2 +- OCaml 5.1.1 rebuild for Fedora 40 + +* Sat Dec 9 2023 Jerry James - 4.12.4-1 +- Version 4.12.4 +- Drop upstreamed patches: python, stdint, escapes + +* Thu Oct 05 2023 Richard W.M. Jones - 4.12.2-7 +- OCaml 5.1 rebuild for Fedora 40 + +* Thu Jul 27 2023 Jerry James - 4.12.2-6 +- Rebuild for ocaml-zarith 1.13 + +* Sat Jul 22 2023 Fedora Release Engineering - 4.12.2-5 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_39_Mass_Rebuild + +* Fri Jul 21 2023 Jerry James - 4.12.2-4 +- Exclude the OCaml and Java subpackages only on i386 + +* Wed Jul 12 2023 Richard W.M. Jones - 4.12.2-4 +- OCaml 5.0 rebuild for Fedora 39 + +* Mon Jul 10 2023 Jerry James - 4.12.2-3 +- OCaml 5.0.0 rebuild + +* Thu Jun 15 2023 Python Maint - 4.12.2-2 +- Rebuilt for Python 3.12 + +* Mon May 15 2023 Jerry James - 4.12.2-1 +- Version 4.12.2 + +* Tue Jan 24 2023 Richard W.M. Jones - 4.12.1-2 +- Rebuild OCaml packages for F38 + +* Sat Jan 21 2023 Jerry James - 4.12.1-1 +- Version 4.12.1 + +* Sat Jan 21 2023 Fedora Release Engineering - 4.12.0-2 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_38_Mass_Rebuild + +* Tue Jan 17 2023 Jerry James - 4.12.0-1 +- Version 4.12.0 +- Drop upstreamed -data-race and -uninit patches + +* Sun Jan 8 2023 Jerry James - 4.11.2-2 +- Add -data-race patch to fix segfault (bz 2157972) +- Add -uninit patch to fix use of an uninitialized value + +* Wed Dec 14 2022 Jerry James - 4.11.2-1 +- Further clarify license of the doc subpackage (SPDX) + +* Sun Sep 4 2022 Jerry James - 4.11.2-1 +- Version 4.11.2 + +* Fri Aug 19 2022 Jerry James - 4.11.0-1 +- Version 4.11.0 +- Clarify license of the doc subpackage + +* Mon Aug 8 2022 Jerry James - 4.10.2-1 +- Version 4.10.2 + +* Sat Jul 23 2022 Fedora Release Engineering - 4.8.17-6 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_37_Mass_Rebuild + +* Tue Jun 28 2022 Jerry James - 4.8.17-5 +- Do not support Java on i686 (rhbz#2104112) +- Use new OCaml macros + +* Mon Jun 20 2022 Python Maint - 4.8.17-4 +- Rebuilt for Python 3.11 + +* Sat Jun 18 2022 Richard W.M. Jones - 4.8.17-3 +- OCaml 4.14.0 rebuild + +* Mon Jun 13 2022 Python Maint - 4.8.17-2 +- Rebuilt for Python 3.11 + +* Mon May 16 2022 Jerry James - 4.8.17-1 +- Version 4.8.17 +- Drop upstreamed -ambiguous-overload patch + +* Thu Mar 24 2022 Jerry James - 4.8.15-2 +- Add -ambiguous-overload patch to fix cppcheck build failure + +* Mon Mar 21 2022 Jerry James - 4.8.15-1 +- Version 4.8.15 + +* Sat Feb 05 2022 Jiri Vanek - 4.8.14-4 +- Rebuilt for java-17-openjdk as system jdk + +* Fri Feb 04 2022 Richard W.M. Jones - 4.8.14-3 +- OCaml 4.13.1 rebuild to remove package notes + +* Sat Jan 22 2022 Fedora Release Engineering - 4.8.14-2 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_36_Mass_Rebuild + +* Fri Dec 24 2021 Jerry James - 4.8.14-1 +- Version 4.8.14 +- Conditionalize the %%check script + +* Fri Nov 19 2021 Jerry James - 4.8.13-1 +- Version 4.8.13 + +* Mon Oct 04 2021 Richard W.M. Jones - 4.8.12-3 +- OCaml 4.13.1 build + +* Fri Jul 23 2021 Fedora Release Engineering - 4.8.12-2 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_35_Mass_Rebuild + +* Tue Jul 13 2021 Jerry James - 4.8.12-1 +- Version 4.8.12 + +* Sun Jun 6 2021 Jerry James - 4.8.11-1 +- Version 4.8.11 + +* Fri Jun 04 2021 Python Maint - 4.8.10-6 +- Rebuilt for Python 3.10 + +* Wed Mar 3 2021 Jerry James - 4.8.10-5 +- Rebuild for ocaml-zarith 1.12 + +* Mon Mar 1 20:17:48 GMT 2021 Richard W.M. Jones - 4.8.10-4 +- Bump release and rebuild. + +* Mon Mar 1 19:41:16 GMT 2021 Richard W.M. Jones - 4.8.10-3 +- Bump release and rebuild. + +* Mon Mar 1 16:57:45 GMT 2021 Richard W.M. Jones - 4.8.10-2 +- OCaml 4.12.0 build + +* Sat Feb 13 2021 Jerry James - 4.8.10-1 +- Version 4.8.10 + +* Thu Jan 28 2021 Fedora Release Engineering - 4.8.9-5 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_34_Mass_Rebuild + +* Fri Dec 25 2020 Jerry James - 4.8.9-4 +- Fix the python interface (bz 1910923) + +* Mon Nov 16 2020 Jerry James - 4.8.9-3 +- Rebuild for ocaml-zarith 1.11 + +* Fri Sep 25 2020 Jerry James - 4.8.9-2 +- Rebuild for ocaml-zarith 1.10 + +* Fri Sep 11 2020 Jerry James - 4.8.9-1 +- Version 4.8.9 + +* Tue Sep 01 2020 Richard W.M. Jones - 4.8.8-7 +- OCaml 4.11.1 rebuild + +* Fri Aug 21 2020 Richard W.M. Jones - 4.8.8-6 +- OCaml 4.11.0 rebuild + +* Wed Jul 29 2020 Fedora Release Engineering - 4.8.8-5 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_33_Mass_Rebuild + +* Mon Jul 27 2020 Jerry James - 4.8.8-4 +- Build with cmake +- Manually build the OCaml interface +- Limit the class file version in the Java interface +- Allow the library to hide internal symbols; this means that the binary can no + longer be linked with the library, so the main package does not depend on + the -libs package +- The python package no longer contains an ELF object, so make it noarch + +* Sat Jul 11 2020 Jiri Vanek - 4.8.8-4 +- Rebuilt for JDK-11, see https://fedoraproject.org/wiki/Changes/Java11 + +* Tue May 26 2020 Miro Hrončok - 4.8.8-3 +- Rebuilt for Python 3.9 + +* Thu May 14 2020 Wolfgang Stöggl - 4.8.8-2 +- Add Z3 cmake files required by find_package(Z3) + +* Sat May 9 2020 Jerry James - 4.8.8-1 +- Version 4.8.8 +- Drop all patches; all have been upstreamed + +* Mon May 04 2020 Richard W.M. Jones - 4.8.7-10 +- OCaml 4.11.0+dev2-2020-04-22 rebuild + +* Tue Apr 21 2020 Richard W.M. Jones - 4.8.7-9 +- OCaml 4.11.0 pre-release attempt 2 + +* Fri Apr 17 2020 Richard W.M. Jones - 4.8.7-8 +- OCaml 4.11.0 pre-release + +* Thu Apr 02 2020 Richard W.M. Jones - 4.8.7-7 +- Update all OCaml dependencies for RPM 4.16. + +* Wed Feb 26 2020 Richard W.M. Jones - 4.8.7-6 +- OCaml 4.10.0 final. + +* Fri Jan 31 2020 Fedora Release Engineering - 4.8.7-5 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_32_Mass_Rebuild + +* Tue Jan 21 2020 Jerry James - 4.8.7-4 +- Make -doc be archful (bz 1792740) +- Add -signed-char and -gcc-10-s390x patches + +* Sun Jan 19 2020 Richard W.M. Jones - 4.8.7-4 +- OCaml 4.10.0+beta1 rebuild. + +* Fri Jan 10 2020 Richard W.M. Jones - 4.8.7-3 +- OCaml 4.09.0 for riscv64 + +* Sat Dec 7 2019 Jerry James - 4.8.7-2 +- OCaml 4.09.0 (final) rebuild + +* Thu Nov 21 2019 Jerry James - 4.8.7-1 +- New upstream version +- Add -ocamldoc patch to fix documentation build failure +- Add -trailing-zeros32 patch to fix build failures on some platforms + +* Fri Sep 20 2019 Jerry James - 4.8.6-1 +- New upstream version + +* Mon Aug 19 2019 Miro Hrončok - 4.8.5-6 +- Rebuilt for Python 3.8 + +* Fri Aug 16 2019 Richard W.M. Jones - 4.8.5-5 +- OCaml 4.08.1 (final) rebuild. + +* Wed Jul 31 2019 Richard W.M. Jones - 4.8.5-4 +- OCaml 4.08.1 (rc2) rebuild. + +* Sat Jul 27 2019 Fedora Release Engineering - 4.8.5-3 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_31_Mass_Rebuild + +* Thu Jun 27 2019 Richard W.M. Jones - 4.8.5-2 +- OCaml 4.08.0 (final) rebuild. + +* Sat Jun 22 2019 Jerry James - 4.8.5-1 +- New upstream version + +* Mon Apr 29 2019 Richard W.M. Jones - 4.8.4-3 +- OCaml 4.08.0 (beta 3) rebuild. + +* Sun Feb 03 2019 Fedora Release Engineering - 4.8.4-2 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_30_Mass_Rebuild + +* Mon Dec 24 2018 Jerry James - 4.8.4-1 +- New upstream version +- Drop -no-sse patch, now handled upstream + +* Wed Nov 28 2018 Jerry James - 4.8.3-1 +- New upstream version + +* Tue Oct 30 2018 Jerry James - 4.8.1-1 +- New upstream version +- Drop python2 subpackage (bz 1634981) + +* Fri Sep 7 2018 Jerry James - 4.7.1-5 +- Build with SSE2 support on 32-bit x86 + +* Sat Jul 14 2018 Fedora Release Engineering - 4.7.1-5 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_29_Mass_Rebuild + +* Wed Jul 11 2018 Richard W.M. Jones - 4.7.1-4 +- OCaml 4.07.0 (final) rebuild. + +* Wed Jun 20 2018 Richard W.M. Jones - 4.7.1-3 +- OCaml 4.07.0-rc1 rebuild. + +* Tue Jun 19 2018 Miro Hrončok - 4.7.1-2 +- Rebuilt for Python 3.7 + +* Tue May 22 2018 Jerry James - 4.7.1-1 +- New upstream version (bz 1581516) +- Drop upstreamed -vector patch + +* Fri Feb 09 2018 Fedora Release Engineering - 4.6.0-2 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_28_Mass_Rebuild + +* Sun Dec 24 2017 Jerry James - 4.6.0-1 +- New upstream version (bz 1527531) +- Add a python3 subpackage + +* Sun Dec 17 2017 Zbigniew Jędrzejewski-Szmek - 4.5.0-8 +- Python 2 binary package renamed to python2-z3 + See https://fedoraproject.org/wiki/FinalizingFedoraSwitchtoPython3 + +* Fri Nov 17 2017 Richard W.M. Jones - 4.5.0-7 +- OCaml 4.06.0 rebuild. +- Add dependency on ocaml-num. + +* Tue Aug 08 2017 Richard W.M. Jones - 4.5.0-6 +- OCaml 4.05.0 rebuild. + +* Thu Jul 27 2017 Fedora Release Engineering - 4.5.0-5 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_27_Mass_Rebuild + +* Tue Jun 27 2017 Richard W.M. Jones - 4.5.0-4 +- OCaml 4.04.2 rebuild. + +* Fri May 12 2017 Richard W.M. Jones - 4.5.0-3 +- OCaml 4.04.1 rebuild. + +* Sat Feb 11 2017 Fedora Release Engineering - 4.5.0-2 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_26_Mass_Rebuild + +* Tue Nov 8 2016 Jerry James - 4.5.0-1 +- New upstream version +- All patches except -sse2 have been upstreamed; drop them +- Upstream now ships __init__.py; drop our version +- Drop all the buildroot tricks; Makefile supports DESTDIR now +- Use C.UTF-8 instead of en_US.UTF-8 + +* Sat Nov 05 2016 Richard W.M. Jones - 4.4.1-8 +- Rebuild for OCaml 4.04.0. + +* Tue Jul 19 2016 Fedora Release Engineering - 4.4.1-7 +- https://fedoraproject.org/wiki/Changes/Automatic_Provides_for_Python_RPM_Packages + +* Wed Jul 13 2016 Jerry James - 4.4.1-6 +- Fix Java interface (bz 1353773) + +* Thu Jun 30 2016 Jerry James - 4.4.1-5 +- Fix __init__.py (bz 1351580) + +* Fri Feb 05 2016 Fedora Release Engineering - 4.4.1-4 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_24_Mass_Rebuild + +* Tue Feb 02 2016 Jonathan Wakely - 4.4.1-3 +- Patched for C++11 compatibility. + +* Wed Jan 20 2016 Jerry James - 4.4.1-2 +- Add __init__.py to the python interface (bz 1298429) + +* Thu Oct 8 2015 Jerry James - 4.4.1-1 +- New upstream version + +* Tue Jul 28 2015 Richard W.M. Jones - 4.4.0-4 +- OCaml 4.02.3 rebuild. + +* Thu Jun 25 2015 Richard W.M. Jones - 4.4.0-3 +- ocaml-4.02.2 final rebuild. + +* Thu Jun 18 2015 Richard W.M. Jones - 4.4.0-2 +- ocaml-4.02.2 rebuild. + +* Wed May 27 2015 Jerry James - 4.4.0-1 +- New upstream version + +* Wed Apr 22 2015 Jerry James - 4.3.2-3.20150329git.29606b5 +- Fix issues found on review (bz 1206826) + +* Mon Mar 30 2015 Jerry James - 4.3.2-2.20150329git.29606b5 +- Update to latest git HEAD +- Include examples in -doc + +* Sat Mar 28 2015 Jerry James - 4.3.2-1.20150327git.ac21ffe +- Initial RPM diff --git a/z3.spec b/z3.spec index d6a7651..7ced9f4 100644 --- a/z3.spec +++ b/z3.spec @@ -15,7 +15,7 @@ Name: z3 Version: 4.13.0 -Release: 6%{?dist} +Release: %autorelease Summary: Satisfiability Modulo Theories (SMT) solver License: MIT @@ -313,390 +313,4 @@ cd - %{python3_sitelib}/z3/ %changelog -* Sat Jul 20 2024 Fedora Release Engineering - 4.13.0-6 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_41_Mass_Rebuild - -* Tue Jul 16 2024 Jerry James - 4.13.0-5 -- Rebuild for ocaml-zarith 1.14 - -* Wed Jun 19 2024 Richard W.M. Jones - 4.13.0-4 -- OCaml 5.2.0 ppc64le fix - -* Fri Jun 07 2024 Python Maint - 4.13.0-3 -- Rebuilt for Python 3.13 - -* Wed May 29 2024 Richard W.M. Jones - 4.13.0-2 -- OCaml 5.2.0 for Fedora 41 - -* Thu Mar 14 2024 Jerry James - 4.13.0-1 -- Version 4.13.0 - -* Sun Feb 25 2024 Jerry James - 4.12.6-1 -- Version 4.12.6 - -* Sat Jan 27 2024 Jerry James - 4.12.5-1 -- Version 4.12.5 - -* Sat Jan 27 2024 Fedora Release Engineering - 4.12.4-5 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_40_Mass_Rebuild - -* Thu Dec 21 2023 Jerry James - 4.12.4-4 -- Fix python package library load name (bz 2255464) - -* Mon Dec 18 2023 Richard W.M. Jones - 4.12.4-3 -- OCaml 5.1.1 + s390x code gen fix for Fedora 40 - -* Tue Dec 12 2023 Richard W.M. Jones - 4.12.4-2 -- OCaml 5.1.1 rebuild for Fedora 40 - -* Sat Dec 9 2023 Jerry James - 4.12.4-1 -- Version 4.12.4 -- Drop upstreamed patches: python, stdint, escapes - -* Thu Oct 05 2023 Richard W.M. Jones - 4.12.2-7 -- OCaml 5.1 rebuild for Fedora 40 - -* Thu Jul 27 2023 Jerry James - 4.12.2-6 -- Rebuild for ocaml-zarith 1.13 - -* Sat Jul 22 2023 Fedora Release Engineering - 4.12.2-5 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_39_Mass_Rebuild - -* Fri Jul 21 2023 Jerry James - 4.12.2-4 -- Exclude the OCaml and Java subpackages only on i386 - -* Wed Jul 12 2023 Richard W.M. Jones - 4.12.2-4 -- OCaml 5.0 rebuild for Fedora 39 - -* Mon Jul 10 2023 Jerry James - 4.12.2-3 -- OCaml 5.0.0 rebuild - -* Thu Jun 15 2023 Python Maint - 4.12.2-2 -- Rebuilt for Python 3.12 - -* Mon May 15 2023 Jerry James - 4.12.2-1 -- Version 4.12.2 - -* Tue Jan 24 2023 Richard W.M. Jones - 4.12.1-2 -- Rebuild OCaml packages for F38 - -* Sat Jan 21 2023 Jerry James - 4.12.1-1 -- Version 4.12.1 - -* Sat Jan 21 2023 Fedora Release Engineering - 4.12.0-2 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_38_Mass_Rebuild - -* Tue Jan 17 2023 Jerry James - 4.12.0-1 -- Version 4.12.0 -- Drop upstreamed -data-race and -uninit patches - -* Sun Jan 8 2023 Jerry James - 4.11.2-2 -- Add -data-race patch to fix segfault (bz 2157972) -- Add -uninit patch to fix use of an uninitialized value - -* Wed Dec 14 2022 Jerry James - 4.11.2-1 -- Further clarify license of the doc subpackage (SPDX) - -* Sun Sep 4 2022 Jerry James - 4.11.2-1 -- Version 4.11.2 - -* Fri Aug 19 2022 Jerry James - 4.11.0-1 -- Version 4.11.0 -- Clarify license of the doc subpackage - -* Mon Aug 8 2022 Jerry James - 4.10.2-1 -- Version 4.10.2 - -* Sat Jul 23 2022 Fedora Release Engineering - 4.8.17-6 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_37_Mass_Rebuild - -* Tue Jun 28 2022 Jerry James - 4.8.17-5 -- Do not support Java on i686 (rhbz#2104112) -- Use new OCaml macros - -* Mon Jun 20 2022 Python Maint - 4.8.17-4 -- Rebuilt for Python 3.11 - -* Sat Jun 18 2022 Richard W.M. Jones - 4.8.17-3 -- OCaml 4.14.0 rebuild - -* Mon Jun 13 2022 Python Maint - 4.8.17-2 -- Rebuilt for Python 3.11 - -* Mon May 16 2022 Jerry James - 4.8.17-1 -- Version 4.8.17 -- Drop upstreamed -ambiguous-overload patch - -* Thu Mar 24 2022 Jerry James - 4.8.15-2 -- Add -ambiguous-overload patch to fix cppcheck build failure - -* Mon Mar 21 2022 Jerry James - 4.8.15-1 -- Version 4.8.15 - -* Sat Feb 05 2022 Jiri Vanek - 4.8.14-4 -- Rebuilt for java-17-openjdk as system jdk - -* Fri Feb 04 2022 Richard W.M. Jones - 4.8.14-3 -- OCaml 4.13.1 rebuild to remove package notes - -* Sat Jan 22 2022 Fedora Release Engineering - 4.8.14-2 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_36_Mass_Rebuild - -* Fri Dec 24 2021 Jerry James - 4.8.14-1 -- Version 4.8.14 -- Conditionalize the %%check script - -* Fri Nov 19 2021 Jerry James - 4.8.13-1 -- Version 4.8.13 - -* Mon Oct 04 2021 Richard W.M. Jones - 4.8.12-3 -- OCaml 4.13.1 build - -* Fri Jul 23 2021 Fedora Release Engineering - 4.8.12-2 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_35_Mass_Rebuild - -* Tue Jul 13 2021 Jerry James - 4.8.12-1 -- Version 4.8.12 - -* Sun Jun 6 2021 Jerry James - 4.8.11-1 -- Version 4.8.11 - -* Fri Jun 04 2021 Python Maint - 4.8.10-6 -- Rebuilt for Python 3.10 - -* Wed Mar 3 2021 Jerry James - 4.8.10-5 -- Rebuild for ocaml-zarith 1.12 - -* Mon Mar 1 20:17:48 GMT 2021 Richard W.M. Jones - 4.8.10-4 -- Bump release and rebuild. - -* Mon Mar 1 19:41:16 GMT 2021 Richard W.M. Jones - 4.8.10-3 -- Bump release and rebuild. - -* Mon Mar 1 16:57:45 GMT 2021 Richard W.M. Jones - 4.8.10-2 -- OCaml 4.12.0 build - -* Sat Feb 13 2021 Jerry James - 4.8.10-1 -- Version 4.8.10 - -* Thu Jan 28 2021 Fedora Release Engineering - 4.8.9-5 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_34_Mass_Rebuild - -* Fri Dec 25 2020 Jerry James - 4.8.9-4 -- Fix the python interface (bz 1910923) - -* Mon Nov 16 2020 Jerry James - 4.8.9-3 -- Rebuild for ocaml-zarith 1.11 - -* Fri Sep 25 2020 Jerry James - 4.8.9-2 -- Rebuild for ocaml-zarith 1.10 - -* Fri Sep 11 2020 Jerry James - 4.8.9-1 -- Version 4.8.9 - -* Tue Sep 01 2020 Richard W.M. Jones - 4.8.8-7 -- OCaml 4.11.1 rebuild - -* Fri Aug 21 2020 Richard W.M. Jones - 4.8.8-6 -- OCaml 4.11.0 rebuild - -* Wed Jul 29 2020 Fedora Release Engineering - 4.8.8-5 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_33_Mass_Rebuild - -* Mon Jul 27 2020 Jerry James - 4.8.8-4 -- Build with cmake -- Manually build the OCaml interface -- Limit the class file version in the Java interface -- Allow the library to hide internal symbols; this means that the binary can no - longer be linked with the library, so the main package does not depend on - the -libs package -- The python package no longer contains an ELF object, so make it noarch - -* Sat Jul 11 2020 Jiri Vanek - 4.8.8-4 -- Rebuilt for JDK-11, see https://fedoraproject.org/wiki/Changes/Java11 - -* Tue May 26 2020 Miro Hrončok - 4.8.8-3 -- Rebuilt for Python 3.9 - -* Thu May 14 2020 Wolfgang Stöggl - 4.8.8-2 -- Add Z3 cmake files required by find_package(Z3) - -* Sat May 9 2020 Jerry James - 4.8.8-1 -- Version 4.8.8 -- Drop all patches; all have been upstreamed - -* Mon May 04 2020 Richard W.M. Jones - 4.8.7-10 -- OCaml 4.11.0+dev2-2020-04-22 rebuild - -* Tue Apr 21 2020 Richard W.M. Jones - 4.8.7-9 -- OCaml 4.11.0 pre-release attempt 2 - -* Fri Apr 17 2020 Richard W.M. Jones - 4.8.7-8 -- OCaml 4.11.0 pre-release - -* Thu Apr 02 2020 Richard W.M. Jones - 4.8.7-7 -- Update all OCaml dependencies for RPM 4.16. - -* Wed Feb 26 2020 Richard W.M. Jones - 4.8.7-6 -- OCaml 4.10.0 final. - -* Fri Jan 31 2020 Fedora Release Engineering - 4.8.7-5 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_32_Mass_Rebuild - -* Tue Jan 21 2020 Jerry James - 4.8.7-4 -- Make -doc be archful (bz 1792740) -- Add -signed-char and -gcc-10-s390x patches - -* Sun Jan 19 2020 Richard W.M. Jones - 4.8.7-4 -- OCaml 4.10.0+beta1 rebuild. - -* Fri Jan 10 2020 Richard W.M. Jones - 4.8.7-3 -- OCaml 4.09.0 for riscv64 - -* Sat Dec 7 2019 Jerry James - 4.8.7-2 -- OCaml 4.09.0 (final) rebuild - -* Thu Nov 21 2019 Jerry James - 4.8.7-1 -- New upstream version -- Add -ocamldoc patch to fix documentation build failure -- Add -trailing-zeros32 patch to fix build failures on some platforms - -* Fri Sep 20 2019 Jerry James - 4.8.6-1 -- New upstream version - -* Mon Aug 19 2019 Miro Hrončok - 4.8.5-6 -- Rebuilt for Python 3.8 - -* Fri Aug 16 2019 Richard W.M. Jones - 4.8.5-5 -- OCaml 4.08.1 (final) rebuild. - -* Wed Jul 31 2019 Richard W.M. Jones - 4.8.5-4 -- OCaml 4.08.1 (rc2) rebuild. - -* Sat Jul 27 2019 Fedora Release Engineering - 4.8.5-3 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_31_Mass_Rebuild - -* Thu Jun 27 2019 Richard W.M. Jones - 4.8.5-2 -- OCaml 4.08.0 (final) rebuild. - -* Sat Jun 22 2019 Jerry James - 4.8.5-1 -- New upstream version - -* Mon Apr 29 2019 Richard W.M. Jones - 4.8.4-3 -- OCaml 4.08.0 (beta 3) rebuild. - -* Sun Feb 03 2019 Fedora Release Engineering - 4.8.4-2 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_30_Mass_Rebuild - -* Mon Dec 24 2018 Jerry James - 4.8.4-1 -- New upstream version -- Drop -no-sse patch, now handled upstream - -* Wed Nov 28 2018 Jerry James - 4.8.3-1 -- New upstream version - -* Tue Oct 30 2018 Jerry James - 4.8.1-1 -- New upstream version -- Drop python2 subpackage (bz 1634981) - -* Fri Sep 7 2018 Jerry James - 4.7.1-5 -- Build with SSE2 support on 32-bit x86 - -* Sat Jul 14 2018 Fedora Release Engineering - 4.7.1-5 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_29_Mass_Rebuild - -* Wed Jul 11 2018 Richard W.M. Jones - 4.7.1-4 -- OCaml 4.07.0 (final) rebuild. - -* Wed Jun 20 2018 Richard W.M. Jones - 4.7.1-3 -- OCaml 4.07.0-rc1 rebuild. - -* Tue Jun 19 2018 Miro Hrončok - 4.7.1-2 -- Rebuilt for Python 3.7 - -* Tue May 22 2018 Jerry James - 4.7.1-1 -- New upstream version (bz 1581516) -- Drop upstreamed -vector patch - -* Fri Feb 09 2018 Fedora Release Engineering - 4.6.0-2 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_28_Mass_Rebuild - -* Sun Dec 24 2017 Jerry James - 4.6.0-1 -- New upstream version (bz 1527531) -- Add a python3 subpackage - -* Sun Dec 17 2017 Zbigniew Jędrzejewski-Szmek - 4.5.0-8 -- Python 2 binary package renamed to python2-z3 - See https://fedoraproject.org/wiki/FinalizingFedoraSwitchtoPython3 - -* Fri Nov 17 2017 Richard W.M. Jones - 4.5.0-7 -- OCaml 4.06.0 rebuild. -- Add dependency on ocaml-num. - -* Tue Aug 08 2017 Richard W.M. Jones - 4.5.0-6 -- OCaml 4.05.0 rebuild. - -* Thu Jul 27 2017 Fedora Release Engineering - 4.5.0-5 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_27_Mass_Rebuild - -* Tue Jun 27 2017 Richard W.M. Jones - 4.5.0-4 -- OCaml 4.04.2 rebuild. - -* Fri May 12 2017 Richard W.M. Jones - 4.5.0-3 -- OCaml 4.04.1 rebuild. - -* Sat Feb 11 2017 Fedora Release Engineering - 4.5.0-2 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_26_Mass_Rebuild - -* Tue Nov 8 2016 Jerry James - 4.5.0-1 -- New upstream version -- All patches except -sse2 have been upstreamed; drop them -- Upstream now ships __init__.py; drop our version -- Drop all the buildroot tricks; Makefile supports DESTDIR now -- Use C.UTF-8 instead of en_US.UTF-8 - -* Sat Nov 05 2016 Richard W.M. Jones - 4.4.1-8 -- Rebuild for OCaml 4.04.0. - -* Tue Jul 19 2016 Fedora Release Engineering - 4.4.1-7 -- https://fedoraproject.org/wiki/Changes/Automatic_Provides_for_Python_RPM_Packages - -* Wed Jul 13 2016 Jerry James - 4.4.1-6 -- Fix Java interface (bz 1353773) - -* Thu Jun 30 2016 Jerry James - 4.4.1-5 -- Fix __init__.py (bz 1351580) - -* Fri Feb 05 2016 Fedora Release Engineering - 4.4.1-4 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_24_Mass_Rebuild - -* Tue Feb 02 2016 Jonathan Wakely - 4.4.1-3 -- Patched for C++11 compatibility. - -* Wed Jan 20 2016 Jerry James - 4.4.1-2 -- Add __init__.py to the python interface (bz 1298429) - -* Thu Oct 8 2015 Jerry James - 4.4.1-1 -- New upstream version - -* Tue Jul 28 2015 Richard W.M. Jones - 4.4.0-4 -- OCaml 4.02.3 rebuild. - -* Thu Jun 25 2015 Richard W.M. Jones - 4.4.0-3 -- ocaml-4.02.2 final rebuild. - -* Thu Jun 18 2015 Richard W.M. Jones - 4.4.0-2 -- ocaml-4.02.2 rebuild. - -* Wed May 27 2015 Jerry James - 4.4.0-1 -- New upstream version - -* Wed Apr 22 2015 Jerry James - 4.3.2-3.20150329git.29606b5 -- Fix issues found on review (bz 1206826) - -* Mon Mar 30 2015 Jerry James - 4.3.2-2.20150329git.29606b5 -- Update to latest git HEAD -- Include examples in -doc - -* Sat Mar 28 2015 Jerry James - 4.3.2-1.20150327git.ac21ffe -- Initial RPM +%autochangelog From 1e3e9c860286ce80bd3813c98487780bde42e246 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Fri, 27 Sep 2024 17:24:36 -0600 Subject: [PATCH 64/94] Version 4.13.2 --- sources | 2 +- z3.spec | 7 +------ 2 files changed, 2 insertions(+), 7 deletions(-) diff --git a/sources b/sources index 5cc3163..56c4eb0 100644 --- a/sources +++ b/sources @@ -1 +1 @@ -SHA512 (z3-4.13.0.tar.gz) = 8503787fe0b18592b5a131bcec2cacfa5f5096d76386a1c4fda7a836e472924b154433306d27600ff0d0758ddb710c965901fbfc2e5605919b624b9d4d1bc4fd +SHA512 (z3-4.13.2.tar.gz) = 211a855ad2313aacbef67ccad9e02f4d8012ce015880383faefaae2e78785efbc167634f6c272d844dd04ba36c55a25192cae74bfd0c75a32588672ac8516e09 diff --git a/z3.spec b/z3.spec index 7ced9f4..fa6dc9c 100644 --- a/z3.spec +++ b/z3.spec @@ -14,7 +14,7 @@ %global giturl https://github.com/Z3Prover/z3 Name: z3 -Version: 4.13.0 +Version: 4.13.2 Release: %autorelease Summary: Satisfiability Modulo Theories (SMT) solver @@ -155,7 +155,6 @@ Python 3 interface to z3. %ifnarch %{ocaml_native_compiler} %patch -P0 -p1 %endif -%autopatch -m 1 -p1 # Enable verbose builds, use Fedora CFLAGS, preserve timestamps when installing, # include the entire contents of the archives in the library, link the library @@ -180,7 +179,6 @@ sed -e '/libz3java/s,\(System\.load\)Library("\(.*\)"),\1("%{_libdir}/z3/\2.so") sed -i '/HTML_TIMESTAMP/s/YES/NO/' doc/z3api.cfg.in doc/z3code.dox %build -export LANG=C.UTF-8 export PYTHON=%{python3} %cmake -G Ninja \ @@ -217,8 +215,6 @@ sed -i '/^api/s/ libz3\$(SO_EXT)//g' build/Makefile %endif %install -export LANG="C.UTF-8" - # Install the C++, python3, and Java interfaces %cmake_install @@ -257,7 +253,6 @@ sed -i 's,//usr,,' %{buildroot}%{_libdir}/pkgconfig/z3.pc %if %{with test} %check -export LANG="C.UTF-8" cd build make test-z3 ./test-z3 /a From 03af5cbb90315a70be8f7abd90004c7b3bb5ca81 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Fri, 11 Oct 2024 10:33:50 -0600 Subject: [PATCH 65/94] Version 4.13.3 --- sources | 2 +- z3.spec | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/sources b/sources index 56c4eb0..5d76ed9 100644 --- a/sources +++ b/sources @@ -1 +1 @@ -SHA512 (z3-4.13.2.tar.gz) = 211a855ad2313aacbef67ccad9e02f4d8012ce015880383faefaae2e78785efbc167634f6c272d844dd04ba36c55a25192cae74bfd0c75a32588672ac8516e09 +SHA512 (z3-4.13.3.tar.gz) = c899f57d8cb5450801463b07cd651869d766a920e41a4beedc96c4978e940bfadff9af2fbbb5ba10f94f6742bb33f7abaca0a351f3e1803d778e84d735d6829e diff --git a/z3.spec b/z3.spec index fa6dc9c..885ec05 100644 --- a/z3.spec +++ b/z3.spec @@ -14,7 +14,7 @@ %global giturl https://github.com/Z3Prover/z3 Name: z3 -Version: 4.13.2 +Version: 4.13.3 Release: %autorelease Summary: Satisfiability Modulo Theories (SMT) solver From d7781ac96b250c9cdb90b65324acace150ed4a46 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Fri, 27 Dec 2024 11:42:08 -0700 Subject: [PATCH 66/94] 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 67/94] 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 68/94] Rebuilt for https://fedoraproject.org/wiki/Fedora_42_Mass_Rebuild From b0d1169569a7096061218d382b5d6458d34f6982 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Tue, 4 Mar 2025 13:24:44 -0700 Subject: [PATCH 69/94] 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 70/94] 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 71/94] 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 72/94] 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 73/94] 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 74/94] 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 75/94] 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 76/94] 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 77/94] 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 78/94] 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 79/94] 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 80/94] 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 81/94] 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 82/94] 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 83/94] 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 84/94] 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 85/94] 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 86/94] 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 87/94] 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 88/94] 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 89/94] 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 90/94] 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 91/94] 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 92/94] 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 93/94] 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 94/94] 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/