diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp index 49e03c8e2..b8629fb50 100644 --- a/src/smt/smt_parallel.cpp +++ b/src/smt/smt_parallel.cpp @@ -154,6 +154,10 @@ namespace smt { goto check_cube_start; b.split(m_l2g, id, node, atom); simplify(); + if (m_config.m_share_units) { + IF_VERBOSE(1, verbose_stream() << " Sharing units\n"); + share_units(); + } break; } case l_true: { @@ -203,10 +207,6 @@ namespace smt { break; } } - if (m_config.m_share_units) { - IF_VERBOSE(1, verbose_stream() << " Sharing units\n"); - share_units(); - } } } @@ -236,6 +236,7 @@ namespace smt { // Collect new units learned locally by this worker and send to batch manager 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(); for (unsigned j = m_num_shared_units; j < sz; ++j) { // iterate only over new literals since last sync literal lit = ctx->assigned_literals()[j];