diff --git a/sources b/sources index 9e729c3..a0be432 100644 --- a/sources +++ b/sources @@ -1 +1 @@ -SHA512 (z3-4.8.7.tar.gz) = 145e2b2f1fa4edd0917107c7e1d54d779c7ed85c48af2ce6def4c90d1c4db05f74c9657e173cedf48770589fbe484c97fa1923295271cd3792523ffc4f67ed0c +SHA512 (z3-4.8.8.tar.gz) = a6823cadb7cdad11b8f0db1530676c0ec4853886dfb3c4dbc5b798c5dbd445afb0c61675f81cb7f99c1b1734d9cd0ec96a07c68a948da3c25801fc6767fea47f diff --git a/z3-gcc-10-s390x.patch b/z3-gcc-10-s390x.patch deleted file mode 100644 index b680900..0000000 --- a/z3-gcc-10-s390x.patch +++ /dev/null @@ -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::update_basis_and_x_tableau(int, int, lp::mpq const&); - template bool lp::lp_primal_core_solver::update_basis_and_x_tableau(int, int, double const&); - template bool lp::lp_primal_core_solver >::update_basis_and_x_tableau(int, int, lp::numeric_pair const&); -+template void lp::lp_primal_core_solver >::update_inf_cost_for_column_tableau(unsigned); - - } diff --git a/z3-ocamldoc.patch b/z3-ocamldoc.patch deleted file mode 100644 index f12931a..0000000 --- a/z3-ocamldoc.patch +++ /dev/null @@ -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.") diff --git a/z3-signed-char.patch b/z3-signed-char.patch deleted file mode 100644 index ce49a59..0000000 --- a/z3-signed-char.patch +++ /dev/null @@ -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(-1): - m_state = EOF_TOKEN; - break; - default: diff --git a/z3-trailing-zeros32.patch b/z3-trailing-zeros32.patch deleted file mode 100644 index 0b0fedc..0000000 --- a/z3-trailing-zeros32.patch +++ /dev/null @@ -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; diff --git a/z3.spec b/z3.spec index 3972dff..03d7f45 100644 --- a/z3.spec +++ b/z3.spec @@ -1,21 +1,13 @@ -%global medtag 30e7c225cd51 +%global medtag ad55a1f1c617 Name: z3 -Version: 4.8.7 -Release: 6%{?dist}.1 +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,10 @@ mv %{buildroot}%{_prefix}/lib/lib%{name}java.so %{buildroot}%{_libdir}/%{name} %{python3_sitearch}/%{name}/ %changelog +* Sat May 9 2020 Jerry James - 4.8.8-1 +- Version 4.8.8 +- Drop all patches; all have been upstreamed + * Thu Feb 27 2020 Richard W.M. Jones - 4.8.7-6.1 - OCaml 4.10.0 final (Fedora 32).