From d44508e7e33405407ea4222566f8a82e8e3108da Mon Sep 17 00:00:00 2001
From: Jerry James <loganjerry@gmail.com>
Date: Mar 24 2022 19:58:33 +0000
Subject: Add -ambiguous-overload patch to fix cppcheck build failure.


---

diff --git a/z3-ambiguous-overload.patch b/z3-ambiguous-overload.patch
new file mode 100644
index 0000000..f50e3f4
--- /dev/null
+++ b/z3-ambiguous-overload.patch
@@ -0,0 +1,111 @@
+--- 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<Z3_ast> _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<Z3_ast> _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<Z3_ast> _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<Z3_ast> _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<Z3_ast> _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<Z3_ast> _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<Z3_ast> _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<Z3_ast> _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<Z3_ast> _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 e5cb053..decc836 100644
--- a/z3.spec
+++ b/z3.spec
@@ -5,7 +5,7 @@
 
 Name:           z3
 Version:        4.8.15
-Release:        1%{?dist}
+Release:        2%{?dist}
 Summary:        Satisfiability Modulo Theories (SMT) solver
 
 License:        MIT
@@ -13,6 +13,9 @@ 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
@@ -230,6 +233,9 @@ cd -
 %{python3_sitelib}/%{name}/
 
 %changelog
+* 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