diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index 604ec67c5..8a5da7531 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -1300,13 +1300,12 @@ namespace sat {
             }
         };
 
-        vector<std::thread> threads;
+        vector<std::thread> threads(num_threads);
         for (int i = 0; i < num_threads; ++i) {
-            int id = i;
-            threads.push_back(std::thread([&]() { worker_thread(id); }));
+            threads[i] = std::thread([&, i]() { worker_thread(i); });
         }
-        for (int i = 0; i < num_threads; ++i) {
-            threads[i].join();
+        for (auto & th : threads) {
+            th.join();
         }
         
         if (IS_AUX_SOLVER(finished_id)) {
diff --git a/src/smt/tactic/smt_tactic.cpp b/src/smt/tactic/smt_tactic.cpp
index 5445d6089..0796471b1 100644
--- a/src/smt/tactic/smt_tactic.cpp
+++ b/src/smt/tactic/smt_tactic.cpp
@@ -59,7 +59,7 @@ public:
     }
 
     ~smt_tactic() override {
-        SASSERT(m_ctx == 0);
+        SASSERT(m_ctx == nullptr);
     }
 
     smt_params & fparams() {
@@ -132,7 +132,6 @@ public:
                 new_ctx->set_progress_callback(o.m_callback);
             }
             o.m_ctx = new_ctx;
-
         }
 
         ~scoped_init_ctx() {
@@ -208,7 +207,7 @@ public:
                 m_ctx->collect_statistics(m_stats);
                 throw;
             }
-			SASSERT(m_ctx);
+            SASSERT(m_ctx);
             m_ctx->collect_statistics(m_stats);
             proof * pr = m_ctx->get_proof();
             TRACE("smt_tactic", tout << r << " " << pr << "\n";);
diff --git a/src/tactic/tactical.cpp b/src/tactic/tactical.cpp
index 063f3dbe1..ea89c6642 100644
--- a/src/tactic/tactical.cpp
+++ b/src/tactic/tactical.cpp
@@ -370,9 +370,13 @@ enum par_exception_kind {
 
 class par_tactical : public or_else_tactical {
 
+	std::string        ex_msg;
+	unsigned           error_code;
 
 public:
-    par_tactical(unsigned num, tactic * const * ts):or_else_tactical(num, ts) {}
+    par_tactical(unsigned num, tactic * const * ts):or_else_tactical(num, ts) {
+		error_code = 0;
+	}
     ~par_tactical() override {}
 
     
@@ -404,19 +408,15 @@ public:
 
         unsigned finished_id       = UINT_MAX;
         par_exception_kind ex_kind = DEFAULT_EX;
-        std::string        ex_msg;
-        unsigned           error_code = 0;
-        std::mutex         mux;
-        int num_threads = static_cast<int>(sz);
 
-        auto worker_thread = [&](int i) {
-            goal_ref_buffer     _result;
-            
+        std::mutex         mux;
+
+        auto worker_thread = [&](unsigned i) {
+            goal_ref_buffer     _result;                        
             goal_ref in_copy = in_copies[i];
             tactic & t = *(ts.get(i));
             
             try {
-                // IF_VERBOSE(0, verbose_stream() << "start\n");
                 t(in_copy, _result);
                 bool first = false;
                 {
@@ -428,11 +428,11 @@ public:
                 }                
                 if (first) {
                     for (unsigned j = 0; j < sz; j++) {
-                        if (static_cast<unsigned>(i) != j) {
+                        if (i != j) {
                             managers[j]->limit().cancel();
                         }
                     }
-                    IF_VERBOSE(0, verbose_stream() << "first\n");
+                    
                     ast_translation translator(*(managers[i]), m, false);
                     for (goal* g : _result) {
                         result.push_back(g->translate(translator));
@@ -461,13 +461,13 @@ public:
             }
         };
 
-        scoped_ptr_vector<std::thread> threads;
-        for (int i = 0; i < num_threads; ++i) {
-            int id = i;
-            threads.push_back(alloc(std::thread, [&]() { worker_thread(id); }));
+        vector<std::thread> threads(sz);
+
+        for (unsigned i = 0; i < sz; ++i) {
+            threads[i] = std::thread([&, i]() { worker_thread(i); });
         }
-        for (int i = 0; i < num_threads; ++i) {
-            threads[i]->join();
+        for (unsigned i = 0; i < sz; ++i) {
+            threads[i].join();
         }
         
         if (finished_id == UINT_MAX) {
@@ -562,7 +562,7 @@ public:
             std::string  ex_msg;
             std::mutex mux;
 
-            auto worker_thread = [&](int i) {
+            auto worker_thread = [&](unsigned i) {
                 ast_manager & new_m = *(managers[i]);
                 goal_ref new_g = g_copies[i];
 
@@ -663,13 +663,11 @@ public:
                 }
             };
 
-            std::vector<std::thread> threads;
-            int num_threads = static_cast<int>(r1_size);
-            for (int i = 0; i < num_threads; ++i) {
-                int id = i;
-                threads.emplace_back([&]() { worker_thread(id); });
+            vector<std::thread> threads(r1_size);
+            for (unsigned i = 0; i < r1_size; ++i) {
+                threads[i] = std::thread([&, i]() { worker_thread(i); });
             }
-            for (int i = 0; i < num_threads; ++i) {
+            for (unsigned i = 0; i < r1_size; ++i) {
                 threads[i].join();
             }
             
diff --git a/src/util/rlimit.cpp b/src/util/rlimit.cpp
index 69b1cd11c..b99b09102 100644
--- a/src/util/rlimit.cpp
+++ b/src/util/rlimit.cpp
@@ -20,6 +20,8 @@ Revision History:
 #include "util/common_msgs.h"
 
 
+static std::mutex g_rlimit_mux;
+
 reslimit::reslimit():
     m_cancel(0),
     m_suspend(false),
@@ -70,34 +72,34 @@ char const* reslimit::get_cancel_msg() const {
 }
 
 void reslimit::push_child(reslimit* r) {
-    std::lock_guard<std::mutex> lock(m_mux);
+    std::lock_guard<std::mutex> lock(g_rlimit_mux);
     m_children.push_back(r);    
 }
 
 void reslimit::pop_child() {
-    std::lock_guard<std::mutex> lock(m_mux);
+    std::lock_guard<std::mutex> lock(g_rlimit_mux);
     m_children.pop_back();    
 }
 
 void reslimit::cancel() {
-    std::lock_guard<std::mutex> lock(m_mux);
+    std::lock_guard<std::mutex> lock(g_rlimit_mux);
     set_cancel(m_cancel+1);    
 }
 
 
 void reslimit::reset_cancel() {
-    std::lock_guard<std::mutex> lock(m_mux);
+    std::lock_guard<std::mutex> lock(g_rlimit_mux);
     set_cancel(0);    
 }
 
 void reslimit::inc_cancel() {
-    std::lock_guard<std::mutex> lock(m_mux);
+    std::lock_guard<std::mutex> lock(g_rlimit_mux);
     set_cancel(m_cancel+1);    
 }
 
 
 void reslimit::dec_cancel() {
-    std::lock_guard<std::mutex> lock(m_mux);
+    std::lock_guard<std::mutex> lock(g_rlimit_mux);
     if (m_cancel > 0) {
         set_cancel(m_cancel-1);
     }