Version 4.8.8. Drop all patches; all have been upstreamed.

sources

@@ -1 +1 @@
-SHA512 (z3-4.8.7.tar.gz) = 145e2b2f1fa4edd0917107c7e1d54d779c7ed85c48af2ce6def4c90d1c4db05f74c9657e173cedf48770589fbe484c97fa1923295271cd3792523ffc4f67ed0c
+SHA512 (z3-4.8.8.tar.gz) = a6823cadb7cdad11b8f0db1530676c0ec4853886dfb3c4dbc5b798c5dbd445afb0c61675f81cb7f99c1b1734d9cd0ec96a07c68a948da3c25801fc6767fea47f

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

@@ -1,21 +1,13 @@
-%global medtag  30e7c225cd51
+%global medtag  ad55a1f1c617
 
 Name:           z3
-Version:        4.8.7
-Release:        6%{?dist}
+Version:        4.8.8
+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
-# 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
 
 BuildRequires:  doxygen
 BuildRequires:  gcc-c++
@@ -222,6 +214,13 @@ mv %{buildroot}%{_prefix}/lib/lib%{name}java.so %{buildroot}%{_libdir}/%{name}
 %{python3_sitearch}/%{name}/
 
 %changelog
+* Sat May  9 2020 Jerry James <loganjerry@gmail.com> - 4.8.8-1
+- Version 4.8.8
+- Drop all patches; all have been upstreamed
+
+* Thu Feb 27 2020 Richard W.M. Jones <rjones@redhat.com> - 4.8.7-6.1
+- OCaml 4.10.0 final (Fedora 32).
+
 * Wed Feb 26 2020 Richard W.M. Jones <rjones@redhat.com> - 4.8.7-6
 - OCaml 4.10.0 final.