Version 5.1.0

- Drop s390x doc workaround

.gitignore

@@ -1,2 +1,3 @@
 /z3-*.tar.gz
 /Z3-*.tar.gz
+/Z3_cmake_files.tar.gz

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).

changelog

@@ -0,0 +1,387 @@
+* Sat Jul 20 2024 Fedora Release Engineering <releng@fedoraproject.org> - 4.13.0-6
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_41_Mass_Rebuild
+
+* Tue Jul 16 2024 Jerry James <loganjerry@gmail.com> - 4.13.0-5
+- Rebuild for ocaml-zarith 1.14
+
+* Wed Jun 19 2024 Richard W.M. Jones <rjones@redhat.com> - 4.13.0-4
+- OCaml 5.2.0 ppc64le fix
+
+* Fri Jun 07 2024 Python Maint <python-maint@redhat.com> - 4.13.0-3
+- Rebuilt for Python 3.13
+
+* Wed May 29 2024 Richard W.M. Jones <rjones@redhat.com> - 4.13.0-2
+- OCaml 5.2.0 for Fedora 41
+
+* Thu Mar 14 2024 Jerry James <loganjerry@gmail.com> - 4.13.0-1
+- Version 4.13.0
+
+* Sun Feb 25 2024 Jerry James <loganjerry@gmail.com> - 4.12.6-1
+- Version 4.12.6
+
+* Sat Jan 27 2024 Jerry James <loganjerry@gmail.com> - 4.12.5-1
+- Version 4.12.5
+
+* Sat Jan 27 2024 Fedora Release Engineering <releng@fedoraproject.org> - 4.12.4-5
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_40_Mass_Rebuild
+
+* Thu Dec 21 2023 Jerry James <loganjerry@gmail.com> - 4.12.4-4
+- Fix python package library load name (bz 2255464)
+
+* Mon Dec 18 2023 Richard W.M. Jones <rjones@redhat.com> - 4.12.4-3
+- OCaml 5.1.1 + s390x code gen fix for Fedora 40
+
+* Tue Dec 12 2023 Richard W.M. Jones <rjones@redhat.com> - 4.12.4-2
+- OCaml 5.1.1 rebuild for Fedora 40
+
+* Sat Dec  9 2023 Jerry James <loganjerry@gmail.com> - 4.12.4-1
+- Version 4.12.4
+- Drop upstreamed patches: python, stdint, escapes
+
+* Thu Oct 05 2023 Richard W.M. Jones <rjones@redhat.com> - 4.12.2-7
+- OCaml 5.1 rebuild for Fedora 40
+
+* Thu Jul 27 2023 Jerry James <loganjerry@gmail.com> - 4.12.2-6
+- Rebuild for ocaml-zarith 1.13
+
+* Sat Jul 22 2023 Fedora Release Engineering <releng@fedoraproject.org> - 4.12.2-5
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_39_Mass_Rebuild
+
+* Fri Jul 21 2023 Jerry James <loganjerry@gmail.com> - 4.12.2-4
+- Exclude the OCaml and Java subpackages only on i386
+
+* Wed Jul 12 2023 Richard W.M. Jones <rjones@redhat.com> - 4.12.2-4
+- OCaml 5.0 rebuild for Fedora 39
+
+* Mon Jul 10 2023 Jerry James <loganjerry@gmail.com> - 4.12.2-3
+- OCaml 5.0.0 rebuild
+
+* Thu Jun 15 2023 Python Maint <python-maint@redhat.com> - 4.12.2-2
+- Rebuilt for Python 3.12
+
+* Mon May 15 2023 Jerry James <loganjerry@gmail.com> - 4.12.2-1
+- Version 4.12.2
+
+* Tue Jan 24 2023 Richard W.M. Jones <rjones@redhat.com> - 4.12.1-2
+- Rebuild OCaml packages for F38
+
+* Sat Jan 21 2023 Jerry James <loganjerry@gmail.com> - 4.12.1-1
+- Version 4.12.1
+
+* Sat Jan 21 2023 Fedora Release Engineering <releng@fedoraproject.org> - 4.12.0-2
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_38_Mass_Rebuild
+
+* Tue Jan 17 2023 Jerry James <loganjerry@gmail.com> - 4.12.0-1
+- Version 4.12.0
+- Drop upstreamed -data-race and -uninit patches
+
+* Sun Jan  8 2023 Jerry James <loganjerry@gmail.com> - 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 <loganjerry@gmail.com> - 4.11.2-1
+- Further clarify license of the doc subpackage (SPDX)
+
+* Sun Sep  4 2022 Jerry James <loganjerry@gmail.com> - 4.11.2-1
+- Version 4.11.2
+
+* Fri Aug 19 2022 Jerry James <loganjerry@gmail.com> - 4.11.0-1
+- Version 4.11.0
+- Clarify license of the doc subpackage
+
+* Mon Aug  8 2022 Jerry James <loganjerry@gmail.com> - 4.10.2-1
+- Version 4.10.2
+
+* Sat Jul 23 2022 Fedora Release Engineering <releng@fedoraproject.org> - 4.8.17-6
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_37_Mass_Rebuild
+
+* Tue Jun 28 2022 Jerry James <loganjerry@gmail.com> - 4.8.17-5
+- Do not support Java on i686 (rhbz#2104112)
+- Use new OCaml macros
+
+* Mon Jun 20 2022 Python Maint <python-maint@redhat.com> - 4.8.17-4
+- Rebuilt for Python 3.11
+
+* Sat Jun 18 2022 Richard W.M. Jones <rjones@redhat.com> - 4.8.17-3
+- OCaml 4.14.0 rebuild
+
+* Mon Jun 13 2022 Python Maint <python-maint@redhat.com> - 4.8.17-2
+- Rebuilt for Python 3.11
+
+* Mon May 16 2022 Jerry James <loganjerry@gmail.com> - 4.8.17-1
+- Version 4.8.17
+- Drop upstreamed -ambiguous-overload patch
+
+* Thu Mar 24 2022 Jerry James <loganjerry@gmail.com> - 4.8.15-2
+- Add -ambiguous-overload patch to fix cppcheck build failure
+
+* Mon Mar 21 2022 Jerry James <loganjerry@gmail.com> - 4.8.15-1
+- Version 4.8.15
+
+* Sat Feb 05 2022 Jiri Vanek <jvanek@redhat.com> - 4.8.14-4
+- Rebuilt for java-17-openjdk as system jdk
+
+* Fri Feb 04 2022 Richard W.M. Jones <rjones@redhat.com> - 4.8.14-3
+- OCaml 4.13.1 rebuild to remove package notes
+
+* Sat Jan 22 2022 Fedora Release Engineering <releng@fedoraproject.org> - 4.8.14-2
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_36_Mass_Rebuild
+
+* Fri Dec 24 2021 Jerry James <loganjerry@gmail.com> - 4.8.14-1
+- Version 4.8.14
+- Conditionalize the %%check script
+
+* Fri Nov 19 2021 Jerry James <loganjerry@gmail.com> - 4.8.13-1
+- Version 4.8.13
+
+* Mon Oct 04 2021 Richard W.M. Jones <rjones@redhat.com> - 4.8.12-3
+- OCaml 4.13.1 build
+
+* Fri Jul 23 2021 Fedora Release Engineering <releng@fedoraproject.org> - 4.8.12-2
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_35_Mass_Rebuild
+
+* Tue Jul 13 2021 Jerry James <loganjerry@gmail.com> - 4.8.12-1
+- Version 4.8.12
+
+* Sun Jun  6 2021 Jerry James <loganjerry@gmail.com> - 4.8.11-1
+- Version 4.8.11
+
+* Fri Jun 04 2021 Python Maint <python-maint@redhat.com> - 4.8.10-6
+- Rebuilt for Python 3.10
+
+* Wed Mar  3 2021 Jerry James <loganjerry@gmail.com> - 4.8.10-5
+- Rebuild for ocaml-zarith 1.12
+
+* Mon Mar  1 20:17:48 GMT 2021 Richard W.M. Jones <rjones@redhat.com> - 4.8.10-4
+- Bump release and rebuild.
+
+* Mon Mar  1 19:41:16 GMT 2021 Richard W.M. Jones <rjones@redhat.com> - 4.8.10-3
+- Bump release and rebuild.
+
+* Mon Mar  1 16:57:45 GMT 2021 Richard W.M. Jones <rjones@redhat.com> - 4.8.10-2
+- OCaml 4.12.0 build
+
+* Sat Feb 13 2021 Jerry James <loganjerry@gmail.com> - 4.8.10-1
+- Version 4.8.10
+
+* Thu Jan 28 2021 Fedora Release Engineering <releng@fedoraproject.org> - 4.8.9-5
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_34_Mass_Rebuild
+
+* Fri Dec 25 2020 Jerry James <loganjerry@gmail.com> - 4.8.9-4
+- Fix the python interface (bz 1910923)
+
+* Mon Nov 16 2020 Jerry James <loganjerry@gmail.com> - 4.8.9-3
+- Rebuild for ocaml-zarith 1.11
+
+* Fri Sep 25 2020 Jerry James <loganjerry@gmail.com> - 4.8.9-2
+- Rebuild for ocaml-zarith 1.10
+
+* Fri Sep 11 2020 Jerry James <loganjerry@gmail.com> - 4.8.9-1
+- Version 4.8.9
+
+* Tue Sep 01 2020 Richard W.M. Jones <rjones@redhat.com> - 4.8.8-7
+- OCaml 4.11.1 rebuild
+
+* Fri Aug 21 2020 Richard W.M. Jones <rjones@redhat.com> - 4.8.8-6
+- OCaml 4.11.0 rebuild
+
+* Wed Jul 29 2020 Fedora Release Engineering <releng@fedoraproject.org> - 4.8.8-5
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_33_Mass_Rebuild
+
+* Mon Jul 27 2020 Jerry James <loganjerry@gmail.com> - 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 <jvanek@redhat.com> - 4.8.8-4
+- Rebuilt for JDK-11, see https://fedoraproject.org/wiki/Changes/Java11
+
+* Tue May 26 2020 Miro Hrončok <mhroncok@redhat.com> - 4.8.8-3
+- Rebuilt for Python 3.9
+
+* Thu May 14 2020 Wolfgang Stöggl <c72578@yahoo.de> - 4.8.8-2
+- Add Z3 cmake files required by find_package(Z3)
+
+* Sat May  9 2020 Jerry James <loganjerry@gmail.com> - 4.8.8-1
+- Version 4.8.8
+- Drop all patches; all have been upstreamed
+
+* Mon May 04 2020 Richard W.M. Jones <rjones@redhat.com> - 4.8.7-10
+- OCaml 4.11.0+dev2-2020-04-22 rebuild
+
+* Tue Apr 21 2020 Richard W.M. Jones <rjones@redhat.com> - 4.8.7-9
+- OCaml 4.11.0 pre-release attempt 2
+
+* Fri Apr 17 2020 Richard W.M. Jones <rjones@redhat.com> - 4.8.7-8
+- OCaml 4.11.0 pre-release
+
+* Thu Apr 02 2020 Richard W.M. Jones <rjones@redhat.com> - 4.8.7-7
+- Update all OCaml dependencies for RPM 4.16.
+
+* Wed Feb 26 2020 Richard W.M. Jones <rjones@redhat.com> - 4.8.7-6
+- OCaml 4.10.0 final.
+
+* Fri Jan 31 2020 Fedora Release Engineering <releng@fedoraproject.org> - 4.8.7-5
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_32_Mass_Rebuild
+
+* Tue Jan 21 2020 Jerry James <loganjerry@gmail.com> - 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 <rjones@redhat.com> - 4.8.7-4
+- OCaml 4.10.0+beta1 rebuild.
+
+* Fri Jan 10 2020 Richard W.M. Jones <rjones@redhat.com> - 4.8.7-3
+- OCaml 4.09.0 for riscv64
+
+* Sat Dec  7 2019 Jerry James <loganjerry@gmail.com> - 4.8.7-2
+- OCaml 4.09.0 (final) rebuild
+
+* Thu Nov 21 2019 Jerry James <loganjerry@gmail.com> - 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 <loganjerry@gmail.com> - 4.8.6-1
+- New upstream version
+
+* Mon Aug 19 2019 Miro Hrončok <mhroncok@redhat.com> - 4.8.5-6
+- Rebuilt for Python 3.8
+
+* Fri Aug 16 2019 Richard W.M. Jones <rjones@redhat.com> - 4.8.5-5
+- OCaml 4.08.1 (final) rebuild.
+
+* Wed Jul 31 2019 Richard W.M. Jones <rjones@redhat.com> - 4.8.5-4
+- OCaml 4.08.1 (rc2) rebuild.
+
+* Sat Jul 27 2019 Fedora Release Engineering <releng@fedoraproject.org> - 4.8.5-3
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_31_Mass_Rebuild
+
+* Thu Jun 27 2019 Richard W.M. Jones <rjones@redhat.com> - 4.8.5-2
+- OCaml 4.08.0 (final) rebuild.
+
+* Sat Jun 22 2019 Jerry James <loganjerry@gmail.com> - 4.8.5-1
+- New upstream version
+
+* Mon Apr 29 2019 Richard W.M. Jones <rjones@redhat.com> - 4.8.4-3
+- OCaml 4.08.0 (beta 3) rebuild.
+
+* Sun Feb 03 2019 Fedora Release Engineering <releng@fedoraproject.org> - 4.8.4-2
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_30_Mass_Rebuild
+
+* Mon Dec 24 2018 Jerry James <loganjerry@gmail.com> - 4.8.4-1
+- New upstream version
+- Drop -no-sse patch, now handled upstream
+
+* Wed Nov 28 2018 Jerry James <loganjerry@gmail.com> - 4.8.3-1
+- New upstream version
+
+* Tue Oct 30 2018 Jerry James <loganjerry@gmail.com> - 4.8.1-1
+- New upstream version
+- Drop python2 subpackage (bz 1634981)
+
+* Fri Sep  7 2018 Jerry James <loganjerry@gmail.com> - 4.7.1-5
+- Build with SSE2 support on 32-bit x86
+
+* Sat Jul 14 2018 Fedora Release Engineering <releng@fedoraproject.org> - 4.7.1-5
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_29_Mass_Rebuild
+
+* Wed Jul 11 2018 Richard W.M. Jones <rjones@redhat.com> - 4.7.1-4
+- OCaml 4.07.0 (final) rebuild.
+
+* Wed Jun 20 2018 Richard W.M. Jones <rjones@redhat.com> - 4.7.1-3
+- OCaml 4.07.0-rc1 rebuild.
+
+* Tue Jun 19 2018 Miro Hrončok <mhroncok@redhat.com> - 4.7.1-2
+- Rebuilt for Python 3.7
+
+* Tue May 22 2018 Jerry James <loganjerry@gmail.com> - 4.7.1-1
+- New upstream version (bz 1581516)
+- Drop upstreamed -vector patch
+
+* Fri Feb 09 2018 Fedora Release Engineering <releng@fedoraproject.org> - 4.6.0-2
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_28_Mass_Rebuild
+
+* Sun Dec 24 2017 Jerry James <loganjerry@gmail.com> - 4.6.0-1
+- New upstream version (bz 1527531)
+- Add a python3 subpackage
+
+* Sun Dec 17 2017 Zbigniew Jędrzejewski-Szmek <zbyszek@in.waw.pl> - 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 <rjones@redhat.com> - 4.5.0-7
+- OCaml 4.06.0 rebuild.
+- Add dependency on ocaml-num.
+
+* Tue Aug 08 2017 Richard W.M. Jones <rjones@redhat.com> - 4.5.0-6
+- OCaml 4.05.0 rebuild.
+
+* Thu Jul 27 2017 Fedora Release Engineering <releng@fedoraproject.org> - 4.5.0-5
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_27_Mass_Rebuild
+
+* Tue Jun 27 2017 Richard W.M. Jones <rjones@redhat.com> - 4.5.0-4
+- OCaml 4.04.2 rebuild.
+
+* Fri May 12 2017 Richard W.M. Jones <rjones@redhat.com> - 4.5.0-3
+- OCaml 4.04.1 rebuild.
+
+* Sat Feb 11 2017 Fedora Release Engineering <releng@fedoraproject.org> - 4.5.0-2
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_26_Mass_Rebuild
+
+* Tue Nov  8 2016 Jerry James <loganjerry@gmail.com> - 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 <rjones@redhat.com> - 4.4.1-8
+- Rebuild for OCaml 4.04.0.
+
+* Tue Jul 19 2016 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 4.4.1-7
+- https://fedoraproject.org/wiki/Changes/Automatic_Provides_for_Python_RPM_Packages
+
+* Wed Jul 13 2016 Jerry James <loganjerry@gmail.com> - 4.4.1-6
+- Fix Java interface (bz 1353773)
+
+* Thu Jun 30 2016 Jerry James <loganjerry@gmail.com> - 4.4.1-5
+- Fix __init__.py (bz 1351580)
+
+* Fri Feb 05 2016 Fedora Release Engineering <releng@fedoraproject.org> - 4.4.1-4
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_24_Mass_Rebuild
+
+* Tue Feb 02 2016 Jonathan Wakely <jwakely@redhat.com> - 4.4.1-3
+- Patched for C++11 compatibility.
+
+* Wed Jan 20 2016 Jerry James <loganjerry@gmail.com> - 4.4.1-2
+- Add __init__.py to the python interface (bz 1298429)
+
+* Thu Oct  8 2015 Jerry James <loganjerry@gmail.com> - 4.4.1-1
+- New upstream version
+
+* Tue Jul 28 2015 Richard W.M. Jones <rjones@redhat.com> - 4.4.0-4
+- OCaml 4.02.3 rebuild.
+
+* Thu Jun 25 2015 Richard W.M. Jones <rjones@redhat.com> - 4.4.0-3
+- ocaml-4.02.2 final rebuild.
+
+* Thu Jun 18 2015 Richard W.M. Jones <rjones@redhat.com> - 4.4.0-2
+- ocaml-4.02.2 rebuild.
+
+* Wed May 27 2015 Jerry James <loganjerry@gmail.com> - 4.4.0-1
+- New upstream version
+
+* Wed Apr 22 2015 Jerry James <loganjerry@gmail.com> - 4.3.2-3.20150329git.29606b5
+- Fix issues found on review (bz 1206826)
+
+* Mon Mar 30 2015 Jerry James <loganjerry@gmail.com> - 4.3.2-2.20150329git.29606b5
+- Update to latest git HEAD
+- Include examples in -doc
+
+* Sat Mar 28 2015 Jerry James <loganjerry@gmail.com> - 4.3.2-1.20150327git.ac21ffe
+- Initial RPM

sources

@@ -1 +1 @@
-SHA512 (z3-4.8.7.tar.gz) = 145e2b2f1fa4edd0917107c7e1d54d779c7ed85c48af2ce6def4c90d1c4db05f74c9657e173cedf48770589fbe484c97fa1923295271cd3792523ffc4f67ed0c
+SHA512 (z3-5.1.0.tar.gz) = 03a854f720a56484ab99b8a5517150f1c9106400f54ad758cfa58e3ee2f95e349396a64d4f527a5bb9ee37f10ad9ecfa1916d1f5c921f04089deda409374491b

z3-gcc-10-s390x.patch

@@ -1,12 +0,0 @@
-Add explicit template instantiation to work around an s390x problem:
-https://bugzilla.redhat.com/show_bug.cgi?id=1794127
-
---- a/src/util/lp/lp_primal_core_solver.cpp
-+++ b/src/util/lp/lp_primal_core_solver.cpp
-@@ -38,5 +38,6 @@ template void lp::lp_primal_core_solver<
- template bool lp::lp_primal_core_solver<lp::mpq, lp::mpq>::update_basis_and_x_tableau(int, int, lp::mpq const&);
- template bool lp::lp_primal_core_solver<double, double>::update_basis_and_x_tableau(int, int, double const&);
- template bool lp::lp_primal_core_solver<lp::mpq, lp::numeric_pair<lp::mpq> >::update_basis_and_x_tableau(int, int, lp::numeric_pair<lp::mpq> const&);
-+template void lp::lp_primal_core_solver<rational, lp::numeric_pair<rational> >::update_inf_cost_for_column_tableau(unsigned);
- 
- }

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')

z3-ocamldoc.patch

@@ -1,13 +0,0 @@
-diff --git a/doc/mk_api_doc.py b/doc/mk_api_doc.py
-index bfe865e06..7bcc1c017 100644
---- a/doc/mk_api_doc.py
-+++ b/doc/mk_api_doc.py
-@@ -317,7 +317,7 @@ try:
-     if ML_ENABLED:
-         ml_output_dir = os.path.join(OUTPUT_DIRECTORY, 'html', 'ml')
-         mk_dir(ml_output_dir)
--        if subprocess.call(['ocamldoc', '-html', '-d', ml_output_dir, '-sort', '-hide', 'Z3', '-I', '%s/api/ml' % BUILD_DIR, '%s/api/ml/z3enums.mli' % BUILD_DIR, '%s/api/ml/z3.mli' % BUILD_DIR]) != 0:
-+        if subprocess.call(['ocamldoc', '-html', '-d', ml_output_dir, '-sort', '-hide', 'Z3', '-I', '+zarith', '-I', '%s/api/ml' % BUILD_DIR, '%s/api/ml/z3enums.mli' % BUILD_DIR, '%s/api/ml/z3.mli' % BUILD_DIR]) != 0:
-             print("ERROR: ocamldoc failed.")
-             exit(1)
-         print("Generated ML/OCaml documentation.")

z3-signed-char.patch

@@ -1,11 +0,0 @@
---- a/src/parsers/util/scanner.cpp
-+++ b/src/parsers/util/scanner.cpp
-@@ -480,7 +480,7 @@ scanner::token scanner::scan() {
-             return read_number(ch, true);
-         case '#':
-             return read_bv_literal();
--        case -1:
-+        case static_cast<char>(-1):
-             m_state = EOF_TOKEN;
-             break;
-         default:

z3-trailing-zeros32.patch

@@ -1,13 +0,0 @@
-diff --git a/src/util/mpz.cpp b/src/util/mpz.cpp
-index a8190df1b..9c2d3d5ff 100644
---- a/src/util/mpz.cpp
-+++ b/src/util/mpz.cpp
-@@ -72,6 +72,8 @@ inline uint64_t _trailing_zeros64(uint64_t x) {
- 
- #if defined(_WINDOWS) && !defined(_M_ARM) && !defined(_M_ARM64)
- // _trailing_zeros32 already defined using intrinsics
-+#elif defined(__GNUC__)
-+// _trailing_zeros32 already defined using intrinsics
- #else
- inline uint32_t _trailing_zeros32(uint32_t x) {
-     uint32_t r = 0;

z3.rpmlintrc

@@ -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')

z3.spec

@@ -1,44 +1,73 @@
-%global medtag  30e7c225cd51
+# 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.
+
+# 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.8.7
-Release:        6%{?dist}
+Version:        5.1.0
+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
-Source0:        https://github.com/Z3Prover/z3/archive/%{name}-%{version}.tar.gz
-# https://github.com/Z3Prover/z3/pull/2730
-Patch0:         %{name}-ocamldoc.patch
-# https://github.com/Z3Prover/z3/commit/e212159f4e941c78fc03239e0884f2f0454f581f
-Patch1:         %{name}-trailing-zeros32.patch
-# Fix a place where char is assumed to be signed
-Patch2:         %{name}-signed-char.patch
-# https://bugzilla.redhat.com/show_bug.cgi?id=1794127
-Patch3:         %{name}-gcc-10-s390x.patch
+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
+
+# 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:  doxygen
 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
 BuildRequires:  ocaml-findlib
-BuildRequires:  ocaml-ocamldoc
 BuildRequires:  ocaml-zarith-devel
 BuildRequires:  python3-devel
-BuildRequires:  python3dist(setuptools)
-
-Requires:       %{name}-libs%{?_isa} = %{version}-%{release}
+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
@@ -47,341 +76,212 @@ 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
-Requires:       %{name}-libs%{?_isa} = %{version}-%{release}
+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.
+# 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
+# Other licenses are due to files installed by doxygen.
+# 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/jquery.js: MIT
+# html/navtree.css: GPL-1.0-or-later
+# html/search/search.css: GPL-1.0-or-later
+# html/search/search.js: MIT
+# 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.
 
-%package -n java-%{name}
+%ifarch %{java_arches}
+%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}
-%{?python_provide:%python_provide python3-%{name}}
+%package -n python3-z3
 Summary:        Python 3 interface to z3
-Requires:       %{name}-libs%{?_isa} = %{version}-%{release}
+BuildArch:      noarch
+Requires:       z3-libs = %{version}-%{release}
 
-%description -n python3-%{name}
+# Provide the PyPI name
+%py_provides python3-z3-solver
+
+%description -n python3-z3
 Python 3 interface to z3.
 
 %prep
-%autosetup -p1 -n %{name}-%{name}-%{version}
+%autosetup -N -n %{name}-%{name}-%{version}
+%ifnarch %{ocaml_native_compiler}
+%patch 0 -p1
+%endif
 
-# Install python objects into the right place, 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, don't hide library symbols needed by the executable, add a version to
-# the soname, and build the ocaml files with debug info.
-sed -e "s|^\(PYTHON_PACKAGE_DIR=\).*|\1'%{python3_sitearch}'|" \
+# 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.
+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|& $RPM_LD_FLAGS -Wl,--whole-archive|" \
-  -e 's/\(libz3$(SO_EXT)\)\(\\n\)/\1 -Wl,--no-whole-archive\2/' \
-  -e 's/ -fvisibility=hidden//' \
-  -e "s/\(soname,libz3\.so\)'/\1.0'/" \
+  -e "s/\(SLIBEXTRAFLAGS = '\)'/\1-Wl,--no-whole-archive'/" \
+  -e '/SLIBFLAGS/s|-shared|& %{build_ldflags} -Wl,--whole-archive|' \
+  -e 's/\(libz3$(SO_EXT)\)\( \$(SLINK\)/\1 -Wl,--no-whole-archive\2/' \
   -e "s/OCAML_FLAGS = ''/OCAML_FLAGS = '-g'/" \
   -i scripts/mk_util.py
 
-# Comply with the Java packaging guidelines
-sed -e '/catch/s,\(System\.load\)Library("\(.*\)"),\1("%{_libdir}/z3/\2.so"),' \
+# Comply with the Java packaging guidelines and fill in the version for python
+sed -e '/libz3java/s,\(System\.load\)Library("\(.*\)"),\1("%{_libdir}/z3/\2.so"),' \
+    -e "s/'so'/'so.%{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
+# Turn off HTML timestamps for reproducible builds
+sed -i '/HTML_TIMESTAMP/s/YES/NO/' doc/z3api.cfg.in doc/z3code.dox
 
-%build
-export CXXFLAGS="$RPM_OPT_FLAGS"
-export LANG="C.UTF-8"
-export PYTHON="%{__python3}"
+%build -p
+export PYTHON=%{python3}
 
-# This is NOT an autoconf-generated configure script.
-./configure -p %{_prefix} --githash=%{medtag} --gmp --java --ml --python
-# FIXME: intermittent build failures with %%{?_smp_mflags}
-make -C 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]+//' \
+    %{_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
 
-# The z3 binary is NOT linked with libz3, but instead has duplicate copies of a
-# lot of object files, so rebuild it.  But first, add library links.
-pushd build
-mv libz3.so libz3.so.0.0.0
-ln -s libz3.so.0.0.0 libz3.so.0
-ln -s libz3.so.0 libz3.so
-g++ $RPM_OPT_FLAGS -DNDEBUG -o z3 shell/*.o $RPM_LD_FLAGS -L. -lz3 -lgmp
-popd
-
-# Build the documentation
-pushd doc
-%{__python3} mk_api_doc.py --ml --no-dotnet
-popd
-
-%install
-export LANG="C.UTF-8"
-
-# Install the python3 interface
-make -C build install DESTDIR=%{buildroot}
-rm -f %{buildroot}%{python3_sitearch}/%{name}/lib/libz3.so
-ln -s %{_libdir}/libz3.so.0 %{buildroot}%{python3_sitearch}/%{name}/lib/libz3.so
-
-# On 64-bit systems, move the library to the right directory
-if [ "%{_libdir}" != "%{_prefix}/lib" ]; then
-  mkdir -p %{buildroot}%{_libdir}
-  mv %{buildroot}%{_prefix}/lib/libz3.so* %{buildroot}%{_libdir}
-fi
-
-# Make library links
-mv %{buildroot}%{_libdir}/libz3.so %{buildroot}%{_libdir}/libz3.so.0.0.0
-ln -s libz3.so.0.0.0 %{buildroot}%{_libdir}/libz3.so.0
-ln -s libz3.so.0 %{buildroot}%{_libdir}/libz3.so
-
-# Move the header files into their own directory
-mkdir -p %{buildroot}%{_includedir}/%{name}
-mv %{buildroot}%{_includedir}/*.h %{buildroot}%{_includedir}/%{name}
-
-# Move the Java interface to its correct location
-mkdir -p %{buildroot}%{_libdir}/%{name}
-mkdir -p %{buildroot}%{_jnidir}
-mv %{buildroot}%{_prefix}/lib/*.jar %{buildroot}%{_jnidir}
-ln -s %{_jnidir}/com.microsoft.z3.jar %{buildroot}%{_libdir}/%{name}
-mv %{buildroot}%{_prefix}/lib/lib%{name}java.so %{buildroot}%{_libdir}/%{name}
-
-#%%check
-# Some of the tests require more memory than the koji builders have available.
+# The cmake build system does not build the OCaml interface.  Do that manually.
 #
-#export LANG="C.UTF-8"
-#pushd build
-#make test-z3
-#./test-z3 /a
-#popd
+# First, run the configure script to generate several files.
+# This is NOT an autoconf-generated configure script.
+./configure -p %{_prefix} --gmp --ml
+
+# Second, to prevent make from rebuilding the entire library, copy the
+# cmake-built library to where make expects it.
+cp -dp %{_vpath_builddir}/libz3.so* build
+
+# Third, make wants to rebuild libz3.so since its dependencies do not exist.
+# Do selective Makefile surgery to prevent this.
+sed -i '/^api/s/ libz3\$(SO_EXT)//g' build/Makefile
+
+# Fourth, build the OCaml interface
+%make_build -C build ml
+
+%install -a
+%ifarch %{java_arches}
+# Move the Java interface to its correct location
+mkdir -p %{buildroot}%{_libdir}/z3
+mkdir -p %{buildroot}%{_jnidir}
+mv %{buildroot}%{_javadir}/*.jar %{buildroot}%{_jnidir}
+ln -s %{_jnidir}/com.microsoft.z3.jar %{buildroot}%{_libdir}/z3
+mv %{buildroot}%{_libdir}/libz3java.so %{buildroot}%{_libdir}/z3
+%endif
+
+# Install the OCaml interface
+cd build/api/ml
+mkdir -p %{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
+cd -
+
+# We handle the documentation files below
+rm -rf %{buildroot}%{_docdir}/Z3
+
+# Make a man page
+mkdir -p %{buildroot}%{_mandir}/man1
+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
+
+%check
+%if %{with test}
+cd build
+make test-z3
+./test-z3 /a
+cd -
+%endif
 
 %files
-%doc README.md RELEASE_NOTES
-%{_bindir}/%{name}
+%doc README.md RELEASE_NOTES.md
+%{_bindir}/z3
+%{_mandir}/man1/z3.1*
 
 %files libs
 %license LICENSE.txt
-%{_libdir}/lib%{name}.so.*
+%{_libdir}/libz3.so.5.1{,.*}
 
 %files devel
-%{_includedir}/%{name}/
-%{_libdir}/lib%{name}.so
+%{_includedir}/z3/
+%{_libdir}/libz3.so
+%{_libdir}/cmake/z3/
+%{_libdir}/pkgconfig/z3.pc
 
 %files doc
-%doc doc/api/html examples
+%doc %{_vpath_builddir}/doc/api/html examples
 %license LICENSE.txt
 
-%files -n java-%{name}
-%{_libdir}/%{name}/
+%ifarch %{java_arches}
+%files -n java-z3
+%{_libdir}/z3/
 %{_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/Z3/*.so
+%files -n ocaml-z3
+%dir %{ocamldir}/Z3/
+%{ocamldir}/Z3/META
+%{ocamldir}/Z3/*.cma
+%{ocamldir}/Z3/*.cmi
+%ifarch %{ocaml_native_compiler}
+%{ocamldir}/Z3/*.cmxs
+%endif
+%{ocamldir}/stublibs/dllz3ml.so
 
-%files -n ocaml-%{name}-devel
-%{_libdir}/ocaml/Z3/*.a
-%{_libdir}/ocaml/Z3/*.cmx
-%{_libdir}/ocaml/Z3/*.cmxa
-%{_libdir}/ocaml/Z3/*.mli
+%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-%{name}
-%{python3_sitearch}/%{name}/
+%files -n python3-z3
+%{python3_sitelib}/z3/
 
 %changelog
-* Wed Feb 26 2020 Richard W.M. Jones <rjones@redhat.com> - 4.8.7-6
-- OCaml 4.10.0 final.
-
-* Fri Jan 31 2020 Fedora Release Engineering <releng@fedoraproject.org> - 4.8.7-5
-- Rebuilt for https://fedoraproject.org/wiki/Fedora_32_Mass_Rebuild
-
-* Tue Jan 21 2020 Jerry James <loganjerry@gmail.com> - 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 <rjones@redhat.com> - 4.8.7-4
-- OCaml 4.10.0+beta1 rebuild.
-
-* Fri Jan 10 2020 Richard W.M. Jones <rjones@redhat.com> - 4.8.7-3
-- OCaml 4.09.0 for riscv64
-
-* Sat Dec  7 2019 Jerry James <loganjerry@gmail.com> - 4.8.7-2
-- OCaml 4.09.0 (final) rebuild
-
-* Thu Nov 21 2019 Jerry James <loganjerry@gmail.com> - 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 <loganjerry@gmail.com> - 4.8.6-1
-- New upstream version
-
-* Mon Aug 19 2019 Miro Hrončok <mhroncok@redhat.com> - 4.8.5-6
-- Rebuilt for Python 3.8
-
-* Fri Aug 16 2019 Richard W.M. Jones <rjones@redhat.com> - 4.8.5-5
-- OCaml 4.08.1 (final) rebuild.
-
-* Wed Jul 31 2019 Richard W.M. Jones <rjones@redhat.com> - 4.8.5-4
-- OCaml 4.08.1 (rc2) rebuild.
-
-* Sat Jul 27 2019 Fedora Release Engineering <releng@fedoraproject.org> - 4.8.5-3
-- Rebuilt for https://fedoraproject.org/wiki/Fedora_31_Mass_Rebuild
-
-* Thu Jun 27 2019 Richard W.M. Jones <rjones@redhat.com> - 4.8.5-2
-- OCaml 4.08.0 (final) rebuild.
-
-* Sat Jun 22 2019 Jerry James <loganjerry@gmail.com> - 4.8.5-1
-- New upstream version
-
-* Mon Apr 29 2019 Richard W.M. Jones <rjones@redhat.com> - 4.8.4-3
-- OCaml 4.08.0 (beta 3) rebuild.
-
-* Sun Feb 03 2019 Fedora Release Engineering <releng@fedoraproject.org> - 4.8.4-2
-- Rebuilt for https://fedoraproject.org/wiki/Fedora_30_Mass_Rebuild
-
-* Mon Dec 24 2018 Jerry James <loganjerry@gmail.com> - 4.8.4-1
-- New upstream version
-- Drop -no-sse patch, now handled upstream
-
-* Wed Nov 28 2018 Jerry James <loganjerry@gmail.com> - 4.8.3-1
-- New upstream version
-
-* Tue Oct 30 2018 Jerry James <loganjerry@gmail.com> - 4.8.1-1
-- New upstream version
-- Drop python2 subpackage (bz 1634981)
-
-* Fri Sep  7 2018 Jerry James <loganjerry@gmail.com> - 4.7.1-5
-- Build with SSE2 support on 32-bit x86
-
-* Sat Jul 14 2018 Fedora Release Engineering <releng@fedoraproject.org> - 4.7.1-5
-- Rebuilt for https://fedoraproject.org/wiki/Fedora_29_Mass_Rebuild
-
-* Wed Jul 11 2018 Richard W.M. Jones <rjones@redhat.com> - 4.7.1-4
-- OCaml 4.07.0 (final) rebuild.
-
-* Wed Jun 20 2018 Richard W.M. Jones <rjones@redhat.com> - 4.7.1-3
-- OCaml 4.07.0-rc1 rebuild.
-
-* Tue Jun 19 2018 Miro Hrončok <mhroncok@redhat.com> - 4.7.1-2
-- Rebuilt for Python 3.7
-
-* Tue May 22 2018 Jerry James <loganjerry@gmail.com> - 4.7.1-1
-- New upstream version (bz 1581516)
-- Drop upstreamed -vector patch
-
-* Fri Feb 09 2018 Fedora Release Engineering <releng@fedoraproject.org> - 4.6.0-2
-- Rebuilt for https://fedoraproject.org/wiki/Fedora_28_Mass_Rebuild
-
-* Sun Dec 24 2017 Jerry James <loganjerry@gmail.com> - 4.6.0-1
-- New upstream version (bz 1527531)
-- Add a python3 subpackage
-
-* Sun Dec 17 2017 Zbigniew Jędrzejewski-Szmek <zbyszek@in.waw.pl> - 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 <rjones@redhat.com> - 4.5.0-7
-- OCaml 4.06.0 rebuild.
-- Add dependency on ocaml-num.
-
-* Tue Aug 08 2017 Richard W.M. Jones <rjones@redhat.com> - 4.5.0-6
-- OCaml 4.05.0 rebuild.
-
-* Thu Jul 27 2017 Fedora Release Engineering <releng@fedoraproject.org> - 4.5.0-5
-- Rebuilt for https://fedoraproject.org/wiki/Fedora_27_Mass_Rebuild
-
-* Tue Jun 27 2017 Richard W.M. Jones <rjones@redhat.com> - 4.5.0-4
-- OCaml 4.04.2 rebuild.
-
-* Fri May 12 2017 Richard W.M. Jones <rjones@redhat.com> - 4.5.0-3
-- OCaml 4.04.1 rebuild.
-
-* Sat Feb 11 2017 Fedora Release Engineering <releng@fedoraproject.org> - 4.5.0-2
-- Rebuilt for https://fedoraproject.org/wiki/Fedora_26_Mass_Rebuild
-
-* Tue Nov  8 2016 Jerry James <loganjerry@gmail.com> - 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 <rjones@redhat.com> - 4.4.1-8
-- Rebuild for OCaml 4.04.0.
-
-* Tue Jul 19 2016 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 4.4.1-7
-- https://fedoraproject.org/wiki/Changes/Automatic_Provides_for_Python_RPM_Packages
-
-* Wed Jul 13 2016 Jerry James <loganjerry@gmail.com> - 4.4.1-6
-- Fix Java interface (bz 1353773)
-
-* Thu Jun 30 2016 Jerry James <loganjerry@gmail.com> - 4.4.1-5
-- Fix __init__.py (bz 1351580)
-
-* Fri Feb 05 2016 Fedora Release Engineering <releng@fedoraproject.org> - 4.4.1-4
-- Rebuilt for https://fedoraproject.org/wiki/Fedora_24_Mass_Rebuild
-
-* Tue Feb 02 2016 Jonathan Wakely <jwakely@redhat.com> - 4.4.1-3
-- Patched for C++11 compatibility.
-
-* Wed Jan 20 2016 Jerry James <loganjerry@gmail.com> - 4.4.1-2
-- Add __init__.py to the python interface (bz 1298429)
-
-* Thu Oct  8 2015 Jerry James <loganjerry@gmail.com> - 4.4.1-1
-- New upstream version
-
-* Tue Jul 28 2015 Richard W.M. Jones <rjones@redhat.com> - 4.4.0-4
-- OCaml 4.02.3 rebuild.
-
-* Thu Jun 25 2015 Richard W.M. Jones <rjones@redhat.com> - 4.4.0-3
-- ocaml-4.02.2 final rebuild.
-
-* Thu Jun 18 2015 Richard W.M. Jones <rjones@redhat.com> - 4.4.0-2
-- ocaml-4.02.2 rebuild.
-
-* Wed May 27 2015 Jerry James <loganjerry@gmail.com> - 4.4.0-1
-- New upstream version
-
-* Wed Apr 22 2015 Jerry James <loganjerry@gmail.com> - 4.3.2-3.20150329git.29606b5
-- Fix issues found on review (bz 1206826)
-
-* Mon Mar 30 2015 Jerry James <loganjerry@gmail.com> - 4.3.2-2.20150329git.29606b5
-- Update to latest git HEAD
-- Include examples in -doc
-
-* Sat Mar 28 2015 Jerry James <loganjerry@gmail.com> - 4.3.2-1.20150327git.ac21ffe
-- Initial RPM
+%autochangelog