diff --git a/src/solver/parallel_tactic.cpp b/src/solver/parallel_tactic.cpp index c0bf63b237b..8336f005096 100644 --- a/src/solver/parallel_tactic.cpp +++ b/src/solver/parallel_tactic.cpp @@ -503,7 +503,10 @@ class parallel_tactic : public tactic { cube.append(s.split_cubes(1)); SASSERT(cube.size() <= 1); IF_VERBOSE(2, verbose_stream() << "(tactic.parallel :split-cube " << cube.size() << ")\n";); - if (!s.cubes().empty()) m_queue.add_task(s.clone()); + { + // std::lock_guard lock(m_mutex); + if (!s.cubes().empty()) m_queue.add_task(s.clone()); + } if (!cube.empty()) { s.assert_cube(cube.get(0).cube()); vars.reset(); @@ -611,8 +614,12 @@ class parallel_tactic : public tactic { void spawn_cubes(solver_state& s, unsigned width, vector& cubes) { if (cubes.empty()) return; add_branches(cubes.size()); - s.set_cubes(cubes); - solver_state* s1 = s.clone(); + s.set_cubes(cubes); + solver_state* s1 = nullptr; + { + // std::lock_guard lock(m_mutex); + s1 = s.clone(); + } s1->inc_width(width); m_queue.add_task(s1); }