mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-13 22:41:15 +00:00
Code Activity

Update smt_parallel.cpp

Browse source 
Drop non-relevant units from shared structures.
This commit is contained in:
Nikolaj Bjorner 2025-08-03 14:16:52 -07:00
parent b9b3e0d337
commit d66fabe462
1 changed files with 3 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/smt/smt_parallel.cpp
View file

@ -119,6 +119,9 @@ namespace smt {
unsigned sz = pctx.assigned_literals().size();
for (unsigned j = unit_lim[i]; j < sz; ++j) {
literal lit = pctx.assigned_literals()[j];
//IF_VERBOSE(0, verbose_stream() << "(smt.thread " << i << " :unit " << lit << " " << pctx.is_relevant(lit.var()) << ")\n";);
if (!pctx.is_relevant(lit.var()))
continue;
expr_ref e(pctx.bool_var2expr(lit.var()), pctx.m);
if (lit.sign()) e = pctx.m.mk_not(e);
expr_ref ce(tr(e.get()), ctx.m);