rpms/z3
3
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Add -ambiguous-overload patch to fix cppcheck build failure.

Browse Source
This commit is contained in:
Jerry James 2022-03-24 13:58:33 -06:00
parent 0d4eb3e8f9
commit d44508e7e3
2 changed files with 118 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

111
z3-ambiguous-overload.patch Normal file
View File

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

8
z3.spec
View File

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