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

Version 4.8.17. Drop upstreamed -ambiguous-overload patch.

Browse Source
This commit is contained in:
Jerry James 2022-05-19 11:32:13 -06:00
parent d44508e7e3
commit d11a9bc22b
3 changed files with 10 additions and 118 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
sources
View File

@ -1 +1 @@
SHA512 (z3-4.8.15.tar.gz) = 7b08dec5b035a38edc90c4c491f508fd9ed227357de94400169db53d4c59382bd6a81ae6615771023a06534a3aa92668844f0ebfcc2a3b5ef4bba957426a0c6c
SHA512 (z3-4.8.17.tar.gz) = 95517014ec1798c2552253dd5cde6f955896ab297a4f56294f4bc6f2c5428069015f513c6eb9a090a809cfcf4cb1cc38cc83818f19b5b1051e4e6c06f973747d

111
z3-ambiguous-overload.patch
View File

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

15
z3.spec
View File

@ -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 <loganjerry@gmail.com> - 4.8.17-1
- Version 4.8.17
- Drop upstreamed -ambiguous-overload patch
* Thu Mar 24 2022 Jerry James <loganjerry@gmail.com> - 4.8.15-2
- Add -ambiguous-overload patch to fix cppcheck build failure