From 2894808deacd42c6adada24d0c91349623ce8670 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Wed, 13 May 2026 00:01:08 +0000 Subject: [PATCH] address code review: cap conflict growth, clarify cube/split comments, use mk_or for conflict clause Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/8b3749c7-5957-41aa-85b5-2d76d4780d61 Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/solver/parallel_tactical2.cpp | 15 ++++++++++++++- 1 file changed, 14 insertions(+), 1 deletion(-) diff --git a/src/solver/parallel_tactical2.cpp b/src/solver/parallel_tactical2.cpp index bffc82a0b..1374e136a 100644 --- a/src/solver/parallel_tactical2.cpp +++ b/src/solver/parallel_tactical2.cpp @@ -475,6 +475,9 @@ class parallel_solver { void update_max_conflicts() { m_config.m_threads_max_conflicts = static_cast( m_config.m_max_conflict_mul * m_config.m_threads_max_conflicts); + /* cap at the configured global maximum to prevent runaway cube checks */ + if (m_config.m_threads_max_conflicts > m_config.m_max_conflicts) + m_config.m_threads_max_conflicts = m_config.m_max_conflicts; } /* Check the current cube (passed as additional assumptions). @@ -562,6 +565,11 @@ class parallel_solver { s->pop(1); + /* solver::cube() convention: an empty result means done; a result + * whose last element is true means the problem is trivially sat; + * a result whose last element is false means unsat was detected. + * In all other cases every element (including index 0) is a + * valid literal that can serve as a split atom. */ if (c.empty() || m.is_true(c.back()) || m.is_false(c.back())) return expr_ref(nullptr, m); @@ -665,7 +673,12 @@ class parallel_solver { b.backtrack(m_l2g, id, cube_core, lease); if (m_config.m_share_conflicts) { - expr_ref clause(mk_not(mk_and(cube_core)), m); + /* Share the negation of the cube-core conjunction + * as a learned clause: ¬(c₁ ∧ … ∧ cₙ) ≡ ¬c₁ ∨ … ∨ ¬cₙ */ + expr_ref_vector neg_lits(m); + for (expr* c : cube_core) + neg_lits.push_back(mk_not(expr_ref(c, m))); + expr_ref clause(mk_or(neg_lits), m); b.collect_clause(m_l2g, id, clause.get()); } if (m_config.m_share_units) share_units();