make it easier to debug parallel

Z3Prover · Sep 10, 2021 · 34f878f · 34f878f
1 parent 3e6ff76
commit 34f878f
Showing 1 changed file with 10 additions and 3 deletions.
diff --git 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<std::mutex> 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<cube_var>& 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<std::mutex> lock(m_mutex);
+            s1 = s.clone();
+        }
         s1->inc_width(width);
         m_queue.add_task(s1);
     }