diff --git a/src/ast/rewriter/bv_bounds.cpp b/src/ast/rewriter/bv_bounds.cpp
index f30df7890..1658833a8 100644
--- a/src/ast/rewriter/bv_bounds.cpp
+++ b/src/ast/rewriter/bv_bounds.cpp
@@ -628,7 +628,7 @@ bool bv_bounds::is_sat_core(app * v) {
     numeral new_hi = lower - one;
     numeral ptr = lower;
     if (has_neg_intervals) {
-        SASSERT(negative_intervals != NULL);
+        SASSERT(negative_intervals != nullptr);
         std::sort(negative_intervals->begin(), negative_intervals->end(), interval_comp);
         intervals::const_iterator e = negative_intervals->end();
         for (intervals::const_iterator i = negative_intervals->begin(); i != e; ++i) {
diff --git a/src/ast/rewriter/bv_trailing.cpp b/src/ast/rewriter/bv_trailing.cpp
index 433ef6f66..f7c9e121e 100644
--- a/src/ast/rewriter/bv_trailing.cpp
+++ b/src/ast/rewriter/bv_trailing.cpp
@@ -364,7 +364,7 @@ struct bv_trailing::imp {
     }
 
     void reset_cache(const unsigned condition) {
-        SASSERT(m_count_cache[0] == NULL);
+        SASSERT(m_count_cache[0] == nullptr);
         for (unsigned i = 1; i <= TRAILING_DEPTH; ++i) {
             if (m_count_cache[i] == nullptr) continue;
             TRACE("bv-trailing", tout << "may reset cache " << i << " " << condition <<  "\n";);
diff --git a/src/muz/fp/datalog_parser.cpp b/src/muz/fp/datalog_parser.cpp
index cc0a60335..0724d471a 100644
--- a/src/muz/fp/datalog_parser.cpp
+++ b/src/muz/fp/datalog_parser.cpp
@@ -101,7 +101,7 @@ public:
         resize_data(0);
 #if _WINDOWS
         errno_t err = fopen_s(&m_file, fname, "rb");
-        m_ok = (m_file != NULL) && (err == 0);
+        m_ok = (m_file != nullptr) && (err == 0);
 #else
         m_file = fopen(fname, "rb");
         m_ok = (m_file != nullptr);
diff --git a/src/smt/theory_recfun.h b/src/smt/theory_recfun.h
index 95b20eb4b..c233da059 100644
--- a/src/smt/theory_recfun.h
+++ b/src/smt/theory_recfun.h
@@ -69,7 +69,7 @@ namespace smt {
             recfun::case_def const * m_cdef;
             ptr_vector<expr>        m_args;
 
-            body_expansion(recfun::util& u, app * n) : m_pred(n), m_cdef(0), m_args() {
+            body_expansion(recfun::util& u, app * n) : m_pred(n), m_cdef(nullptr), m_args() {
                 m_cdef = &u.get_case_def(n);
                 m_args.append(n->get_num_args(), n->get_args());
             }
diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index 3ee780366..444de1e18 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -505,7 +505,7 @@ namespace smt {
         app * a = mk_fresh_const(name.c_str(), int_sort);
 
         ctx.internalize(a, false);
-        SASSERT(ctx.get_enode(a) != NULL);
+        SASSERT(ctx.get_enode(a) != nullptr);
         SASSERT(ctx.e_internalized(a));
         ctx.mark_as_relevant(a);
         // I'm assuming that this combination will do the correct thing in the integer theory.
@@ -544,7 +544,7 @@ namespace smt {
 
         // I have a hunch that this may not get internalized for free...
         ctx.internalize(a, false);
-        SASSERT(ctx.get_enode(a) != NULL);
+        SASSERT(ctx.get_enode(a) != nullptr);
         SASSERT(ctx.e_internalized(a));
         // this might help??
         mk_var(ctx.get_enode(a));
@@ -566,7 +566,7 @@ namespace smt {
         m_trail.push_back(a);
 
         ctx.internalize(a, false);
-        SASSERT(ctx.get_enode(a) != NULL);
+        SASSERT(ctx.get_enode(a) != nullptr);
         SASSERT(ctx.e_internalized(a));
         mk_var(ctx.get_enode(a));
         m_basicstr_axiom_todo.push_back(ctx.get_enode(a));
@@ -617,7 +617,7 @@ namespace smt {
         app * a = mk_fresh_const(name.c_str(), string_sort);
 
         ctx.internalize(a, false);
-        SASSERT(ctx.get_enode(a) != NULL);
+        SASSERT(ctx.get_enode(a) != nullptr);
         // this might help??
         mk_var(ctx.get_enode(a));
 
@@ -710,7 +710,7 @@ namespace smt {
      * Returns the simplified concatenation of two expressions,
      * where either both expressions are constant strings
      * or one expression is the empty string.
-     * If this precondition does not hold, the function returns NULL.
+     * If this precondition does not hold, the function returns nullptr.
      * (note: this function was strTheory::Concat())
      */
     expr * theory_str::mk_concat_const_str(expr * n1, expr * n2) {
@@ -2148,7 +2148,7 @@ namespace smt {
     // Evaluates the concatenation (n1 . n2) with respect to
     // the current equivalence classes of n1 and n2.
     // Returns a constant string expression representing this concatenation
-    // if one can be determined, or NULL if this is not possible.
+    // if one can be determined, or nullptr if this is not possible.
     expr * theory_str::eval_concat(expr * n1, expr * n2) {
         bool n1HasEqcValue = false;
         bool n2HasEqcValue = false;
@@ -2222,7 +2222,7 @@ namespace smt {
 
             for (enode_vector::iterator parent_it = current_parents.begin(); parent_it != current_parents.end(); ++parent_it) {
                 enode * e_parent = *parent_it;
-                SASSERT(e_parent != NULL);
+                SASSERT(e_parent != nullptr);
 
                 app * a_parent = e_parent->get_owner();
                 TRACE("str", tout << "considering parent " << mk_ismt2_pp(a_parent, m) << std::endl;);
@@ -5575,7 +5575,7 @@ namespace smt {
                   tout << " " << mk_pp(el, m);
               }
               tout << std::endl;
-              if (constStrAst == NULL) {
+              if (constStrAst == nullptr) {
                   tout << "constStrAst = NULL" << std::endl;
               } else {
                   tout << "constStrAst = " << mk_pp(constStrAst, m) << std::endl;
@@ -7787,7 +7787,7 @@ namespace smt {
                             generate_mutual_exclusion(arrangement_disjunction);
                         }
                     } /* (arg1Len != 1 || arg2Len != 1) */
-                } /* if (Concat(arg1, arg2) == NULL) */
+                } /* if (Concat(arg1, arg2) == nullptr) */
             }
         }
     }
@@ -10417,12 +10417,12 @@ namespace smt {
                 }
             } // foreach(term in str_in_re_terms)
 
-            eautomaton * aut_inter = NULL;
+            eautomaton * aut_inter = nullptr;
             CTRACE("str", !intersect_constraints.empty(), tout << "check intersection of automata constraints for " << mk_pp(str, m) << std::endl;);
             for (svector<regex_automaton_under_assumptions>::iterator aut_it = intersect_constraints.begin();
                     aut_it != intersect_constraints.end(); ++aut_it) {
                 regex_automaton_under_assumptions aut = *aut_it;
-                if (aut_inter == NULL) {
+                if (aut_inter == nullptr) {
                     // start somewhere
                     aut_inter = aut.get_automaton();
                     used_intersect_constraints.push_back(aut);
@@ -10472,7 +10472,7 @@ namespace smt {
                     }
                 }
             } // foreach(entry in intersect_constraints)
-            if (aut_inter != NULL) {
+            if (aut_inter != nullptr) {
                 aut_inter->compress();
             }
             TRACE("str", tout << "intersected " << used_intersect_constraints.size() << " constraints" << std::endl;);
@@ -10503,7 +10503,7 @@ namespace smt {
             }
             conflict_lhs = mk_and(conflict_terms);
 
-            if (used_intersect_constraints.size() > 1 && aut_inter != NULL) {
+            if (used_intersect_constraints.size() > 1 && aut_inter != nullptr) {
                 // check whether the intersection is only the empty string
                 unsigned initial_state = aut_inter->init();
                 if (aut_inter->final_states().size() == 1 && aut_inter->is_final_state(initial_state)) {
@@ -10521,7 +10521,7 @@ namespace smt {
                 }
             }
 
-            if (aut_inter != NULL && aut_inter->is_empty()) {
+            if (aut_inter != nullptr && aut_inter->is_empty()) {
                 TRACE("str", tout << "product automaton is empty; asserting conflict clause" << std::endl;);
                 expr_ref conflict_clause(m.mk_not(mk_and(conflict_terms)), m);
                 assert_axiom(conflict_clause);
@@ -11809,7 +11809,7 @@ namespace smt {
             expr_ref assertL(mk_and(and_items_LHS), m);
             SASSERT(assertL);
             expr * finalAxiom = m.mk_or(m.mk_not(assertL), lenTestAssert.get());
-            SASSERT(finalAxiom != NULL);
+            SASSERT(finalAxiom != nullptr);
             TRACE("str", tout << "crash avoidance finalAxiom: " << mk_pp(finalAxiom, m) << std::endl;);
             return finalAxiom;
         } else {
@@ -12095,7 +12095,7 @@ namespace smt {
                 lenTester_fvar_map.insert(indicator, freeVar);
 
                 expr * lenTestAssert = gen_len_test_options(freeVar, indicator, testNum);
-                SASSERT(lenTestAssert != NULL);
+                SASSERT(lenTestAssert != nullptr);
                 return lenTestAssert;
             } else {
                 TRACE("str", tout << "found previous in-scope length assertions" << std::endl;);
@@ -12201,7 +12201,7 @@ namespace smt {
                         testNum = i + 1;
                     }
                     expr * lenTestAssert = gen_len_test_options(freeVar, indicator, testNum);
-                    SASSERT(lenTestAssert != NULL);
+                    SASSERT(lenTestAssert != nullptr);
                     return lenTestAssert;
                 } else {
                     // if we are performing automata-based reasoning and the term associated with
diff --git a/src/tactic/smtlogics/qfufbv_tactic.cpp b/src/tactic/smtlogics/qfufbv_tactic.cpp
index 38eaa25fb..8dd77cba2 100644
--- a/src/tactic/smtlogics/qfufbv_tactic.cpp
+++ b/src/tactic/smtlogics/qfufbv_tactic.cpp
@@ -121,7 +121,7 @@ private:
             tactic_ref t = mk_qfaufbv_tactic(m_m, m_p);
             sat = mk_tactic2solver(m_m, t.get(), m_p);
         }
-        SASSERT(sat != NULL);
+        SASSERT(sat != nullptr);
         sat->set_produce_models(true);
         return sat;
     }
diff --git a/src/util/array.h b/src/util/array.h
index cf82e123c..9f0321777 100644
--- a/src/util/array.h
+++ b/src/util/array.h
@@ -154,7 +154,7 @@ public:
         return static_cast<unsigned>(reinterpret_cast<size_t *>(m_data)[SIZE_IDX]); 
     }
     
-    bool empty() const { return m_data == 0; }
+    bool empty() const { return m_data == nullptr; }
 
     T & operator[](unsigned idx) { 
         SASSERT(idx < size()); 
diff --git a/src/util/scoped_timer.cpp b/src/util/scoped_timer.cpp
index 9850699be..871356d25 100644
--- a/src/util/scoped_timer.cpp
+++ b/src/util/scoped_timer.cpp
@@ -146,7 +146,7 @@ struct scoped_timer::imp {
 #if defined(_WINDOWS) || defined(_CYGWIN)
         m_first = true;
         CreateTimerQueueTimer(&m_timer,
-                              NULL,
+                              nullptr,
                               abort_proc,
                               this,
                               0,
@@ -180,9 +180,9 @@ struct scoped_timer::imp {
         m_ms = ms;
         m_initialized = false;
         m_signal_sent = false;
-        ENSURE(pthread_mutex_init(&m_mutex, NULL) == 0);
-        ENSURE(pthread_cond_init(&m_cond, NULL) == 0);
-        ENSURE(pthread_create(&m_thread_id, NULL, &thread_func, this) == 0);
+        ENSURE(pthread_mutex_init(&m_mutex, nullptr) == 0);
+        ENSURE(pthread_cond_init(&m_cond, nullptr) == 0);
+        ENSURE(pthread_create(&m_thread_id, nullptr, &thread_func, this) == 0);
 #else
     // Other platforms
 #endif
@@ -190,7 +190,7 @@ struct scoped_timer::imp {
 
     ~imp() {
 #if defined(_WINDOWS) || defined(_CYGWIN)
-        DeleteTimerQueueTimer(NULL,
+        DeleteTimerQueueTimer(nullptr,
                               m_timer,
                               INVALID_HANDLE_VALUE);
 #elif defined(__APPLE__) && defined(__MACH__)
@@ -242,7 +242,7 @@ struct scoped_timer::imp {
         // Perform signal outside of lock to avoid waking timing thread twice.
         pthread_cond_signal(&m_cond);
 
-        pthread_join(m_thread_id, NULL);
+        pthread_join(m_thread_id, nullptr);
         pthread_cond_destroy(&m_cond);
         pthread_mutex_destroy(&m_mutex);
 #else
diff --git a/src/util/warning.cpp b/src/util/warning.cpp
index 1e9f8a484..5ffc38527 100644
--- a/src/util/warning.cpp
+++ b/src/util/warning.cpp
@@ -88,7 +88,7 @@ void format2ostream(std::ostream & out, char const* msg, va_list args) {
 #ifdef _WINDOWS
     size_t msg_len = _vscprintf(msg, args_copy);
 #else
-    size_t msg_len = vsnprintf(NULL, 0, msg, args_copy);
+    size_t msg_len = vsnprintf(nullptr, 0, msg, args_copy);
 #endif
     va_end(args_copy);