diff --git a/src/ast/expr2polynomial.cpp b/src/ast/expr2polynomial.cpp
index ea37730cf..25ece60ab 100644
--- a/src/ast/expr2polynomial.cpp
+++ b/src/ast/expr2polynomial.cpp
@@ -23,6 +23,7 @@ Notes:
 #include "ast/ast_smt2_pp.h"
 #include "util/z3_exception.h"
 #include "util/common_msgs.h"
+#include <atomic>
 
 struct expr2polynomial::imp {
     struct frame {
@@ -51,7 +52,7 @@ struct expr2polynomial::imp {
 
     bool                               m_use_var_idxs;
 
-    volatile bool                      m_cancel;
+    std::atomic<bool>                  m_cancel;
 
     imp(expr2polynomial & w, ast_manager & am, polynomial::manager & pm, expr2var * e2v, bool use_var_idxs):
         m_wrapper(w),
diff --git a/src/sat/sat_parallel.cpp b/src/sat/sat_parallel.cpp
index 03fff2b58..5fb07ef3c 100644
--- a/src/sat/sat_parallel.cpp
+++ b/src/sat/sat_parallel.cpp
@@ -100,11 +100,9 @@ namespace sat {
 
     void parallel::init_solvers(solver& s, unsigned num_extra_solvers) {
         unsigned num_threads = num_extra_solvers + 1;
-        m_solvers.resize(num_extra_solvers);
+        m_solvers.init(num_extra_solvers);
+        m_limits.init(num_extra_solvers);
         symbol saved_phase = s.m_params.get_sym("phase", symbol("caching"));
-        for (unsigned i = 0; i < num_extra_solvers; ++i) {        
-            m_limits.push_back(reslimit());
-        }
         
         for (unsigned i = 0; i < num_extra_solvers; ++i) {
             s.m_params.set_uint("random_seed", s.m_rand());
diff --git a/src/solver/combined_solver.cpp b/src/solver/combined_solver.cpp
index 267a22de0..4252d45c2 100644
--- a/src/solver/combined_solver.cpp
+++ b/src/solver/combined_solver.cpp
@@ -23,6 +23,7 @@ Notes:
 #include "ast/ast_pp.h"
 #include "solver/solver.h"
 #include "solver/combined_solver_params.hpp"
+#include <atomic>
 #define PS_VB_LVL 15
 
 /**
@@ -71,7 +72,7 @@ private:
 
     struct aux_timeout_eh : public event_handler {
         solver *        m_solver;
-        volatile bool   m_canceled;
+        std::atomic<bool> m_canceled;
         aux_timeout_eh(solver * s):m_solver(s), m_canceled(false) {}
         ~aux_timeout_eh() override {
             if (m_canceled) {                
diff --git a/src/solver/parallel_tactic.cpp b/src/solver/parallel_tactic.cpp
index 8e3c3bb97..c32648a44 100644
--- a/src/solver/parallel_tactic.cpp
+++ b/src/solver/parallel_tactic.cpp
@@ -47,6 +47,7 @@ tactic * mk_parallel_tactic(solver* s, params_ref const& p) {
 
 #else
 
+#include <atomic>
 #include <thread>
 #include <mutex>
 #include <cmath>
@@ -63,7 +64,7 @@ class parallel_tactic : public tactic {
         ptr_vector<solver_state>     m_tasks;
         ptr_vector<solver_state>     m_active;
         unsigned                     m_num_waiters;
-        volatile bool                m_shutdown;
+        std::atomic<bool>            m_shutdown;
 
         void inc_wait() {
             std::lock_guard<std::mutex> lock(m_mutex);
@@ -365,7 +366,7 @@ private:
     unsigned      m_branches;
     unsigned      m_backtrack_frequency;
     unsigned      m_conquer_delay;
-    volatile bool m_has_undef;
+    std::atomic<bool> m_has_undef;
     bool          m_allsat;
     unsigned      m_num_unsat;
     unsigned      m_last_depth;
diff --git a/src/util/debug.cpp b/src/util/debug.cpp
index dd9922344..4380a0548 100644
--- a/src/util/debug.cpp
+++ b/src/util/debug.cpp
@@ -21,11 +21,12 @@ Revision History:
 #include<unistd.h>
 #endif
 #include<iostream>
+#include "util/mutex.h"
 #include "util/str_hashtable.h"
 #include "util/z3_exception.h"
 #include "util/z3_version.h"
 
-static volatile bool g_enable_assertions = true;
+static atomic<bool> g_enable_assertions(true);
 
 void enable_assertions(bool f) {
     g_enable_assertions = f;
diff --git a/src/util/rlimit.h b/src/util/rlimit.h
index c69942af0..9be53cd55 100644
--- a/src/util/rlimit.h
+++ b/src/util/rlimit.h
@@ -19,6 +19,7 @@ Revision History:
 #pragma once
 
 #include "util/vector.h"
+#include <atomic>
 
 void initialize_rlimit();
 void finalize_rlimit();
@@ -28,7 +29,7 @@ void finalize_rlimit();
 */
 
 class reslimit {
-    volatile unsigned   m_cancel;
+    std::atomic<unsigned> m_cancel;
     bool            m_suspend;
     uint64_t        m_count;
     uint64_t        m_limit;
diff --git a/src/util/vector.h b/src/util/vector.h
index 5a913b580..592f49c26 100644
--- a/src/util/vector.h
+++ b/src/util/vector.h
@@ -133,8 +133,13 @@ public:
     }
 
     vector(SZ s) {
+        m_data = nullptr;
+        init(s);
+    }
+
+    void init(SZ s) {
+        SASSERT(m_data == nullptr;);
         if (s == 0) {
-            m_data = nullptr;
             return;
         }
         SZ * mem = reinterpret_cast<SZ*>(memory::allocate(sizeof(T) * s + sizeof(SZ) * 2));