From 7564ccc3f1d746942834e267bfa30d0a768d9b3c Mon Sep 17 00:00:00 2001 From: Lev Nachmanson <5377127+levnach@users.noreply.github.com> Date: Sat, 27 Jun 2026 17:43:08 -0700 Subject: [PATCH] capture row by pointer (#9973) Capture row as a pointer as lambda strips the reference and the vector was copied by value in lar_solver! --------- Signed-off-by: Lev Nachmanson Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- src/math/lp/bound_analyzer_on_row.h | 4 ++-- src/solver/parallel_tactical.cpp | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/math/lp/bound_analyzer_on_row.h b/src/math/lp/bound_analyzer_on_row.h index 70358ca7b8..6c2787d13d 100644 --- a/src/math/lp/bound_analyzer_on_row.h +++ b/src/math/lp/bound_analyzer_on_row.h @@ -297,7 +297,7 @@ namespace lp { void limit_j(unsigned bound_j, const mpq& u, bool coeff_before_j_is_pos, bool is_lower_bound, bool strict) { auto* lar = &m_bp.lp(); - const auto& row = this->m_row; + auto* row = &this->m_row; auto explain = [row, bound_j, coeff_before_j_is_pos, is_lower_bound, strict, lar]() { (void) strict; TRACE(bound_analyzer, tout << "explain_bound_on_var_on_coeff, bound_j = " << bound_j << ", coeff_before_j_is_pos = " << coeff_before_j_is_pos << ", is_lower_bound = " << is_lower_bound << ", strict = " << strict << "\n";); @@ -305,7 +305,7 @@ namespace lp { int j_sign = (coeff_before_j_is_pos ? 1 : -1) * bound_sign; u_dependency* ret = nullptr; - for (auto const& r : row) { + for (auto const& r : *row) { unsigned j = r.var(); if (j == bound_j) continue; diff --git a/src/solver/parallel_tactical.cpp b/src/solver/parallel_tactical.cpp index eb6659bf0d..b2955ed5a2 100644 --- a/src/solver/parallel_tactical.cpp +++ b/src/solver/parallel_tactical.cpp @@ -52,7 +52,7 @@ public: #ifdef SINGLE_THREAD -tactic* mk_parallel_tactic2(solver* s, params_ref const& p) { +tactic* mk_parallel_tactic(solver* s, params_ref const& p) { return alloc(non_parallel_tactic2, s, p); }