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

This commit is contained in:
Jerry James 2020-05-09 16:45:27 -06:00
parent f61d5ceefa
commit dd0859c8cf
6 changed files with 8 additions and 61 deletions

View File

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

View File

@ -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);
}

View File

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

View File

@ -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:

View File

@ -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;

18
z3.spec
View File

@ -1,21 +1,13 @@
%global medtag 30e7c225cd51 %global medtag ad55a1f1c617
Name: z3 Name: z3
Version: 4.8.7 Version: 4.8.8
Release: 10%{?dist} Release: 1%{?dist}
Summary: Satisfiability Modulo Theories (SMT) solver Summary: Satisfiability Modulo Theories (SMT) solver
License: MIT License: MIT
URL: https://github.com/Z3Prover/z3 URL: https://github.com/Z3Prover/z3
Source0: https://github.com/Z3Prover/z3/archive/%{name}-%{version}.tar.gz 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: doxygen
BuildRequires: gcc-c++ BuildRequires: gcc-c++
@ -222,6 +214,10 @@ mv %{buildroot}%{_prefix}/lib/lib%{name}java.so %{buildroot}%{_libdir}/%{name}
%{python3_sitearch}/%{name}/ %{python3_sitearch}/%{name}/
%changelog %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
* Mon May 04 2020 Richard W.M. Jones <rjones@redhat.com> - 4.8.7-10 * Mon May 04 2020 Richard W.M. Jones <rjones@redhat.com> - 4.8.7-10
- OCaml 4.11.0+dev2-2020-04-22 rebuild - OCaml 4.11.0+dev2-2020-04-22 rebuild