diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp index 4d9f84c02..66e4ee28d 100644 --- a/src/smt/smt_parallel.cpp +++ b/src/smt/smt_parallel.cpp @@ -341,6 +341,7 @@ namespace smt { // currenly, the code just implements the greedy strategy void parallel::batch_manager::return_cubes(ast_translation& l2g, vectorconst& C_worker, expr_ref_vector const& A_worker) { + std::scoped_lock lock(mux); auto atom_in_cube = [&](expr_ref_vector const& cube, expr* atom) { return any_of(cube, [&](expr* e) { return e == atom || (m.is_not(e, e) && e == atom); }); };