mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-24 10:59:38 +00:00
Code Activity

dont collect clauses twice

Browse source
This commit is contained in:
Ilana Shapiro 2025-12-20 09:36:30 -08:00
parent e11bf4b9b1
commit c36cb2f516
1 changed files with 0 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/smt/smt_parallel.cpp
View file

@ -236,7 +236,6 @@ namespace smt {
// Collect new units learned locally by this worker and send to batch manager // Collect new units learned locally by this worker and send to batch manager
ctx->pop_to_base_lvl(); ctx->pop_to_base_lvl();
collect_shared_clauses(); // collect shared clauses from other workers while we're ALREADY POPPED TO BASE LEVEL
unsigned sz = ctx->assigned_literals().size(); unsigned sz = ctx->assigned_literals().size();
for (unsigned j = m_num_shared_units; j < sz; ++j) { // iterate only over new literals since last sync for (unsigned j = m_num_shared_units; j < sz; ++j) { // iterate only over new literals since last sync
literal lit = ctx->assigned_literals()[j]; literal lit = ctx->assigned_literals()[j];