Skip to content

Commit bba1111

Browse files
committed
resolve bug about not popping local ctx to base level before collecting shared lits
1 parent ae64207 commit bba1111

File tree

1 file changed

+1
-0
lines changed

1 file changed

+1
-0
lines changed

src/smt/smt_parallel.cpp

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -124,6 +124,7 @@ namespace smt {
124124

125125
void parallel::worker::share_units(ast_translation& l2g) {
126126
// Collect new units learned locally by this worker and send to batch manager
127+
ctx->pop_to_base_lvl();
127128
unsigned sz = ctx->assigned_literals().size();
128129
for (unsigned j = m_num_shared_units; j < sz; ++j) { // iterate only over new literals since last sync
129130
literal lit = ctx->assigned_literals()[j];

0 commit comments

Comments
 (0)