git: 92b9946c916c - main - math/z3: Update to 4.13.2
- Go to: [ bottom of page ] [ top of archives ] [ this month ]
Date: Sat, 28 Sep 2024 14:18:06 UTC
The branch main has been updated by arrowd:
URL: https://cgit.FreeBSD.org/ports/commit/?id=92b9946c916c8f9841f795df308ae373c6a4916b
commit 92b9946c916c8f9841f795df308ae373c6a4916b
Author: Gleb Popov <arrowd@FreeBSD.org>
AuthorDate: 2024-09-28 14:17:38 +0000
Commit: Gleb Popov <arrowd@FreeBSD.org>
CommitDate: 2024-09-28 14:18:02 +0000
math/z3: Update to 4.13.2
Reported by: repology.org
---
math/z3/Makefile | 2 +-
math/z3/distinfo | 6 +-
math/z3/files/patch-backport-2ce89e5f4 | 125 ---------------------------------
math/z3/pkg-plist | 2 +-
4 files changed, 5 insertions(+), 130 deletions(-)
diff --git a/math/z3/Makefile b/math/z3/Makefile
index d58e82b1d59a..d793caa3e4a6 100644
--- a/math/z3/Makefile
+++ b/math/z3/Makefile
@@ -1,6 +1,6 @@
PORTNAME= z3
DISTVERSIONPREFIX= z3-
-DISTVERSION= 4.13.0
+DISTVERSION= 4.13.2
CATEGORIES= math
MAINTAINER= arrowd@FreeBSD.org
diff --git a/math/z3/distinfo b/math/z3/distinfo
index 57345d04df5a..8ff6c36ddf0d 100644
--- a/math/z3/distinfo
+++ b/math/z3/distinfo
@@ -1,3 +1,3 @@
-TIMESTAMP = 1713421143
-SHA256 (Z3Prover-z3-z3-4.13.0_GH0.tar.gz) = 01bcc61c8362e37bb89fd2430f7e3385e86df7915019bd2ce45de9d9bd934502
-SIZE (Z3Prover-z3-z3-4.13.0_GH0.tar.gz) = 5520232
+TIMESTAMP = 1727532409
+SHA256 (Z3Prover-z3-z3-4.13.2_GH0.tar.gz) = fd7dc6dd2633074f0a47670d6378b0e5c28c2c26f2b58aa23e9cd7f0bc9ba0dc
+SIZE (Z3Prover-z3-z3-4.13.2_GH0.tar.gz) = 5578178
diff --git a/math/z3/files/patch-backport-2ce89e5f4 b/math/z3/files/patch-backport-2ce89e5f4
deleted file mode 100644
index 07161f1d64ed..000000000000
--- a/math/z3/files/patch-backport-2ce89e5f4
+++ /dev/null
@@ -1,125 +0,0 @@
-From 2ce89e5f491fa817d02d8fdce8c62798beab258b Mon Sep 17 00:00:00 2001
-From: David Seifert <16636962+SoapGentoo@users.noreply.github.com>
-Date: Mon, 29 Jul 2024 20:07:10 +0200
-Subject: [PATCH] Gcc 15 two phase (#7313)
-
-* Fix `-Wclass-memaccess`
-
-* Fix for GCC 15 two-phase lookup
-
-* GCC 15 is more aggressive about checking dependent names:
- https://gcc.gnu.org/git/?p=gcc.git;a=commitdiff;h=r15-2117-g313afcfdabeab3
-
-Bug: https://bugs.gentoo.org/936634
----
- src/math/lp/lp_settings.h | 69 ++++++++++++++++-----------------
- src/math/lp/static_matrix.h | 2 +-
- src/math/lp/static_matrix_def.h | 2 +-
- 3 files changed, 36 insertions(+), 37 deletions(-)
-
-diff --git src/math/lp/lp_settings.h src/math/lp/lp_settings.h
-index d1a4be21c64..0d47877c76b 100644
---- src/math/lp/lp_settings.h
-+++ src/math/lp/lp_settings.h
---- src/math/lp/lp_settings.h.orig 2024-03-07 18:25:16 UTC
-+++ src/math/lp/lp_settings.h
-@@ -97,39 +97,39 @@ struct statistics {
- };
-
- struct statistics {
-- unsigned m_make_feasible;
-- unsigned m_total_iterations;
-- unsigned m_iters_with_no_cost_growing;
-- unsigned m_num_factorizations;
-- unsigned m_num_of_implied_bounds;
-- unsigned m_need_to_solve_inf;
-- unsigned m_max_cols;
-- unsigned m_max_rows;
-- unsigned m_gcd_calls;
-- unsigned m_gcd_conflicts;
-- unsigned m_cube_calls;
-- unsigned m_cube_success;
-- unsigned m_patches;
-- unsigned m_patches_success;
-- unsigned m_hnf_cutter_calls;
-- unsigned m_hnf_cuts;
-- unsigned m_nla_calls;
-- unsigned m_gomory_cuts;
-- unsigned m_nla_add_bounds;
-- unsigned m_nla_propagate_bounds;
-- unsigned m_nla_propagate_eq;
-- unsigned m_nla_lemmas;
-- unsigned m_nra_calls;
-- unsigned m_nla_bounds_improvements;
-- unsigned m_horner_calls;
-- unsigned m_horner_conflicts;
-- unsigned m_cross_nested_forms;
-- unsigned m_grobner_calls;
-- unsigned m_grobner_conflicts;
-- unsigned m_offset_eqs;
-- unsigned m_fixed_eqs;
-+ unsigned m_make_feasible = 0;
-+ unsigned m_total_iterations = 0;
-+ unsigned m_iters_with_no_cost_growing = 0;
-+ unsigned m_num_factorizations = 0;
-+ unsigned m_num_of_implied_bounds = 0;
-+ unsigned m_need_to_solve_inf = 0;
-+ unsigned m_max_cols = 0;
-+ unsigned m_max_rows = 0;
-+ unsigned m_gcd_calls = 0;
-+ unsigned m_gcd_conflicts = 0;
-+ unsigned m_cube_calls = 0;
-+ unsigned m_cube_success = 0;
-+ unsigned m_patches = 0;
-+ unsigned m_patches_success = 0;
-+ unsigned m_hnf_cutter_calls = 0;
-+ unsigned m_hnf_cuts = 0;
-+ unsigned m_nla_calls = 0;
-+ unsigned m_gomory_cuts = 0;
-+ unsigned m_nla_add_bounds = 0;
-+ unsigned m_nla_propagate_bounds = 0;
-+ unsigned m_nla_propagate_eq = 0;
-+ unsigned m_nla_lemmas = 0;
-+ unsigned m_nra_calls = 0;
-+ unsigned m_nla_bounds_improvements = 0;
-+ unsigned m_horner_calls = 0;
-+ unsigned m_horner_conflicts = 0;
-+ unsigned m_cross_nested_forms = 0;
-+ unsigned m_grobner_calls = 0;
-+ unsigned m_grobner_conflicts = 0;
-+ unsigned m_offset_eqs = 0;
-+ unsigned m_fixed_eqs = 0;
- statistics() { reset(); }
-- void reset() { memset(this, 0, sizeof(*this)); }
-+ void reset() { *this = statistics{}; }
- void collect_statistics(::statistics& st) const {
- st.update("arith-factorizations", m_num_factorizations);
- st.update("arith-make-feasible", m_make_feasible);
-diff --git src/math/lp/static_matrix.h src/math/lp/static_matrix.h
-index 9d6bb859964..42dd476b5d4 100644
---- src/math/lp/static_matrix.h
-+++ src/math/lp/static_matrix.h
-@@ -79,7 +79,7 @@ class static_matrix (public)
- ref(static_matrix & m, unsigned row, unsigned col):m_matrix(m), m_row(row), m_col(col) {}
- ref & operator=(T const & v) { m_matrix.set( m_row, m_col, v); return *this; }
-
-- ref operator=(ref & v) { m_matrix.set(m_row, m_col, v.m_matrix.get(v.m_row, v.m_col)); return *this; }
-+ ref operator=(ref & v) { m_matrix.set(m_row, m_col, v.m_matrix.get_elem(v.m_row, v.m_col)); return *this; }
-
- operator T () const { return m_matrix.get_elem(m_row, m_col); }
- };
-diff --git src/math/lp/static_matrix_def.h src/math/lp/static_matrix_def.h
-index 0370ee8990a..c3b2fc16821 100644
---- src/math/lp/static_matrix_def.h
-+++ src/math/lp/static_matrix_def.h
---- src/math/lp/static_matrix_def.h.orig 2024-03-07 18:25:16 UTC
-+++ src/math/lp/static_matrix_def.h
-@@ -92,7 +92,7 @@ static_matrix<T, X>::static_matrix(static_matrix const
- init_row_columns(m, m);
- for (; m-- > 0; )
- for (auto & col : A.m_columns[m])
-- set(col.var(), m, A.get_value_of_column_cell(col));
-+ set(col.var(), m, A.get_column_cell(col));
- }
-
- template <typename T, typename X> void static_matrix<T, X>::clear() {
diff --git a/math/z3/pkg-plist b/math/z3/pkg-plist
index 09c647afface..41fa8dd7a334 100644
--- a/math/z3/pkg-plist
+++ b/math/z3/pkg-plist
@@ -19,5 +19,5 @@ lib/cmake/z3/Z3Targets-%%CMAKE_BUILD_TYPE%%.cmake
lib/cmake/z3/Z3Targets.cmake
lib/libz3.so
lib/libz3.so.4.13
-lib/libz3.so.4.13.0.0
+lib/libz3.so.4.13.2.0
libdata/pkgconfig/z3.pc