mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-20 11:55:49 +00:00
Code Activity

fix: reduce verbose lock contention in theory_diff_logic (issue #8019)

Browse source 
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>
This commit is contained in:
copilot-swe-agent[bot] 2026-03-17 19:10:42 +00:00 • committed by Lev Nachmanson
parent 0461e010bb
commit 3745bdd43b
2 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/smt/theory_dense_diff_logic_def.h
View file

@ -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<bool>(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;
}
}

2
src/smt/theory_diff_logic_def.h
View file

@ -170,7 +170,7 @@ template<typename Ext>
void theory_diff_logic<Ext>::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<bool>(m_non_diff_logic_exprs));
m_non_diff_logic_exprs = true;
}