mirror of
https://github.com/Z3Prover/z3
synced 2025-09-30 21:19:29 +00:00
Revert "resolve bug about not popping local ctx to base level before collecting shared lits"
This reverts commit bba1111e1b
.
This commit is contained in:
parent
7f25a0d71b
commit
3ba08bd3c5
1 changed files with 0 additions and 1 deletions
|
@ -124,7 +124,6 @@ namespace smt {
|
||||||
|
|
||||||
void parallel::worker::share_units(ast_translation& l2g) {
|
void parallel::worker::share_units(ast_translation& l2g) {
|
||||||
// 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();
|
|
||||||
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];
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue