diff --git a/src/ackermannization/lackr.h b/src/ackermannization/lackr.h
index 98c1988f7..049fb8bb3 100644
--- a/src/ackermannization/lackr.h
+++ b/src/ackermannization/lackr.h
@@ -102,7 +102,7 @@ class lackr {
         //
         // Introduce congruence ackermann lemma for the two given terms.
         //
-        bool ackr(app * const t1, app * const t2);
+        bool ackr(app * t1, app * t2);
 
         //
         // Introduce the ackermann lemma for each pair of terms.
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/math/simplex/model_based_opt.cpp b/src/math/simplex/model_based_opt.cpp
index 8a771e07c..4053c41b7 100644
--- a/src/math/simplex/model_based_opt.cpp
+++ b/src/math/simplex/model_based_opt.cpp
@@ -606,7 +606,7 @@ namespace opt {
         }
     }
 
-    void model_based_opt::mk_coeffs_without(vector<var>& dst, vector<var> const src, unsigned x) {
+    void model_based_opt::mk_coeffs_without(vector<var>& dst, vector<var> const& src, unsigned x) {
         for (var const & v : src) {
             if (v.m_id != x) dst.push_back(v);
         }
diff --git a/src/math/simplex/model_based_opt.h b/src/math/simplex/model_based_opt.h
index e52d0cfe0..30442fc58 100644
--- a/src/math/simplex/model_based_opt.h
+++ b/src/math/simplex/model_based_opt.h
@@ -132,7 +132,7 @@ namespace opt {
 
         void normalize(unsigned row_id);
 
-        void mk_coeffs_without(vector<var>& dst, vector<var> const src, unsigned x);
+        void mk_coeffs_without(vector<var>& dst, vector<var> const& src, unsigned x);
 
         unsigned new_row();
 
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/muz/rel/dl_compiler.h b/src/muz/rel/dl_compiler.h
index d7bdcad34..6bc2a819f 100644
--- a/src/muz/rel/dl_compiler.h
+++ b/src/muz/rel/dl_compiler.h
@@ -148,7 +148,7 @@ namespace datalog {
         void make_join(reg_idx t1, reg_idx t2, const variable_intersection & vars, reg_idx & result, 
             bool reuse_t1, instruction_block & acc);
         void make_min(reg_idx source, reg_idx & target, const unsigned_vector & group_by_cols,
-            const unsigned min_col, instruction_block & acc);
+            unsigned min_col, instruction_block & acc);
         void make_join_project(reg_idx t1, reg_idx t2, const variable_intersection & vars, 
             const unsigned_vector & removed_cols, reg_idx & result, bool reuse_t1, instruction_block & acc);
         void make_filter_interpreted_and_project(reg_idx src, app_ref & cond,
diff --git a/src/muz/rel/dl_instruction.h b/src/muz/rel/dl_instruction.h
index 6e0b7bfe5..918763a95 100644
--- a/src/muz/rel/dl_instruction.h
+++ b/src/muz/rel/dl_instruction.h
@@ -285,7 +285,7 @@ namespace datalog {
             const unsigned * cols1, const unsigned * cols2, unsigned removed_col_cnt, 
             const unsigned * removed_cols, reg_idx result);
         static instruction * mk_min(reg_idx source, reg_idx target, const unsigned_vector & group_by_cols,
-            const unsigned min_col);
+            unsigned min_col);
         static instruction * mk_rename(reg_idx src, unsigned cycle_len, const unsigned * permutation_cycle, 
             reg_idx tgt);
         static instruction * mk_filter_by_negation(reg_idx tgt, reg_idx neg_rel, unsigned col_cnt,
diff --git a/src/sat/sat_simplifier_params.pyg b/src/sat/sat_simplifier_params.pyg
index 3757aad2d..60ca4a49b 100644
--- a/src/sat/sat_simplifier_params.pyg
+++ b/src/sat/sat_simplifier_params.pyg
@@ -2,7 +2,7 @@ def_module_params(module_name='sat',
                   class_name='sat_simplifier_params',
                   export=True,
                   params=(('bce',  BOOL, False, 'eliminate blocked clauses'),
-                          ('abce', BOOL, False, 'eliminate blocked clauses using asymmmetric literals'),
+                          ('abce', BOOL, False, 'eliminate blocked clauses using asymmetric literals'),
                           ('cce',  BOOL, False, 'eliminate covered clauses'),
                           ('ate',  BOOL, True,  'asymmetric tautology elimination'),
                           ('acce', BOOL, False, 'eliminate covered clauses using asymmetric added literals'),
@@ -11,7 +11,7 @@ def_module_params(module_name='sat',
 	                  ('bce_delay', UINT, 2, 'delay eliminate blocked clauses until simplification round'),
                           ('retain_blocked_clauses', BOOL, True, 'retain blocked clauses as lemmas'),
                           ('blocked_clause_limit', UINT, 100000000, 'maximum number of literals visited during blocked clause elimination'),
-                          ('override_incremental', BOOL, False, 'override incemental safety gaps. Enable elimination of blocked clauses and variables even if solver is reused'),
+                          ('override_incremental', BOOL, False, 'override incremental safety gaps. Enable elimination of blocked clauses and variables even if solver is reused'),
                           ('resolution.limit', UINT, 500000000, 'approx. maximum number of literals visited during variable elimination'),
                           ('resolution.occ_cutoff', UINT, 10, 'first cutoff (on number of positive/negative occurrences) for Boolean variable elimination'),
                           ('resolution.occ_cutoff_range1', UINT, 8, 'second cutoff (number of positive/negative occurrences) for Boolean variable elimination, for problems containing less than res_cls_cutoff1 clauses'),
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..18267c4fc 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) {
@@ -1661,53 +1661,66 @@ namespace smt {
         }
     }
 
+    //  (str.replace s t t') is the string obtained by replacing the first occurrence
+    //  of t in s, if any, by t'. Note that if t is empty, the result is to prepend
+    //  t' to s; also, if t does not occur in s then the result is s.
     void theory_str::instantiate_axiom_Replace(enode * e) {
         context & ctx = get_context();
         ast_manager & m = get_manager();
 
-        app * expr = e->get_owner();
-        if (axiomatized_terms.contains(expr)) {
-            TRACE("str", tout << "already set up Replace axiom for " << mk_pp(expr, m) << std::endl;);
+        app * ex = e->get_owner();
+        if (axiomatized_terms.contains(ex)) {
+            TRACE("str", tout << "already set up Replace axiom for " << mk_pp(ex, m) << std::endl;);
             return;
         }
-        axiomatized_terms.insert(expr);
+        axiomatized_terms.insert(ex);
 
-        TRACE("str", tout << "instantiate Replace axiom for " << mk_pp(expr, m) << std::endl;);
+        TRACE("str", tout << "instantiate Replace axiom for " << mk_pp(ex, m) << std::endl;);
 
         expr_ref x1(mk_str_var("x1"), m);
         expr_ref x2(mk_str_var("x2"), m);
         expr_ref i1(mk_int_var("i1"), m);
         expr_ref result(mk_str_var("result"), m);
 
+        expr * replaceS;
+        expr * replaceT;
+        expr * replaceTPrime;
+        u.str.is_replace(ex, replaceS, replaceT, replaceTPrime);
+
+        // t empty => result = (str.++ t' s)
+        expr_ref emptySrcAst(ctx.mk_eq_atom(replaceT, mk_string("")), m);
+        expr_ref prependTPrimeToS(ctx.mk_eq_atom(result, mk_concat(replaceTPrime, replaceS)), m);
+
         // condAst = Contains(args[0], args[1])
-        expr_ref condAst(mk_contains(expr->get_arg(0), expr->get_arg(1)), m);
+        expr_ref condAst(mk_contains(ex->get_arg(0), ex->get_arg(1)), m);
         // -----------------------
         // true branch
         expr_ref_vector thenItems(m);
         //  args[0] = x1 . args[1] . x2
-        thenItems.push_back(ctx.mk_eq_atom(expr->get_arg(0), mk_concat(x1, mk_concat(expr->get_arg(1), x2))));
+        thenItems.push_back(ctx.mk_eq_atom(ex->get_arg(0), mk_concat(x1, mk_concat(ex->get_arg(1), x2))));
         //  i1 = |x1|
         thenItems.push_back(ctx.mk_eq_atom(i1, mk_strlen(x1)));
         //  args[0]  = x3 . x4 /\ |x3| = |x1| + |args[1]| - 1 /\ ! contains(x3, args[1])
         expr_ref x3(mk_str_var("x3"), m);
         expr_ref x4(mk_str_var("x4"), m);
-        expr_ref tmpLen(m_autil.mk_add(i1, mk_strlen(expr->get_arg(1)), mk_int(-1)), m);
-        thenItems.push_back(ctx.mk_eq_atom(expr->get_arg(0), mk_concat(x3, x4)));
+        expr_ref tmpLen(m_autil.mk_add(i1, mk_strlen(ex->get_arg(1)), mk_int(-1)), m);
+        thenItems.push_back(ctx.mk_eq_atom(ex->get_arg(0), mk_concat(x3, x4)));
         thenItems.push_back(ctx.mk_eq_atom(mk_strlen(x3), tmpLen));
-        thenItems.push_back(mk_not(m, mk_contains(x3, expr->get_arg(1))));
-        thenItems.push_back(ctx.mk_eq_atom(result, mk_concat(x1, mk_concat(expr->get_arg(2), x2))));
+        thenItems.push_back(mk_not(m, mk_contains(x3, ex->get_arg(1))));
+        thenItems.push_back(ctx.mk_eq_atom(result, mk_concat(x1, mk_concat(ex->get_arg(2), x2))));
         // -----------------------
         // false branch
-        expr_ref elseBranch(ctx.mk_eq_atom(result, expr->get_arg(0)), m);
+        expr_ref elseBranch(ctx.mk_eq_atom(result, ex->get_arg(0)), m);
 
         th_rewriter rw(m);
 
-        expr_ref breakdownAssert(m.mk_ite(condAst, m.mk_and(thenItems.size(), thenItems.c_ptr()), elseBranch), m);
+        expr_ref breakdownAssert(m.mk_ite(emptySrcAst, prependTPrimeToS,
+                m.mk_ite(condAst, mk_and(thenItems), elseBranch)), m);
         expr_ref breakdownAssert_rw(breakdownAssert, m);
         rw(breakdownAssert_rw);
         assert_axiom(breakdownAssert_rw);
 
-        expr_ref reduceToResult(ctx.mk_eq_atom(expr, result), m);
+        expr_ref reduceToResult(ctx.mk_eq_atom(ex, result), m);
         expr_ref reduceToResult_rw(reduceToResult, m);
         rw(reduceToResult_rw);
         assert_axiom(reduceToResult_rw);
@@ -2148,7 +2161,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 +2235,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 +5588,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 +7800,7 @@ namespace smt {
                             generate_mutual_exclusion(arrangement_disjunction);
                         }
                     } /* (arg1Len != 1 || arg2Len != 1) */
-                } /* if (Concat(arg1, arg2) == NULL) */
+                } /* if (Concat(arg1, arg2) == nullptr) */
             }
         }
     }
@@ -10417,12 +10430,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 +10485,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 +10516,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 +10534,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 +11822,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 +12108,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 +12214,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/mpn.h b/src/util/mpn.h
index a5d3c30d8..ea20fc42b 100644
--- a/src/util/mpn.h
+++ b/src/util/mpn.h
@@ -37,29 +37,29 @@ public:
     mpn_manager();
     ~mpn_manager();
 
-    int compare(mpn_digit const * a, size_t const lnga,
-                mpn_digit const * b, size_t const lngb) const;
+    int compare(mpn_digit const * a, size_t lnga,
+                mpn_digit const * b, size_t lngb) const;
 
-    bool add(mpn_digit const * a, size_t const lnga,
-             mpn_digit const * b, size_t const lngb,
-             mpn_digit *c, size_t const lngc_alloc,
+    bool add(mpn_digit const * a, size_t lnga,
+             mpn_digit const * b, size_t lngb,
+             mpn_digit *c, size_t lngc_alloc,
              size_t * plngc) const;
 
-    bool sub(mpn_digit const * a, size_t const lnga,
-             mpn_digit const * b, size_t const lngb,
+    bool sub(mpn_digit const * a, size_t lnga,
+             mpn_digit const * b, size_t lngb,
              mpn_digit * c, mpn_digit * pborrow) const;
 
-    bool mul(mpn_digit const * a, size_t const lnga,
-             mpn_digit const * b, size_t const lngb,
+    bool mul(mpn_digit const * a, size_t lnga,
+             mpn_digit const * b, size_t lngb,
              mpn_digit * c) const;
 
-    bool div(mpn_digit const * numer, size_t const lnum,
-             mpn_digit const * denom, size_t const lden,
+    bool div(mpn_digit const * numer, size_t lnum,
+             mpn_digit const * denom, size_t lden,
              mpn_digit * quot,
              mpn_digit * rem);
 
-    char * to_string(mpn_digit const * a, size_t const lng,
-                     char * buf, size_t const lbuf) const;
+    char * to_string(mpn_digit const * a, size_t lng,
+                     char * buf, size_t lbuf) const;
 private:
     #ifdef _AMD64_
     class  mpn_sbuffer : public sbuffer<mpn_digit> {
@@ -88,29 +88,29 @@ private:
 
     static const mpn_digit zero;
     mpn_sbuffer u, v, t_ms, t_ab;
-    void display_raw(std::ostream & out, mpn_digit const * a, size_t const lng) const;
+    void display_raw(std::ostream & out, mpn_digit const * a, size_t lng) const;
 
-    size_t div_normalize(mpn_digit const * numer, size_t const lnum,
-                         mpn_digit const * denom, size_t const lden,
+    size_t div_normalize(mpn_digit const * numer, size_t lnum,
+                         mpn_digit const * denom, size_t lden,
                          mpn_sbuffer & n_numer,
                          mpn_sbuffer & n_denom) const;
 
     void div_unnormalize(mpn_sbuffer & numer, mpn_sbuffer & denom,
-                         size_t const d, mpn_digit * rem) const;
+                         size_t d, mpn_digit * rem) const;
 
-    bool div_1(mpn_sbuffer & numer, mpn_digit const denom,
+    bool div_1(mpn_sbuffer & numer, mpn_digit denom,
                mpn_digit * quot) const;
 
     bool div_n(mpn_sbuffer & numer, mpn_sbuffer const & denom,
                mpn_digit * quot, mpn_digit * rem,
                mpn_sbuffer & ms, mpn_sbuffer & ab) const;
 
-    void trace(mpn_digit const * a, size_t const lnga, 
-               mpn_digit const * b, size_t const lngb, 
+    void trace(mpn_digit const * a, size_t lnga,
+               mpn_digit const * b, size_t lngb,
                const char * op) const;
 
-    void trace(mpn_digit const * a, size_t const lnga) const;
-    void trace_nl(mpn_digit const * a, size_t const lnga) const;
+    void trace(mpn_digit const * a, size_t lnga) const;
+    void trace_nl(mpn_digit const * a, size_t lnga) const;
 };
 
 #endif
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);