From 3745bdd43b2b2349b1904c7d49eccd99ef11a188 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Tue, 17 Mar 2026 19:10:42 +0000 Subject: [PATCH] fix: reduce verbose lock contention in theory_diff_logic (issue #8019) In multi-threaded solving, IF_VERBOSE(0, ...) in found_non_diff_logic_expr was always acquiring the global g_verbose_mux mutex (since verbosity >= 0 is always true) while holding it for potentially expensive mk_pp() calls. This caused catastrophic lock contention when multiple threads internalized atoms. Change IF_VERBOSE(0, ...) to IF_VERBOSE(2, ...) in both theory_diff_logic_def.h and theory_dense_diff_logic_def.h. The diagnostic message is still available at verbosity level 2 (-v:2), but is no longer printed (or locked) at the default verbosity level, eliminating the contention. Co-authored-by: levnach <5377127+levnach@users.noreply.github.com> --- src/smt/theory_dense_diff_logic_def.h | 2 +- src/smt/theory_diff_logic_def.h | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/smt/theory_dense_diff_logic_def.h b/src/smt/theory_dense_diff_logic_def.h index e260b0f6b..83c65d810 100644 --- a/src/smt/theory_dense_diff_logic_def.h +++ b/src/smt/theory_dense_diff_logic_def.h @@ -125,7 +125,7 @@ namespace smt { if (!m_non_diff_logic_exprs) { TRACE(non_diff_logic, tout << "found non diff logic expression:\n" << mk_pp(n, m) << "\n";); ctx.push_trail(value_trail(m_non_diff_logic_exprs)); - IF_VERBOSE(0, verbose_stream() << "(smt.diff_logic: non-diff logic expression " << mk_pp(n, m) << ")\n";); + IF_VERBOSE(2, verbose_stream() << "(smt.diff_logic: non-diff logic expression " << mk_pp(n, m) << ")\n";); m_non_diff_logic_exprs = true; } } diff --git a/src/smt/theory_diff_logic_def.h b/src/smt/theory_diff_logic_def.h index 382b2d3de..7b7519d55 100644 --- a/src/smt/theory_diff_logic_def.h +++ b/src/smt/theory_diff_logic_def.h @@ -170,7 +170,7 @@ template void theory_diff_logic::found_non_diff_logic_expr(expr * n) { if (!m_non_diff_logic_exprs) { TRACE(non_diff_logic, tout << "found non diff logic expression:\n" << mk_pp(n, m) << "\n";); - IF_VERBOSE(0, verbose_stream() << "(smt.diff_logic: non-diff logic expression " << mk_pp(n, m) << ")\n";); + IF_VERBOSE(2, verbose_stream() << "(smt.diff_logic: non-diff logic expression " << mk_pp(n, m) << ")\n";); ctx.push_trail(value_trail(m_non_diff_logic_exprs)); m_non_diff_logic_exprs = true; }