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