From f988e76da6ec3e7221b9dec130aa4d40f5a353c4 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Sun, 8 Feb 2026 03:21:20 +0000 Subject: [PATCH 1/4] Initial plan From a08e8a99f9ab7ab37181eb5e2e7a5abdae916260 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Sun, 8 Feb 2026 03:26:13 +0000 Subject: [PATCH 2/4] Add -headerpad_max_install_names flag for macOS dylib builds This fixes the install_name_tool issue on macOS where the tool fails with "larger updated load commands do not fit". The linker flag -Wl,-headerpad_max_install_names ensures sufficient header padding in the Mach-O binary for install_name_tool to modify install names. Changes made: - CMake: Added flag to libz3, z3java, z3jl shared libraries on Darwin - Python build: Changed flag from ML-only to all macOS builds - OCaml CMake: Added flag to OCaml stublib build on APPLE Fixes #7623 (regression in 4.15.5) Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- scripts/mk_util.py | 4 +++- src/CMakeLists.txt | 4 ++++ src/api/java/CMakeLists.txt | 4 ++++ src/api/julia/CMakeLists.txt | 4 ++++ src/api/ml/CMakeLists.txt | 3 +++ 5 files changed, 18 insertions(+), 1 deletion(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 48cdb953a..864b6e23e 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -2749,7 +2749,9 @@ def mk_config(): CXXFLAGS = '%s -arch arm64' % CXXFLAGS LDFLAGS = '%s -arch arm64' % LDFLAGS SLIBEXTRAFLAGS = '%s -arch arm64' % SLIBEXTRAFLAGS - if IS_OSX and is_ml_enabled(): + # Add header padding for macOS to allow install_name_tool to modify the dylib + # This fixes issues where install_name_tool fails with "larger updated load commands do not fit" + if IS_OSX: SLIBFLAGS += ' -Wl,-headerpad_max_install_names' config.write('PREFIX=%s\n' % PREFIX) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 2af9a7170..22b5ce513 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -134,6 +134,10 @@ if (CMAKE_SYSTEM_NAME STREQUAL "Darwin") # Enable RPATH support MACOSX_RPATH TRUE ) + # Add header padding to allow install_name_tool to modify the dylib + # This fixes issues where install_name_tool fails with "larger updated load commands do not fit" + # See: https://github.com/Z3Prover/z3/issues/7623 + target_link_options(libz3 PRIVATE "-Wl,-headerpad_max_install_names") endif() if (NOT MSVC) diff --git a/src/api/java/CMakeLists.txt b/src/api/java/CMakeLists.txt index 862e25962..5245a62da 100644 --- a/src/api/java/CMakeLists.txt +++ b/src/api/java/CMakeLists.txt @@ -48,6 +48,10 @@ target_include_directories(z3java PRIVATE "${PROJECT_BINARY_DIR}/src/api" ${JNI_INCLUDE_DIRS} ) +# Add header padding for macOS to allow install_name_tool to modify the dylib +if (CMAKE_SYSTEM_NAME STREQUAL "Darwin") + target_link_options(z3java PRIVATE "-Wl,-headerpad_max_install_names") +endif() # FIXME: Should this library have SONAME and VERSION set? # This prevents CMake from automatically defining ``z3java_EXPORTS`` diff --git a/src/api/julia/CMakeLists.txt b/src/api/julia/CMakeLists.txt index 952b33fb5..9b34564be 100644 --- a/src/api/julia/CMakeLists.txt +++ b/src/api/julia/CMakeLists.txt @@ -34,6 +34,10 @@ target_include_directories(z3jl PRIVATE "${PROJECT_BINARY_DIR}/src/api" "${PROJECT_SOURCE_DIR}/src/api/c++" ) +# Add header padding for macOS to allow install_name_tool to modify the dylib +if (CMAKE_SYSTEM_NAME STREQUAL "Darwin") + target_link_options(z3jl PRIVATE "-Wl,-headerpad_max_install_names") +endif() option(Z3_INSTALL_JULIA_BINDINGS "Install Julia bindings when invoking install target" ON) if(Z3_INSTALL_JULIA_BINDINGS) diff --git a/src/api/ml/CMakeLists.txt b/src/api/ml/CMakeLists.txt index c7de53faa..0e5e92be8 100644 --- a/src/api/ml/CMakeLists.txt +++ b/src/api/ml/CMakeLists.txt @@ -159,6 +159,9 @@ endif() if( APPLE ) # set(ocaml_rpath "@executable_path/../libz3${so_ext}") + # Add header padding to allow install_name_tool to modify the dylib + # This fixes issues where install_name_tool fails with "larger updated load commands do not fit" + list(APPEND c_lib_deps "-ldopt" "-Wl,-headerpad_max_install_names") elseif( UNIX ) set(ocaml_rpath "\\$ORIGIN/../libz3${so_ext}") list(APPEND c_lib_deps "-dllpath" ${ocaml_rpath}) From 56db8d5e98f0228b8cd8021442764ae9d3cae591 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Sun, 8 Feb 2026 08:40:49 -1000 Subject: [PATCH 3/4] fix nlsat_explain.cpp that the regression tests would pass with lws=false Signed-off-by: Lev Nachmanson --- src/nlsat/nlsat_explain.cpp | 27 +++++++++++++++++++-------- 1 file changed, 19 insertions(+), 8 deletions(-) diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp index 714e49c3f..51d8ff171 100644 --- a/src/nlsat/nlsat_explain.cpp +++ b/src/nlsat/nlsat_explain.cpp @@ -100,8 +100,8 @@ namespace nlsat { m_simplify_cores = false; m_full_dimensional = false; m_minimize_cores = false; - m_add_all_coeffs = true; - m_add_zero_disc = true; + m_add_all_coeffs = false; + m_add_zero_disc = false; } // display helpers moved to free functions in nlsat_common.h @@ -901,11 +901,11 @@ namespace nlsat { yy = m_pm.mk_polynomial(y); p_diff = 2*A*yy + B; p_diff = m_pm.normalize(p_diff); - int sq = ensure_sign(q); + int sq = ensure_sign_quad(q); if (sq < 0) { return false; } - int sa = ensure_sign(A); + int sa = ensure_sign_quad(A); if (sa == 0) { q = B*yy + C; return mk_plinear_root(k, y, i, q); @@ -918,12 +918,23 @@ namespace nlsat { return true; } - int ensure_sign(polynomial_ref & p) { + void ensure_sign(polynomial_ref & p) { + if (is_const(p) || m_processed.contains(p)) + return; int s = sign(p); - if (!is_const(p)) { + TRACE(nlsat_explain, tout << p << "\n";); + add_assumption(s == 0 ? atom::EQ : (s < 0 ? atom::LT : atom::GT), p); + // Also add p to the projection to ensure proper cell construction + insert_fresh_factors_in_todo(p); + } + + // Specialized version for quadratic root handling. + // Returns the sign value (-1, 0, or 1). + int ensure_sign_quad(polynomial_ref & p) { + int s = sign(p); + if (!is_const(p) && !m_processed.contains(p)) { TRACE(nlsat_explain, tout << p << "\n";); add_assumption(s == 0 ? atom::EQ : (s < 0 ? atom::LT : atom::GT), p); - // Also add p to the projection to ensure proper cell construction insert_fresh_factors_in_todo(p); } return s; @@ -1101,7 +1112,6 @@ namespace nlsat { use_all_coeffs = true; } // Set m_add_all_coeffs for the rest of the projection, restore on function exit - flet _set_all_coeffs(m_add_all_coeffs, use_all_coeffs || m_add_all_coeffs); var x = m_todo.extract_max_polys(ps); collect_to_processed(ps); @@ -1665,6 +1675,7 @@ namespace nlsat { void compute_conflict_explanation(unsigned num, literal const * ls, scoped_literal_vector & result) { SASSERT(check_already_added()); SASSERT(num > 0); + flet _restore_add_all_coeffs(m_add_all_coeffs, false); TRACE(nlsat_explain, tout << "the infeasible clause:\n"; display(tout, m_solver, num, ls) << "\n"; From c0be7ac621d3ea2cc95673b9c81dfcf292de049c Mon Sep 17 00:00:00 2001 From: Copilot <198982749+Copilot@users.noreply.github.com> Date: Sun, 8 Feb 2026 18:53:43 +0000 Subject: [PATCH 4/4] Remove unused swap() methods (#8538) --- src/math/dd/dd_bdd.h | 2 +- src/math/dd/dd_pdd.h | 2 +- src/util/obj_hashtable.h | 4 ---- src/util/obj_ref.h | 11 +++++++---- src/util/ref_pair_vector.h | 5 ----- src/util/scoped_ptr_vector.h | 5 ++--- src/util/util.h | 4 ++-- src/util/vector.h | 8 ++++---- 8 files changed, 17 insertions(+), 24 deletions(-) diff --git a/src/math/dd/dd_bdd.h b/src/math/dd/dd_bdd.h index 93332bd91..352b48551 100644 --- a/src/math/dd/dd_bdd.h +++ b/src/math/dd/dd_bdd.h @@ -278,7 +278,7 @@ namespace dd { bdd(unsigned root, bdd_manager* m): root(root), m(m) { m->inc_ref(root); } public: bdd(bdd const & other): root(other.root), m(other.m) { m->inc_ref(root); } - bdd(bdd && other) noexcept : root(0), m(other.m) { std::swap(root, other.root); } + bdd(bdd && other) noexcept : root(other.root), m(other.m) { other.root = 0; } bdd& operator=(bdd const& other); ~bdd() { m->dec_ref(root); } bdd lo() const { return bdd(m->lo(root), m); } diff --git a/src/math/dd/dd_pdd.h b/src/math/dd/dd_pdd.h index ecdaf1e69..907176f04 100644 --- a/src/math/dd/dd_pdd.h +++ b/src/math/dd/dd_pdd.h @@ -418,7 +418,7 @@ namespace dd { public: pdd(pdd_manager& m): pdd(0, m) { SASSERT(is_zero()); } pdd(pdd const& other): pdd(other.root, other.m) { m->inc_ref(root); } - pdd(pdd && other) noexcept : pdd(0, other.m) { std::swap(root, other.root); } + pdd(pdd && other) noexcept : root(other.root), m(other.m) { other.root = 0; } pdd& operator=(pdd const& other); pdd& operator=(unsigned k); pdd& operator=(rational const& k); diff --git a/src/util/obj_hashtable.h b/src/util/obj_hashtable.h index cf7cdff05..ae53fbe6d 100644 --- a/src/util/obj_hashtable.h +++ b/src/util/obj_hashtable.h @@ -206,10 +206,6 @@ public: collisions.push_back(kd.m_key); } } - - void swap(obj_map & other) noexcept { - m_table.swap(other.m_table); - } }; /** diff --git a/src/util/obj_ref.h b/src/util/obj_ref.h index 9ab68676d..0c28752be 100644 --- a/src/util/obj_ref.h +++ b/src/util/obj_ref.h @@ -52,8 +52,8 @@ public: inc_ref(); } - obj_ref(obj_ref && other) noexcept : m_obj(nullptr), m_manager(other.m_manager) { - std::swap(m_obj, other.m_obj); + obj_ref(obj_ref && other) noexcept : m_obj(other.m_obj), m_manager(other.m_manager) { + other.m_obj = nullptr; } ~obj_ref() { dec_ref(); } @@ -95,8 +95,11 @@ public: obj_ref & operator=(obj_ref && n) noexcept { SASSERT(&m_manager == &n.m_manager); - std::swap(m_obj, n.m_obj); - n.reset(); + if (this != &n) { + dec_ref(); + m_obj = n.m_obj; + n.m_obj = nullptr; + } return *this; } diff --git a/src/util/ref_pair_vector.h b/src/util/ref_pair_vector.h index 1ed708168..3f88cfb85 100644 --- a/src/util/ref_pair_vector.h +++ b/src/util/ref_pair_vector.h @@ -193,11 +193,6 @@ public: TManager & m() const { return get_manager(); } - - void swap(ref_pair_vector & other) noexcept { - SASSERT(&(this->m_manager) == &(other.m_manager)); - this->m_nodes.swap(other.m_nodes); - } class element_ref { elem_t & m_ref; diff --git a/src/util/scoped_ptr_vector.h b/src/util/scoped_ptr_vector.h index 06688eb71..8fe5f91ad 100644 --- a/src/util/scoped_ptr_vector.h +++ b/src/util/scoped_ptr_vector.h @@ -31,14 +31,13 @@ public: scoped_ptr_vector(scoped_ptr_vector& other) = delete; scoped_ptr_vector& operator=(scoped_ptr_vector& other) = delete; - scoped_ptr_vector(scoped_ptr_vector&& other) noexcept { - m_vector.swap(other.m_vector); + scoped_ptr_vector(scoped_ptr_vector&& other) noexcept : m_vector(std::move(other.m_vector)) { } scoped_ptr_vector& operator=(scoped_ptr_vector&& other) noexcept { if (this == &other) return *this; reset(); - m_vector.swap(other.m_vector); + m_vector = std::move(other.m_vector); return *this; } diff --git a/src/util/util.h b/src/util/util.h index 4b5af2b52..d580209e9 100644 --- a/src/util/util.h +++ b/src/util/util.h @@ -231,8 +231,8 @@ public: m_ptr(ptr) { } - scoped_ptr(scoped_ptr &&other) noexcept : m_ptr(nullptr) { - std::swap(m_ptr, other.m_ptr); + scoped_ptr(scoped_ptr &&other) noexcept : m_ptr(other.m_ptr) { + other.m_ptr = nullptr; } ~scoped_ptr() { diff --git a/src/util/vector.h b/src/util/vector.h index 8932a789c..b0c1a0b6b 100644 --- a/src/util/vector.h +++ b/src/util/vector.h @@ -165,8 +165,8 @@ public: SASSERT(size() == source.size()); } - vector(vector&& other) noexcept { - std::swap(m_data, other.m_data); + vector(vector&& other) noexcept : m_data(other.m_data) { + other.m_data = nullptr; } vector(SZ s, T const * data) { @@ -225,8 +225,8 @@ public: return *this; } destroy(); - m_data = nullptr; - std::swap(m_data, source.m_data); + m_data = source.m_data; + source.m_data = nullptr; return *this; }