diff --git a/src/analyses/ai.h b/src/analyses/ai.h
index 3c078d2a9bb..11b6d1bd992 100644
--- a/src/analyses/ai.h
+++ b/src/analyses/ai.h
@@ -12,12 +12,14 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_ANALYSES_AI_H
 #define CPROVER_ANALYSES_AI_H
 
-#include <map>
 #include <iosfwd>
+#include <map>
+#include <memory>
 
 #include <util/json.h>
 #include <util/xml.h>
 #include <util/expr.h>
+#include <util/make_unique.h>
 
 #include <goto-programs/goto_model.h>
 
@@ -334,7 +336,7 @@ class ai_baset
     const namespacet &ns)=0;
   virtual statet &get_state(locationt l)=0;
   virtual const statet &find_state(locationt l) const=0;
-  virtual statet* make_temporary_state(const statet &s)=0;
+  virtual std::unique_ptr<statet> make_temporary_state(const statet &s)=0;
 };
 
 // domainT is expected to be derived from ai_domain_baseT
@@ -400,9 +402,9 @@ class ait:public ai_baset
       static_cast<const domainT &>(src), from, to);
   }
 
-  statet *make_temporary_state(const statet &s) override
+  std::unique_ptr<statet> make_temporary_state(const statet &s) override
   {
-    return new domainT(static_cast<const domainT &>(s));
+    return util_make_unique<domainT>(static_cast<const domainT &>(s));
   }
 
   void fixedpoint(
diff --git a/src/analyses/goto_rw.cpp b/src/analyses/goto_rw.cpp
index 73b7a8c3520..7d9b8b42a63 100644
--- a/src/analyses/goto_rw.cpp
+++ b/src/analyses/goto_rw.cpp
@@ -9,8 +9,9 @@ Date: April 2010
 \*******************************************************************/
 
 
-#include <limits>
 #include <algorithm>
+#include <limits>
+#include <memory>
 
 #include <util/std_code.h>
 #include <util/std_expr.h>
@@ -19,6 +20,7 @@ Date: April 2010
 #include <util/endianness_map.h>
 #include <util/arith_tools.h>
 #include <util/simplify_expr.h>
+#include <util/make_unique.h>
 
 #include <goto-programs/goto_functions.h>
 
@@ -50,12 +52,12 @@ rw_range_sett::~rw_range_sett()
   for(rw_range_sett::objectst::iterator it=r_range_set.begin();
       it!=r_range_set.end();
       ++it)
-    delete it->second;
+    it->second=nullptr;
 
   for(rw_range_sett::objectst::iterator it=w_range_set.begin();
       it!=w_range_set.end();
       ++it)
-    delete it->second;
+    it->second=nullptr;
 }
 
 void rw_range_sett::output(std::ostream &out) const
@@ -462,15 +464,18 @@ void rw_range_sett::add(
   const range_spect &range_start,
   const range_spect &range_end)
 {
-  objectst::iterator entry=(mode==get_modet::LHS_W ? w_range_set : r_range_set).
-    insert(
-      std::pair<const irep_idt&, range_domain_baset*>(identifier, 0)).first;
-
-  if(entry->second==0)
-    entry->second=new range_domaint();
-
-  static_cast<range_domaint*>(entry->second)->push_back(
-    std::make_pair(range_start, range_end));
+  objectst::iterator entry=
+    (mode==get_modet::LHS_W?w_range_set:r_range_set)
+       .insert(
+         std::pair<const irep_idt &, std::unique_ptr<range_domain_baset>>(
+           identifier, nullptr))
+       .first;
+
+  if(entry->second==nullptr)
+    entry->second=util_make_unique<range_domaint>();
+
+  static_cast<range_domaint&>(*entry->second).push_back(
+    {range_start, range_end});
 }
 
 void rw_range_sett::get_objects_rec(
@@ -662,16 +667,18 @@ void rw_guarded_range_set_value_sett::add(
   const range_spect &range_start,
   const range_spect &range_end)
 {
-  objectst::iterator entry=(mode==get_modet::LHS_W ? w_range_set : r_range_set).
-    insert(
-      std::pair<const irep_idt&, range_domain_baset*>(identifier, 0)).first;
-
-  if(entry->second==0)
-    entry->second=new guarded_range_domaint();
-
-  static_cast<guarded_range_domaint*>(entry->second)->insert(
-    std::make_pair(range_start,
-                   std::make_pair(range_end, guard.as_expr())));
+  objectst::iterator entry=
+    (mode==get_modet::LHS_W?w_range_set:r_range_set)
+      .insert(
+        std::pair<const irep_idt &, std::unique_ptr<range_domain_baset>>(
+          identifier, nullptr))
+      .first;
+
+  if(entry->second==nullptr)
+    entry->second=util_make_unique<guarded_range_domaint>();
+
+  static_cast<guarded_range_domaint&>(*entry->second).insert(
+    {range_start, {range_end, guard.as_expr()}});
 }
 
 void goto_rw(goto_programt::const_targett target,
diff --git a/src/analyses/goto_rw.h b/src/analyses/goto_rw.h
index 06b7a7ab411..8dd43880f93 100644
--- a/src/analyses/goto_rw.h
+++ b/src/analyses/goto_rw.h
@@ -15,6 +15,7 @@ Date: April 2010
 #include <map>
 #include <ostream>
 #include <limits>
+#include <memory> // unique_ptr
 
 #include <util/guard.h>
 
@@ -83,10 +84,10 @@ class rw_range_sett
 {
 public:
   #ifdef USE_DSTRING
-  typedef std::map<irep_idt, range_domain_baset*> objectst;
+  typedef std::map<irep_idt, std::unique_ptr<range_domain_baset>> objectst;
   #else
-  typedef std::unordered_map<irep_idt, range_domain_baset*, string_hash>
-    objectst;
+  typedef std::unordered_map<
+    irep_idt, std::unique_ptr<range_domain_baset>, string_hash> objectst;
   #endif
 
   virtual ~rw_range_sett();
@@ -108,8 +109,8 @@ class rw_range_sett
 
   const range_domaint &get_ranges(objectst::const_iterator it) const
   {
-    assert(dynamic_cast<range_domaint*>(it->second)!=0);
-    return *static_cast<range_domaint*>(it->second);
+    PRECONDITION(dynamic_cast<range_domaint*>(it->second.get())!=nullptr);
+    return static_cast<const range_domaint &>(*it->second);
   }
 
   enum class get_modet { LHS_W, READ };
@@ -277,8 +278,9 @@ class rw_guarded_range_set_value_sett:public rw_range_set_value_sett
 
   const guarded_range_domaint &get_ranges(objectst::const_iterator it) const
   {
-    assert(dynamic_cast<guarded_range_domaint*>(it->second)!=0);
-    return *static_cast<guarded_range_domaint*>(it->second);
+    PRECONDITION(
+      dynamic_cast<guarded_range_domaint*>(it->second.get())!=nullptr);
+    return static_cast<const guarded_range_domaint &>(*it->second);
   }
 
   virtual void get_objects_rec(
diff --git a/src/analyses/local_may_alias.h b/src/analyses/local_may_alias.h
index b54cf4e9e88..f3d7a7b38c6 100644
--- a/src/analyses/local_may_alias.h
+++ b/src/analyses/local_may_alias.h
@@ -12,10 +12,11 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_ANALYSES_LOCAL_MAY_ALIAS_H
 #define CPROVER_ANALYSES_LOCAL_MAY_ALIAS_H
 
-#include <stack>
 #include <memory>
+#include <stack>
 
 #include <util/union_find.h>
+#include <util/make_unique.h>
 
 #include "locals.h"
 #include "dirty.h"
@@ -117,8 +118,7 @@ class local_may_alias_factoryt
     goto_functionst::function_mapt::const_iterator f_it2=
       goto_functions->function_map.find(fkt);
     assert(f_it2!=goto_functions->function_map.end());
-    return *(fkt_map[fkt]=std::unique_ptr<local_may_aliast>(
-              new local_may_aliast(f_it2->second)));
+    return *(fkt_map[fkt]=util_make_unique<local_may_aliast>(f_it2->second));
   }
 
   local_may_aliast &operator()(goto_programt::const_targett t)
diff --git a/src/analyses/reaching_definitions.cpp b/src/analyses/reaching_definitions.cpp
index 70ea10b79ca..a47c3cb4947 100644
--- a/src/analyses/reaching_definitions.cpp
+++ b/src/analyses/reaching_definitions.cpp
@@ -13,8 +13,11 @@ Date: February 2013
 /// Range-based reaching definitions analysis (following Field- Sensitive
 ///   Program Dependence Analysis, Litvak et al., FSE 2010)
 
+#include <memory>
+
 #include <util/pointer_offset_size.h>
 #include <util/prefix.h>
+#include <util/make_unique.h>
 
 #include <pointer-analysis/value_set_analysis_fi.h>
 
@@ -23,6 +26,15 @@ Date: February 2013
 
 #include "reaching_definitions.h"
 
+reaching_definitions_analysist::reaching_definitions_analysist(
+  const namespacet &_ns):
+    concurrency_aware_ait<rd_range_domaint>(),
+    ns(_ns)
+{
+}
+
+reaching_definitions_analysist::~reaching_definitions_analysist()=default;
+
 void rd_range_domaint::populate_cache(const irep_idt &identifier) const
 {
   assert(bv_container);
@@ -711,26 +723,16 @@ const rd_range_domaint::ranges_at_loct &rd_range_domaint::get(
     return entry->second;
 }
 
-reaching_definitions_analysist::~reaching_definitions_analysist()
-{
-  if(is_dirty)
-    delete is_dirty;
-  if(is_threaded)
-    delete is_threaded;
-  if(value_sets)
-    delete value_sets;
-}
-
 void reaching_definitions_analysist::initialize(
   const goto_functionst &goto_functions)
 {
-  value_set_analysis_fit *value_sets_=new value_set_analysis_fit(ns);
+  auto value_sets_=util_make_unique<value_set_analysis_fit>(ns);
   (*value_sets_)(goto_functions);
-  value_sets=value_sets_;
+  value_sets=std::move(value_sets_);
 
-  is_threaded=new is_threadedt(goto_functions);
+  is_threaded=util_make_unique<is_threadedt>(goto_functions);
 
-  is_dirty=new dirtyt(goto_functions);
+  is_dirty=util_make_unique<dirtyt>(goto_functions);
 
   concurrency_aware_ait<rd_range_domaint>::initialize(goto_functions);
 }
diff --git a/src/analyses/reaching_definitions.h b/src/analyses/reaching_definitions.h
index 2cc7d815fa3..88b20d4216b 100644
--- a/src/analyses/reaching_definitions.h
+++ b/src/analyses/reaching_definitions.h
@@ -240,14 +240,7 @@ class reaching_definitions_analysist:
 {
 public:
   // constructor
-  explicit reaching_definitions_analysist(const namespacet &_ns):
-    concurrency_aware_ait<rd_range_domaint>(),
-    ns(_ns),
-    value_sets(0),
-    is_threaded(0),
-    is_dirty(0)
-  {
-  }
+  explicit reaching_definitions_analysist(const namespacet &_ns);
 
   virtual ~reaching_definitions_analysist();
 
@@ -286,9 +279,9 @@ class reaching_definitions_analysist:
 
 protected:
   const namespacet &ns;
-  value_setst * value_sets;
-  is_threadedt * is_threaded;
-  dirtyt * is_dirty;
+  std::unique_ptr<value_setst> value_sets;
+  std::unique_ptr<is_threadedt> is_threaded;
+  std::unique_ptr<dirtyt> is_dirty;
 };
 
 #endif // CPROVER_ANALYSES_REACHING_DEFINITIONS_H
diff --git a/src/analyses/static_analysis.h b/src/analyses/static_analysis.h
index 17d8dced473..21d89367da5 100644
--- a/src/analyses/static_analysis.h
+++ b/src/analyses/static_analysis.h
@@ -16,10 +16,13 @@ Author: Daniel Kroening, kroening@kroening.com
 #error Deprecated, use ai.h instead
 #endif
 
-#include <map>
 #include <iosfwd>
+#include <map>
+#include <memory>
 #include <unordered_set>
 
+#include <util/make_unique.h>
+
 #include <goto-programs/goto_functions.h>
 
 // don't use me -- I am just a base class
@@ -252,7 +255,7 @@ class static_analysis_baset
   virtual void generate_state(locationt l)=0;
   virtual statet &get_state(locationt l)=0;
   virtual const statet &get_state(locationt l) const=0;
-  virtual statet* make_temporary_state(statet &s)=0;
+  virtual std::unique_ptr<statet> make_temporary_state(statet &s)=0;
 
   typedef domain_baset::expr_sett expr_sett;
 
@@ -331,9 +334,9 @@ class static_analysist:public static_analysis_baset
     return static_cast<T &>(a).merge(static_cast<const T &>(b), to);
   }
 
-  virtual statet *make_temporary_state(statet &s)
+  virtual std::unique_ptr<statet> make_temporary_state(statet &s)
   {
-    return new T(static_cast<T &>(s));
+    return util_make_unique<T>(static_cast<T &>(s));
   }
 
   virtual void generate_state(locationt l)
diff --git a/src/ansi-c/ansi_c_language.cpp b/src/ansi-c/ansi_c_language.cpp
index e4a005b7100..14428b475b8 100644
--- a/src/ansi-c/ansi_c_language.cpp
+++ b/src/ansi-c/ansi_c_language.cpp
@@ -139,9 +139,9 @@ void ansi_c_languaget::show_parse(std::ostream &out)
   parse_tree.output(out);
 }
 
-languaget *new_ansi_c_language()
+std::unique_ptr<languaget> new_ansi_c_language()
 {
-  return new ansi_c_languaget;
+  return util_make_unique<ansi_c_languaget>();
 }
 
 bool ansi_c_languaget::from_expr(
diff --git a/src/ansi-c/ansi_c_language.h b/src/ansi-c/ansi_c_language.h
index 45b7d6aaa3f..ef3de517449 100644
--- a/src/ansi-c/ansi_c_language.h
+++ b/src/ansi-c/ansi_c_language.h
@@ -12,7 +12,10 @@ Author: Daniel Kroening, kroening@kroening.com
 
 /*! \defgroup gr_ansi_c ANSI-C front-end */
 
+#include <memory>
+
 #include <util/language.h>
+#include <util/make_unique.h>
 
 #include "ansi_c_parse_tree.h"
 
@@ -64,8 +67,8 @@ class ansi_c_languaget:public languaget
     exprt &expr,
     const namespacet &ns) override;
 
-  languaget *new_language() override
-  { return new ansi_c_languaget; }
+  std::unique_ptr<languaget> new_language() override
+  { return util_make_unique<ansi_c_languaget>(); }
 
   std::string id() const override { return "C"; }
   std::string description() const override { return "ANSI-C 99"; }
@@ -78,6 +81,6 @@ class ansi_c_languaget:public languaget
   std::string parse_path;
 };
 
-languaget *new_ansi_c_language();
+std::unique_ptr<languaget> new_ansi_c_language();
 
 #endif // CPROVER_ANSI_C_ANSI_C_LANGUAGE_H
diff --git a/src/cbmc/bmc.cpp b/src/cbmc/bmc.cpp
index ae7741f423c..956e0e22cb9 100644
--- a/src/cbmc/bmc.cpp
+++ b/src/cbmc/bmc.cpp
@@ -314,11 +314,11 @@ safety_checkert::resultt bmct::run(
   std::unique_ptr<memory_model_baset> memory_model;
 
   if(mm.empty() || mm=="sc")
-    memory_model=std::unique_ptr<memory_model_baset>(new memory_model_sct(ns));
+    memory_model=util_make_unique<memory_model_sct>(ns);
   else if(mm=="tso")
-    memory_model=std::unique_ptr<memory_model_baset>(new memory_model_tsot(ns));
+    memory_model=util_make_unique<memory_model_tsot>(ns);
   else if(mm=="pso")
-    memory_model=std::unique_ptr<memory_model_baset>(new memory_model_psot(ns));
+    memory_model=util_make_unique<memory_model_psot>(ns);
   else
   {
     error() << "Invalid memory model " << mm
diff --git a/src/cbmc/cbmc_main.cpp b/src/cbmc/cbmc_main.cpp
index e5e679a8d0e..4b014d17351 100644
--- a/src/cbmc/cbmc_main.cpp
+++ b/src/cbmc/cbmc_main.cpp
@@ -34,7 +34,9 @@ extern unsigned long long irep_cmp_ne_cnt;
 #ifdef _MSC_VER
 int wmain(int argc, const wchar_t **argv_wide)
 {
-  const char **argv=narrow_argv(argc, argv_wide);
+  auto vec=narrow_argv(argc, argv_wide);
+  auto narrow=to_c_str_array(std::begin(vec), std::end(vec));
+  auto argv=narrow.data();
 #else
 int main(int argc, const char **argv)
 {
diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
index 772b62d9b74..c6482826d0b 100644
--- a/src/cbmc/cbmc_parse_options.cpp
+++ b/src/cbmc/cbmc_parse_options.cpp
@@ -601,9 +601,9 @@ int cbmc_parse_optionst::get_goto_program(
         return 6;
       }
 
-      languaget *language=get_language_from_filename(filename);
+      std::unique_ptr<languaget> language=get_language_from_filename(filename);
 
-      if(language==NULL)
+      if(!language)
       {
         error() << "failed to figure out type of file `"
                 <<  filename << "'" << eom;
@@ -750,17 +750,15 @@ void cbmc_parse_optionst::preprocessing()
       return;
     }
 
-    languaget *ptr=get_language_from_filename(filename);
+    std::unique_ptr<languaget> language=get_language_from_filename(filename);
 
-    if(ptr==NULL)
+    if(!language)
     {
       error() << "failed to figure out type of file" << eom;
       return;
     }
 
-    ptr->set_message_handler(get_message_handler());
-
-    std::unique_ptr<languaget> language(ptr);
+    language->set_message_handler(get_message_handler());
 
     if(language->preprocess(infile, filename, std::cout))
       error() << "PREPROCESSING ERROR" << eom;
diff --git a/src/cbmc/cbmc_solvers.cpp b/src/cbmc/cbmc_solvers.cpp
index 1825a1cd3ab..2fbf73b7c71 100644
--- a/src/cbmc/cbmc_solvers.cpp
+++ b/src/cbmc/cbmc_solvers.cpp
@@ -9,11 +9,12 @@ Author: Daniel Kroening, kroening@kroening.com
 /// \file
 /// Solvers for VCs Generated by Symbolic Execution of ANSI-C
 
-#include <memory>
-#include <iostream>
 #include <fstream>
+#include <iostream>
+#include <memory>
 
 #include <util/unicode.h>
+#include <util/make_unique.h>
 
 #include <solvers/sat/satcheck.h>
 #include <solvers/refinement/bv_refinement.h>
@@ -86,65 +87,65 @@ smt2_dect::solvert cbmc_solverst::get_smt2_solver_type() const
   return s;
 }
 
-/// Get the default decision procedure
-cbmc_solverst::solvert* cbmc_solverst::get_default()
+std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_default()
 {
-  solvert *solver=new solvert;
+  auto solver=util_make_unique<solvert>();
 
   if(options.get_bool_option("beautify") ||
      !options.get_bool_option("sat-preprocessor")) // no simplifier
   {
     // simplifier won't work with beautification
-    solver->set_prop(new satcheck_no_simplifiert());
+    solver->set_prop(util_make_unique<satcheck_no_simplifiert>());
   }
   else // with simplifier
   {
-    solver->set_prop(new satcheckt());
+    solver->set_prop(util_make_unique<satcheckt>());
   }
 
   solver->prop().set_message_handler(get_message_handler());
 
-  bv_cbmct *bv_cbmc=new bv_cbmct(ns, solver->prop());
+  auto bv_cbmc=util_make_unique<bv_cbmct>(ns, solver->prop());
 
   if(options.get_option("arrays-uf")=="never")
     bv_cbmc->unbounded_array=bv_cbmct::unbounded_arrayt::U_NONE;
   else if(options.get_option("arrays-uf")=="always")
     bv_cbmc->unbounded_array=bv_cbmct::unbounded_arrayt::U_ALL;
 
-  solver->set_prop_conv(bv_cbmc);
+  solver->set_prop_conv(std::move(bv_cbmc));
 
   return solver;
 }
 
-cbmc_solverst::solvert* cbmc_solverst::get_dimacs()
+std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_dimacs()
 {
   no_beautification();
   no_incremental_check();
 
-  dimacs_cnft *prop=new dimacs_cnft();
+  auto prop=util_make_unique<dimacs_cnft>();
   prop->set_message_handler(get_message_handler());
 
   std::string filename=options.get_option("outfile");
 
-  return new solvert(new cbmc_dimacst(ns, *prop, filename), prop);
+  auto cbmc_dimacs=util_make_unique<cbmc_dimacst>(ns, *prop, filename);
+  return util_make_unique<solvert>(std::move(cbmc_dimacs), std::move(prop));
 }
 
-cbmc_solverst::solvert* cbmc_solverst::get_bv_refinement()
+std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_bv_refinement()
 {
-  propt *prop;
-
-  // We offer the option to disable the SAT preprocessor
-  if(options.get_bool_option("sat-preprocessor"))
+  std::unique_ptr<propt> prop=[this]() -> std::unique_ptr<propt>
   {
-    no_beautification();
-    prop=new satcheckt();
-  }
-  else
-    prop=new satcheck_no_simplifiert();
+    // We offer the option to disable the SAT preprocessor
+    if(options.get_bool_option("sat-preprocessor"))
+    {
+      no_beautification();
+      return util_make_unique<satcheckt>();
+    }
+    return util_make_unique<satcheck_no_simplifiert>();
+  }();
 
   prop->set_message_handler(get_message_handler());
 
-  bv_refinementt *bv_refinement=new bv_refinementt(ns, *prop);
+  auto bv_refinement=util_make_unique<bv_refinementt>(ns, *prop);
   bv_refinement->set_ui(ui);
 
   // we allow setting some parameters
@@ -157,19 +158,18 @@ cbmc_solverst::solvert* cbmc_solverst::get_bv_refinement()
   bv_refinement->do_arithmetic_refinement =
     options.get_bool_option("refine-arithmetic");
 
-  return new solvert(bv_refinement, prop);
+  return util_make_unique<solvert>(std::move(bv_refinement), std::move(prop));
 }
 
 /// the string refinement adds to the bit vector refinement specifications for
 /// functions from the Java string library
 /// \return a solver for cbmc
-cbmc_solverst::solvert* cbmc_solverst::get_string_refinement()
+std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_string_refinement()
 {
-  propt *prop;
-  prop=new satcheck_no_simplifiert();
+  auto prop=util_make_unique<satcheck_no_simplifiert>();
   prop->set_message_handler(get_message_handler());
 
-  string_refinementt *string_refinement=new string_refinementt(
+  auto string_refinement=util_make_unique<string_refinementt>(
     ns, *prop, MAX_NB_REFINEMENT);
   string_refinement->set_ui(ui);
 
@@ -191,10 +191,12 @@ cbmc_solverst::solvert* cbmc_solverst::get_string_refinement()
   string_refinement->do_arithmetic_refinement=
     options.get_bool_option("refine-arithmetic");
 
-  return new solvert(string_refinement, prop);
+  return util_make_unique<solvert>(
+    std::move(string_refinement), std::move(prop));
 }
 
-cbmc_solverst::solvert* cbmc_solverst::get_smt1(smt1_dect::solvert solver)
+std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_smt1(
+  smt1_dect::solvert solver)
 {
   no_beautification();
   no_incremental_check();
@@ -209,20 +211,20 @@ cbmc_solverst::solvert* cbmc_solverst::get_smt1(smt1_dect::solvert solver)
       throw 0;
     }
 
-    smt1_dect *smt1_dec=
-      new smt1_dect(
+    auto smt1_dec=
+      util_make_unique<smt1_dect>(
         ns,
         "cbmc",
         "Generated by CBMC " CBMC_VERSION,
         "QF_AUFBV",
         solver);
 
-    return new solvert(smt1_dec);
+    return util_make_unique<solvert>(std::move(smt1_dec));
   }
   else if(filename=="-")
   {
-    smt1_convt *smt1_conv=
-      new smt1_convt(
+    auto smt1_conv=
+      util_make_unique<smt1_convt>(
         ns,
         "cbmc",
         "Generated by CBMC " CBMC_VERSION,
@@ -232,14 +234,14 @@ cbmc_solverst::solvert* cbmc_solverst::get_smt1(smt1_dect::solvert solver)
 
     smt1_conv->set_message_handler(get_message_handler());
 
-    return new solvert(smt1_conv);
+    return util_make_unique<solvert>(std::move(smt1_conv));
   }
   else
   {
     #ifdef _MSC_VER
-    std::ofstream *out=new std::ofstream(widen(filename));
+    auto out=util_make_unique<std::ofstream>(widen(filename));
     #else
-    std::ofstream *out=new std::ofstream(filename);
+    auto out=util_make_unique<std::ofstream>(filename);
     #endif
 
     if(!out)
@@ -248,8 +250,8 @@ cbmc_solverst::solvert* cbmc_solverst::get_smt1(smt1_dect::solvert solver)
       throw 0;
     }
 
-    smt1_convt *smt1_conv=
-      new smt1_convt(
+    auto smt1_conv=
+      util_make_unique<smt1_convt>(
         ns,
         "cbmc",
         "Generated by CBMC " CBMC_VERSION,
@@ -259,11 +261,12 @@ cbmc_solverst::solvert* cbmc_solverst::get_smt1(smt1_dect::solvert solver)
 
     smt1_conv->set_message_handler(get_message_handler());
 
-    return new solvert(smt1_conv, out);
+    return util_make_unique<solvert>(std::move(smt1_conv), std::move(out));
   }
 }
 
-cbmc_solverst::solvert* cbmc_solverst::get_smt2(smt2_dect::solvert solver)
+std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_smt2(
+  smt2_dect::solvert solver)
 {
   no_beautification();
 
@@ -277,8 +280,8 @@ cbmc_solverst::solvert* cbmc_solverst::get_smt2(smt2_dect::solvert solver)
       throw 0;
     }
 
-    smt2_dect *smt2_dec=
-      new smt2_dect(
+    auto smt2_dec=
+      util_make_unique<smt2_dect>(
         ns,
         "cbmc",
         "Generated by CBMC " CBMC_VERSION,
@@ -288,12 +291,12 @@ cbmc_solverst::solvert* cbmc_solverst::get_smt2(smt2_dect::solvert solver)
     if(options.get_bool_option("fpa"))
       smt2_dec->use_FPA_theory=true;
 
-    return new solvert(smt2_dec);
+    return util_make_unique<solvert>(std::move(smt2_dec));
   }
   else if(filename=="-")
   {
-    smt2_convt *smt2_conv=
-      new smt2_convt(
+    auto smt2_conv=
+      util_make_unique<smt2_convt>(
         ns,
         "cbmc",
         "Generated by CBMC " CBMC_VERSION,
@@ -306,14 +309,14 @@ cbmc_solverst::solvert* cbmc_solverst::get_smt2(smt2_dect::solvert solver)
 
     smt2_conv->set_message_handler(get_message_handler());
 
-    return new solvert(smt2_conv);
+    return util_make_unique<solvert>(std::move(smt2_conv));
   }
   else
   {
     #ifdef _MSC_VER
-    std::ofstream *out=new std::ofstream(widen(filename));
+    auto out=util_make_unique<std::ofstream>(widen(filename));
     #else
-    std::ofstream *out=new std::ofstream(filename);
+    auto out=util_make_unique<std::ofstream>(filename);
     #endif
 
     if(!*out)
@@ -322,8 +325,8 @@ cbmc_solverst::solvert* cbmc_solverst::get_smt2(smt2_dect::solvert solver)
       throw 0;
     }
 
-    smt2_convt *smt2_conv=
-      new smt2_convt(
+    auto smt2_conv=
+      util_make_unique<smt2_convt>(
         ns,
         "cbmc",
         "Generated by CBMC " CBMC_VERSION,
@@ -336,7 +339,7 @@ cbmc_solverst::solvert* cbmc_solverst::get_smt2(smt2_dect::solvert solver)
 
     smt2_conv->set_message_handler(get_message_handler());
 
-    return new solvert(smt2_conv, out);
+    return util_make_unique<solvert>(std::move(smt2_conv), std::move(out));
   }
 }
 
diff --git a/src/cbmc/cbmc_solvers.h b/src/cbmc/cbmc_solvers.h
index f17f9b663bf..8dfb038bee8 100644
--- a/src/cbmc/cbmc_solvers.h
+++ b/src/cbmc/cbmc_solvers.h
@@ -53,19 +53,19 @@ class cbmc_solverst:public messaget
     {
     }
 
-    explicit solvert(prop_convt *p):prop_conv_ptr(p)
+    explicit solvert(std::unique_ptr<prop_convt> p):prop_conv_ptr(std::move(p))
     {
     }
 
-    solvert(prop_convt *p1, propt *p2):
-      prop_ptr(p2),
-      prop_conv_ptr(p1)
+    solvert(std::unique_ptr<prop_convt> p1, std::unique_ptr<propt> p2):
+      prop_ptr(std::move(p2)),
+      prop_conv_ptr(std::move(p1))
     {
     }
 
-    solvert(prop_convt *p1, std::ofstream *p2):
-      ofstream_ptr(p2),
-      prop_conv_ptr(p1)
+    solvert(std::unique_ptr<prop_convt> p1, std::unique_ptr<std::ofstream> p2):
+      ofstream_ptr(std::move(p2)),
+      prop_conv_ptr(std::move(p1))
     {
     }
 
@@ -81,19 +81,19 @@ class cbmc_solverst:public messaget
       return *prop_ptr;
     }
 
-    void set_prop_conv(prop_convt *p)
+    void set_prop_conv(std::unique_ptr<prop_convt> p)
     {
-      prop_conv_ptr=std::unique_ptr<prop_convt>(p);
+      prop_conv_ptr=std::move(p);
     }
 
-    void set_prop(propt *p)
+    void set_prop(std::unique_ptr<propt> p)
     {
-      prop_ptr=std::unique_ptr<propt>(p);
+      prop_ptr=std::move(p);
     }
 
-    void set_ofstream(std::ofstream *p)
+    void set_ofstream(std::unique_ptr<std::ofstream> p)
     {
-      ofstream_ptr=std::unique_ptr<std::ofstream>(p);
+      ofstream_ptr=std::move(p);
     }
 
     // the objects are deleted in the opposite order they appear below
@@ -105,22 +105,17 @@ class cbmc_solverst:public messaget
   // returns a solvert object
   virtual std::unique_ptr<solvert> get_solver()
   {
-    solvert *solver;
-
     if(options.get_bool_option("dimacs"))
-      solver=get_dimacs();
-    else if(options.get_bool_option("refine"))
-      solver=get_bv_refinement();
-    else if(options.get_bool_option("refine-strings"))
-      solver=get_string_refinement();
-    else if(options.get_bool_option("smt1"))
-      solver=get_smt1(get_smt1_solver_type());
-    else if(options.get_bool_option("smt2"))
-      solver=get_smt2(get_smt2_solver_type());
-    else
-      solver=get_default();
-
-    return std::unique_ptr<solvert>(solver);
+      return get_dimacs();
+    if(options.get_bool_option("refine"))
+      return get_bv_refinement();
+    if(options.get_bool_option("refine-strings"))
+      return get_string_refinement();
+    if(options.get_bool_option("smt1"))
+      return get_smt1(get_smt1_solver_type());
+    if(options.get_bool_option("smt2"))
+      return get_smt2(get_smt2_solver_type());
+    return get_default();
   }
 
   virtual ~cbmc_solverst()
@@ -137,12 +132,12 @@ class cbmc_solverst:public messaget
   // use gui format
   language_uit::uit ui;
 
-  solvert *get_default();
-  solvert *get_dimacs();
-  solvert *get_bv_refinement();
-  solvert *get_string_refinement();
-  solvert *get_smt1(smt1_dect::solvert solver);
-  solvert *get_smt2(smt2_dect::solvert solver);
+  std::unique_ptr<solvert> get_default();
+  std::unique_ptr<solvert> get_dimacs();
+  std::unique_ptr<solvert> get_string_refinement();
+  std::unique_ptr<solvert> get_bv_refinement();
+  std::unique_ptr<solvert> get_smt1(smt1_dect::solvert solver);
+  std::unique_ptr<solvert> get_smt2(smt2_dect::solvert solver);
 
   smt1_dect::solvert get_smt1_solver_type() const;
   smt2_dect::solvert get_smt2_solver_type() const;
diff --git a/src/clobber/clobber_main.cpp b/src/clobber/clobber_main.cpp
index 16e2a286900..12e60d0e668 100644
--- a/src/clobber/clobber_main.cpp
+++ b/src/clobber/clobber_main.cpp
@@ -16,14 +16,13 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifdef _MSC_VER
 int wmain(int argc, const wchar_t **argv_wide)
 {
-  const char **argv=narrow_argv(argc, argv_wide);
-  clobber_parse_optionst parse_options(argc, argv);
-  return parse_options.main();
-}
+  auto vec=narrow_argv(argc, argv_wide);
+  auto narrow=to_c_str_array(std::begin(vec), std::end(vec));
+  auto argv=narrow.data();
 #else
 int main(int argc, const char **argv)
 {
+#endif
   clobber_parse_optionst parse_options(argc, argv);
   return parse_options.main();
 }
-#endif
diff --git a/src/clobber/clobber_parse_options.cpp b/src/clobber/clobber_parse_options.cpp
index 42aadee4326..61e54971c7e 100644
--- a/src/clobber/clobber_parse_options.cpp
+++ b/src/clobber/clobber_parse_options.cpp
@@ -247,9 +247,9 @@ bool clobber_parse_optionst::get_goto_program(
         return true;
       }
 
-      languaget *language=get_language_from_filename(filename);
+      std::unique_ptr<languaget> language=get_language_from_filename(filename);
 
-      if(language==NULL)
+      if(!language)
       {
         error() << "failed to figure out type of file `" <<  filename << "'"
                 << eom;
diff --git a/src/cpp/cpp_language.cpp b/src/cpp/cpp_language.cpp
index 3843038950a..bcfee26ec41 100644
--- a/src/cpp/cpp_language.cpp
+++ b/src/cpp/cpp_language.cpp
@@ -204,9 +204,9 @@ void cpp_languaget::show_parse(
     out << "UNKNOWN: " << item.pretty() << '\n';
 }
 
-languaget *new_cpp_language()
+std::unique_ptr<languaget> new_cpp_language()
 {
-  return new cpp_languaget;
+  return util_make_unique<cpp_languaget>();
 }
 
 bool cpp_languaget::from_expr(
diff --git a/src/cpp/cpp_language.h b/src/cpp/cpp_language.h
index 982e2e180c1..e6999773f62 100644
--- a/src/cpp/cpp_language.h
+++ b/src/cpp/cpp_language.h
@@ -14,7 +14,10 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 
 /*! \defgroup gr_cpp C++ front-end */
 
+#include <memory>
+
 #include <util/language.h>
+#include <util/make_unique.h> // unique_ptr
 
 #include "cpp_parse_tree.h"
 
@@ -76,8 +79,8 @@ class cpp_languaget:public languaget
     exprt &expr,
     const namespacet &ns) override;
 
-  languaget *new_language() override
-  { return new cpp_languaget; }
+  std::unique_ptr<languaget> new_language() override
+  { return util_make_unique<cpp_languaget>(); }
 
   std::string id() const override { return "cpp"; }
   std::string description() const override { return "C++"; }
@@ -97,6 +100,6 @@ class cpp_languaget:public languaget
   }
 };
 
-languaget *new_cpp_language();
+std::unique_ptr<languaget> new_cpp_language();
 
 #endif // CPROVER_CPP_CPP_LANGUAGE_H
diff --git a/src/goto-analyzer/goto_analyzer_main.cpp b/src/goto-analyzer/goto_analyzer_main.cpp
index 64e14c74936..eb44037d372 100644
--- a/src/goto-analyzer/goto_analyzer_main.cpp
+++ b/src/goto-analyzer/goto_analyzer_main.cpp
@@ -16,7 +16,9 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifdef _MSC_VER
 int wmain(int argc, const wchar_t **argv_wide)
 {
-  const char **argv=narrow_argv(argc, argv_wide);
+  auto vec=narrow_argv(argc, argv_wide);
+  auto narrow=to_c_str_array(std::begin(vec), std::end(vec));
+  auto argv=narrow.data();
 #else
 int main(int argc, const char **argv)
 {
diff --git a/src/goto-cc/compile.cpp b/src/goto-cc/compile.cpp
index aa3256da590..084a07b2a42 100644
--- a/src/goto-cc/compile.cpp
+++ b/src/goto-cc/compile.cpp
@@ -457,7 +457,7 @@ bool compilet::parse(const std::string &file_name)
     return true;
   }
 
-  languaget *languagep;
+  std::unique_ptr<languaget> languagep;
 
   // Using '-x', the type of a file can be overridden;
   // otherwise, it's guessed from the extension.
@@ -472,14 +472,13 @@ bool compilet::parse(const std::string &file_name)
   else
     languagep=get_language_from_filename(file_name);
 
-  if(languagep==NULL)
+  if(!languagep)
   {
     error() << "failed to figure out type of file `" << file_name << "'" << eom;
     return true;
   }
 
-  languaget &language=*languagep;
-  language.set_message_handler(get_message_handler());
+  languagep->set_message_handler(get_message_handler());
 
   language_filet language_file;
 
@@ -489,7 +488,7 @@ bool compilet::parse(const std::string &file_name)
 
   language_filet &lf=res.first->second;
   lf.filename=file_name;
-  lf.language=languagep;
+  lf.language=std::move(languagep);
 
   if(mode==PREPROCESS_ONLY)
   {
@@ -511,13 +510,13 @@ bool compilet::parse(const std::string &file_name)
       }
     }
 
-    language.preprocess(infile, file_name, *os);
+    lf.language->preprocess(infile, file_name, *os);
   }
   else
   {
     statistics() << "Parsing: " << file_name << eom;
 
-    if(language.parse(infile, file_name))
+    if(lf.language->parse(infile, file_name))
     {
       if(get_ui()==ui_message_handlert::uit::PLAIN)
         error() << "PARSING ERROR" << eom;
diff --git a/src/goto-cc/goto_cc_main.cpp b/src/goto-cc/goto_cc_main.cpp
index ebe885a37a3..a0913d8d5ae 100644
--- a/src/goto-cc/goto_cc_main.cpp
+++ b/src/goto-cc/goto_cc_main.cpp
@@ -45,7 +45,9 @@ int main(int argc, const char **argv)
 #endif
 {
   #ifdef _MSC_VER
-  const char **argv=narrow_argv(argc, argv_wide);
+  auto vec=narrow_argv(argc, argv_wide);
+  auto narrow=to_c_str_array(std::begin(vec), std::end(vec));
+  auto argv=narrow.data();
   #endif
 
   if(argv==NULL || argc<1)
diff --git a/src/goto-diff/goto_diff_main.cpp b/src/goto-diff/goto_diff_main.cpp
index 604777582d0..8d32d6ec379 100644
--- a/src/goto-diff/goto_diff_main.cpp
+++ b/src/goto-diff/goto_diff_main.cpp
@@ -26,7 +26,9 @@ extern unsigned long long irep_cmp_ne_cnt;
 #ifdef _MSC_VER
 int wmain(int argc, const wchar_t **argv_wide)
 {
-  const char **argv=narrow_argv(argc, argv_wide);
+  auto vec=narrow_argv(argc, argv_wide);
+  auto narrow=to_c_str_array(std::begin(vec), std::end(vec));
+  auto argv=narrow.data();
 #else
 int main(int argc, const char **argv)
 {
diff --git a/src/goto-diff/goto_diff_parse_options.cpp b/src/goto-diff/goto_diff_parse_options.cpp
index ee2a74a0b24..451e29bd418 100644
--- a/src/goto-diff/goto_diff_parse_options.cpp
+++ b/src/goto-diff/goto_diff_parse_options.cpp
@@ -9,8 +9,8 @@ Author: Peter Schrammel
 /// \file
 /// GOTO-DIFF Command Line Option Processing
 
-#include <fstream>
 #include <cstdlib> // exit()
+#include <fstream>
 #include <iostream>
 #include <memory>
 
@@ -18,6 +18,7 @@ Author: Peter Schrammel
 #include <util/config.h>
 #include <util/language.h>
 #include <util/options.h>
+#include <util/make_unique.h>
 
 #include <goto-programs/goto_convert_functions.h>
 #include <goto-programs/remove_function_pointers.h>
@@ -317,9 +318,9 @@ int goto_diff_parse_optionst::doit()
     return 0;
   }
 
-  std::unique_ptr<goto_difft> goto_diff;
-  goto_diff = std::unique_ptr<goto_difft>(
-    new syntactic_difft(goto_model1, goto_model2, get_message_handler()));
+  std::unique_ptr<goto_difft> goto_diff=
+    util_make_unique<syntactic_difft>(
+      goto_model1, goto_model2, get_message_handler());
   goto_diff->set_ui(get_ui());
 
   (*goto_diff)();
diff --git a/src/goto-instrument/accelerate/enumerating_loop_acceleration.h b/src/goto-instrument/accelerate/enumerating_loop_acceleration.h
index f84d3fbd23b..a9d03b7ad69 100644
--- a/src/goto-instrument/accelerate/enumerating_loop_acceleration.h
+++ b/src/goto-instrument/accelerate/enumerating_loop_acceleration.h
@@ -12,6 +12,10 @@ Author: Matt Lewis
 #ifndef CPROVER_GOTO_INSTRUMENT_ACCELERATE_ENUMERATING_LOOP_ACCELERATION_H
 #define CPROVER_GOTO_INSTRUMENT_ACCELERATE_ENUMERATING_LOOP_ACCELERATION_H
 
+#include <memory>
+
+#include <util/make_unique.h>
+
 #include <goto-programs/goto_program.h>
 
 #include <analyses/natural_loops.h>
@@ -39,17 +43,10 @@ class enumerating_loop_accelerationt:public loop_accelerationt
     loop(_loop),
     loop_header(_loop_header),
     polynomial_accelerator(symbol_table, goto_functions),
-    path_limit(_path_limit)
-  {
-    // path_enumerator = new all_paths_enumeratort(goto_program, loop,
-    // loop_header);
-    path_enumerator = new sat_path_enumeratort(symbol_table, goto_functions,
-        goto_program, loop, loop_header);
-  }
-
-  ~enumerating_loop_accelerationt()
+    path_limit(_path_limit),
+    path_enumerator(util_make_unique<sat_path_enumeratort>(
+      symbol_table, goto_functions, goto_program, loop, loop_header))
   {
-    delete path_enumerator;
   }
 
   virtual bool accelerate(path_acceleratort &accelerator);
@@ -63,7 +60,7 @@ class enumerating_loop_accelerationt:public loop_accelerationt
   polynomial_acceleratort polynomial_accelerator;
   int path_limit;
 
-  path_enumeratort *path_enumerator;
+  std::unique_ptr<path_enumeratort> path_enumerator;
 };
 
 #endif // CPROVER_GOTO_INSTRUMENT_ACCELERATE_ENUMERATING_LOOP_ACCELERATION_H
diff --git a/src/goto-instrument/accelerate/scratch_program.h b/src/goto-instrument/accelerate/scratch_program.h
index da860f39e1a..a132f597c3a 100644
--- a/src/goto-instrument/accelerate/scratch_program.h
+++ b/src/goto-instrument/accelerate/scratch_program.h
@@ -12,8 +12,10 @@ Author: Matt Lewis
 #ifndef CPROVER_GOTO_INSTRUMENT_ACCELERATE_SCRATCH_PROGRAM_H
 #define CPROVER_GOTO_INSTRUMENT_ACCELERATE_SCRATCH_PROGRAM_H
 
+#include <memory>
 #include <string>
 
+#include <util/make_unique.h>
 #include <util/symbol_table.h>
 
 #include <goto-programs/goto_program.h>
@@ -38,18 +40,13 @@ class scratch_programt:public goto_programt
     ns(symbol_table),
     equation(ns),
     symex(ns, symbol_table, equation),
-    satcheck(new satcheckt),
+    satcheck(util_make_unique<satcheckt>()),
     satchecker(ns, *satcheck),
     z3(ns, "accelerate", "", "", smt2_dect::solvert::Z3),
     checker(&z3) // checker(&satchecker)
   {
   }
 
-  ~scratch_programt()
-  {
-    delete satcheck;
-  }
-
   void append(goto_programt::instructionst &instructions);
   void append(goto_programt &program);
   void append_path(patht &path);
@@ -79,7 +76,7 @@ class scratch_programt:public goto_programt
   symex_target_equationt equation;
   goto_symext symex;
 
-  propt *satcheck;
+  std::unique_ptr<propt> satcheck;
   bv_pointerst satchecker;
   smt2_dect z3;
   prop_convt *checker;
diff --git a/src/goto-instrument/dump_c_class.h b/src/goto-instrument/dump_c_class.h
index 4f47cd4cad4..1da4a87d7ae 100644
--- a/src/goto-instrument/dump_c_class.h
+++ b/src/goto-instrument/dump_c_class.h
@@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <set>
 #include <string>
+#include <memory> // unique_ptr
 
 #include <util/language.h>
 
@@ -37,10 +38,7 @@ class dump_ct
       system_symbols=system_library_symbolst();
   }
 
-  virtual ~dump_ct()
-  {
-    delete language;
-  }
+  virtual ~dump_ct()=default;
 
   void operator()(std::ostream &out);
 
@@ -48,7 +46,7 @@ class dump_ct
   const goto_functionst &goto_functions;
   symbol_tablet copied_symbol_table;
   const namespacet ns;
-  languaget *language;
+  std::unique_ptr<languaget> language;
 
   typedef std::unordered_set<irep_idt, irep_id_hash> convertedt;
   convertedt converted_compound, converted_global, converted_enum;
diff --git a/src/goto-instrument/goto_instrument_main.cpp b/src/goto-instrument/goto_instrument_main.cpp
index fb394efbb3d..fb47a8e6ffe 100644
--- a/src/goto-instrument/goto_instrument_main.cpp
+++ b/src/goto-instrument/goto_instrument_main.cpp
@@ -16,7 +16,9 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifdef _MSC_VER
 int wmain(int argc, const wchar_t **argv_wide)
 {
-  const char **argv=narrow_argv(argc, argv_wide);
+  auto vec=narrow_argv(argc, argv_wide);
+  auto narrow=to_c_str_array(std::begin(vec), std::end(vec));
+  auto argv=narrow.data();
 #else
 int main(int argc, const char **argv)
 {
diff --git a/src/goto-instrument/wmm/instrumenter_strategies.cpp b/src/goto-instrument/wmm/instrumenter_strategies.cpp
index 258eec8df0b..35034b319f7 100644
--- a/src/goto-instrument/wmm/instrumenter_strategies.cpp
+++ b/src/goto-instrument/wmm/instrumenter_strategies.cpp
@@ -274,9 +274,9 @@ void inline instrumentert::instrument_minimum_interference_inserter(
   const std::size_t mat_size=set_of_cycles.size()*edges.size();
   message.debug() << "size of the system: " << mat_size
     << messaget::eom;
-  int *imat=new int[mat_size+1];
-  int *jmat=new int[mat_size+1];
-  double *vmat=new double[mat_size+1];
+  std::vector<int> imat(mat_size+1);
+  std::vector<int> jmat(mat_size+1);
+  std::vector<double> vmat(mat_size+1);
 
   /* fills the constraints coeff */
   /* tables read from 1 in glpk -- first row/column ignored */
@@ -345,9 +345,6 @@ void inline instrumentert::instrument_minimum_interference_inserter(
   }
 
   glp_delete_prob(lp);
-  delete[] imat;
-  delete[] jmat;
-  delete[] vmat;
 #else
   throw "sorry, minimum interference option requires glpk; "
         "please recompile goto-instrument with glpk";
diff --git a/src/goto-programs/show_symbol_table.cpp b/src/goto-programs/show_symbol_table.cpp
index 60460147e52..5ec84dd6a99 100644
--- a/src/goto-programs/show_symbol_table.cpp
+++ b/src/goto-programs/show_symbol_table.cpp
@@ -40,25 +40,27 @@ void show_symbol_table_plain(
   {
     const symbolt &symbol=ns.lookup(id);
 
-    languaget *ptr;
+    std::unique_ptr<languaget> ptr;
 
     if(symbol.mode=="")
+    {
       ptr=get_default_language();
+    }
     else
     {
       ptr=get_language_from_mode(symbol.mode);
-      if(ptr==NULL)
-        throw "symbol "+id2string(symbol.name)+" has unknown mode";
     }
 
-    std::unique_ptr<languaget> p(ptr);
+    if(!ptr)
+      throw "symbol "+id2string(symbol.name)+" has unknown mode";
+
     std::string type_str, value_str;
 
     if(symbol.type.is_not_nil())
-      p->from_type(symbol.type, type_str, ns);
+      ptr->from_type(symbol.type, type_str, ns);
 
     if(symbol.value.is_not_nil())
-      p->from_expr(symbol.value, value_str, ns);
+      ptr->from_expr(symbol.value, value_str, ns);
 
     out << "Symbol......: " << symbol.name << '\n' << std::flush;
     out << "Pretty name.: " << symbol.pretty_name << '\n';
diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp
index d88e9c68bac..73ab0713933 100644
--- a/src/goto-symex/goto_symex_state.cpp
+++ b/src/goto-symex/goto_symex_state.cpp
@@ -24,13 +24,14 @@ goto_symex_statet::goto_symex_statet():
   depth(0),
   symex_target(NULL),
   atomic_section_id(0),
-  record_events(true),
-  dirty(0)
+  record_events(true)
 {
   threads.resize(1);
   new_frame();
 }
 
+goto_symex_statet::~goto_symex_statet()=default;
+
 void goto_symex_statet::initialize(const goto_functionst &goto_functions)
 {
   goto_functionst::function_mapt::const_iterator it=
diff --git a/src/goto-symex/goto_symex_state.h b/src/goto-symex/goto_symex_state.h
index d62d4a66af9..3c2deecf994 100644
--- a/src/goto-symex/goto_symex_state.h
+++ b/src/goto-symex/goto_symex_state.h
@@ -13,11 +13,13 @@ Author: Daniel Kroening, kroening@kroening.com
 #define CPROVER_GOTO_SYMEX_GOTO_SYMEX_STATE_H
 
 #include <cassert>
+#include <memory>
 #include <unordered_set>
 
 #include <util/guard.h>
 #include <util/std_expr.h>
 #include <util/ssa_expr.h>
+#include <util/make_unique.h>
 
 #include <pointer-analysis/value_set.h>
 #include <goto-programs/goto_functions.h>
@@ -27,10 +29,11 @@ Author: Daniel Kroening, kroening@kroening.com
 class dirtyt;
 
 // central data structure: state
-class goto_symex_statet
+class goto_symex_statet final
 {
 public:
   goto_symex_statet();
+  ~goto_symex_statet();
 
   // distance from entry
   unsigned depth;
@@ -341,7 +344,7 @@ class goto_symex_statet
 
   void switch_to_thread(unsigned t);
   bool record_events;
-  const dirtyt * dirty;
+  std::unique_ptr<const dirtyt> dirty;
 };
 
 #endif // CPROVER_GOTO_SYMEX_GOTO_SYMEX_STATE_H
diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp
index 501fdabea70..075369dd23f 100644
--- a/src/goto-symex/symex_main.cpp
+++ b/src/goto-symex/symex_main.cpp
@@ -10,11 +10,13 @@ Author: Daniel Kroening, kroening@kroening.com
 /// Symbolic Execution
 
 #include <cassert>
+#include <memory>
 
 #include <util/std_expr.h>
 #include <util/rename.h>
 #include <util/symbol_table.h>
 #include <util/replace_symbol.h>
+#include <util/make_unique.h>
 
 #include <analyses/dirty.h>
 
@@ -112,7 +114,7 @@ void goto_symext::operator()(
   state.top().end_of_function=--goto_program.instructions.end();
   state.top().calling_location.pc=state.top().end_of_function;
   state.symex_target=&target;
-  state.dirty=new dirtyt(goto_functions);
+  state.dirty=util_make_unique<dirtyt>(goto_functions);
 
   assert(state.top().end_of_function->is_end_function());
 
@@ -130,8 +132,7 @@ void goto_symext::operator()(
     }
   }
 
-  delete state.dirty;
-  state.dirty=0;
+  state.dirty=nullptr;
 }
 
 /// symex starting from given program
diff --git a/src/java_bytecode/jar_file.cpp b/src/java_bytecode/jar_file.cpp
index f70ef35492c..1631e368629 100644
--- a/src/java_bytecode/jar_file.cpp
+++ b/src/java_bytecode/jar_file.cpp
@@ -35,11 +35,12 @@ void jar_filet::open(
     for(std::size_t i=0; i<number_of_files; i++)
     {
       mz_uint filename_length=mz_zip_reader_get_filename(&zip, i, nullptr, 0);
-      char *filename_char=new char[filename_length+1];
+      std::vector<char> filename_char(filename_length+1);
       mz_uint filename_len=
-        mz_zip_reader_get_filename(&zip, i, filename_char, filename_length);
+        mz_zip_reader_get_filename(
+          &zip, i, filename_char.data(), filename_length);
       assert(filename_length==filename_len);
-      std::string file_name(filename_char);
+      std::string file_name(filename_char.data());
 
       // non-class files are loaded in any case
       bool add_file=!has_suffix(file_name, ".class");
@@ -52,7 +53,6 @@ void jar_filet::open(
                    << " from " << filename << eom;
         filtered_jar[file_name]=i;
       }
-      delete[] filename_char;
     }
   }
 }
diff --git a/src/java_bytecode/java_bytecode_language.cpp b/src/java_bytecode/java_bytecode_language.cpp
index 1d37e8382df..e3dbec1fef8 100644
--- a/src/java_bytecode/java_bytecode_language.cpp
+++ b/src/java_bytecode/java_bytecode_language.cpp
@@ -699,9 +699,9 @@ void java_bytecode_languaget::show_parse(std::ostream &out)
   java_class_loader(main_class).output(out);
 }
 
-languaget *new_java_bytecode_language()
+std::unique_ptr<languaget> new_java_bytecode_language()
 {
-  return new java_bytecode_languaget;
+  return util_make_unique<java_bytecode_languaget>();
 }
 
 bool java_bytecode_languaget::from_expr(
diff --git a/src/java_bytecode/java_bytecode_language.h b/src/java_bytecode/java_bytecode_language.h
index c107ffd0267..6e1ff4cd5c8 100644
--- a/src/java_bytecode/java_bytecode_language.h
+++ b/src/java_bytecode/java_bytecode_language.h
@@ -10,8 +10,11 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_LANGUAGE_H
 #define CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_LANGUAGE_H
 
+#include <memory>
+
 #include <util/language.h>
 #include <util/cmdline.h>
+#include <util/make_unique.h>
 
 #include "java_class_loader.h"
 #include "java_string_library_preprocess.h"
@@ -79,8 +82,8 @@ class java_bytecode_languaget:public languaget
     exprt &expr,
     const namespacet &ns) override;
 
-  languaget *new_language() override
-  { return new java_bytecode_languaget; }
+  std::unique_ptr<languaget> new_language() override
+  { return util_make_unique<java_bytecode_languaget>(); }
 
   std::string id() const override { return "java"; }
   std::string description() const override { return "Java Bytecode"; }
@@ -107,6 +110,6 @@ class java_bytecode_languaget:public languaget
   std::string java_cp_include_files;
 };
 
-languaget *new_java_bytecode_language();
+std::unique_ptr<languaget> new_java_bytecode_language();
 
 #endif // CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_LANGUAGE_H
diff --git a/src/jsil/jsil_language.cpp b/src/jsil/jsil_language.cpp
index baa9cebee0c..0e774daabaa 100644
--- a/src/jsil/jsil_language.cpp
+++ b/src/jsil/jsil_language.cpp
@@ -101,9 +101,9 @@ void jsil_languaget::show_parse(std::ostream &out)
   parse_tree.output(out);
 }
 
-languaget *new_jsil_language()
+std::unique_ptr<languaget> new_jsil_language()
 {
-  return new jsil_languaget;
+  return util_make_unique<jsil_languaget>();
 }
 
 bool jsil_languaget::from_expr(
diff --git a/src/jsil/jsil_language.h b/src/jsil/jsil_language.h
index 2f6f376525b..da889e111a1 100644
--- a/src/jsil/jsil_language.h
+++ b/src/jsil/jsil_language.h
@@ -12,7 +12,10 @@ Author: Michael Tautschnig, tautschn@amazon.com
 #ifndef CPROVER_JSIL_JSIL_LANGUAGE_H
 #define CPROVER_JSIL_JSIL_LANGUAGE_H
 
+#include <memory>
+
 #include <util/language.h>
+#include <util/make_unique.h>
 
 #include "jsil_parse_tree.h"
 
@@ -32,8 +35,7 @@ class jsil_languaget:public languaget
     symbol_tablet &context,
     const std::string &module);
 
-  virtual bool final(
-    symbol_tablet &context);
+  virtual bool final(symbol_tablet &context);
 
   virtual void show_parse(std::ostream &out);
 
@@ -56,8 +58,8 @@ class jsil_languaget:public languaget
     exprt &expr,
     const namespacet &ns);
 
-  virtual languaget *new_language()
-  { return new jsil_languaget; }
+  virtual std::unique_ptr<languaget> new_language()
+  { return util_make_unique<jsil_languaget>(); }
 
   virtual std::string id() const { return "jsil"; }
   virtual std::string description() const
@@ -72,6 +74,6 @@ class jsil_languaget:public languaget
   std::string parse_path;
 };
 
-languaget *new_jsil_language();
+std::unique_ptr<languaget> new_jsil_language();
 
 #endif // CPROVER_JSIL_JSIL_LANGUAGE_H
diff --git a/src/langapi/language_ui.cpp b/src/langapi/language_ui.cpp
index fe24dff1887..a25aad17e5a 100644
--- a/src/langapi/language_ui.cpp
+++ b/src/langapi/language_ui.cpp
@@ -169,25 +169,27 @@ void language_uit::show_symbol_table_plain(
   {
     const symbolt &symbol=ns.lookup(id);
 
-    languaget *ptr;
+    std::unique_ptr<languaget> ptr;
 
     if(symbol.mode=="")
+    {
       ptr=get_default_language();
+    }
     else
     {
       ptr=get_language_from_mode(symbol.mode);
-      if(ptr==NULL)
-        throw "symbol "+id2string(symbol.name)+" has unknown mode";
     }
 
-    std::unique_ptr<languaget> p(ptr);
+    if(!ptr)
+      throw "symbol "+id2string(symbol.name)+" has unknown mode";
+
     std::string type_str, value_str;
 
     if(symbol.type.is_not_nil())
-      p->from_type(symbol.type, type_str, ns);
+      ptr->from_type(symbol.type, type_str, ns);
 
     if(symbol.value.is_not_nil())
-      p->from_expr(symbol.value, value_str, ns);
+      ptr->from_expr(symbol.value, value_str, ns);
 
     if(brief)
     {
diff --git a/src/langapi/language_util.cpp b/src/langapi/language_util.cpp
index 7e0121ced47..18e2cb42851 100644
--- a/src/langapi/language_util.cpp
+++ b/src/langapi/language_util.cpp
@@ -17,7 +17,7 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 #include "language_util.h"
 #include "mode.h"
 
-static languaget* get_language(
+static std::unique_ptr<languaget> get_language(
   const namespacet &ns,
   const irep_idt &identifier)
 {
@@ -28,9 +28,9 @@ static languaget* get_language(
      symbol->mode=="")
     return get_default_language();
 
-  languaget *ptr=get_language_from_mode(symbol->mode);
+  std::unique_ptr<languaget> ptr=get_language_from_mode(symbol->mode);
 
-  if(ptr==NULL)
+  if(!ptr)
     throw "symbol `"+id2string(symbol->name)+
       "' has unknown mode '"+id2string(symbol->mode)+"'";
 
diff --git a/src/langapi/languages.cpp b/src/langapi/languages.cpp
index 618210bba9c..3c060575f6f 100644
--- a/src/langapi/languages.cpp
+++ b/src/langapi/languages.cpp
@@ -6,15 +6,6 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 
 \*******************************************************************/
 
-
 #include "languages.h"
 
-languagest::languagest(const namespacet &_ns, languaget *_language):ns(_ns)
-{
-  language=_language;
-}
-
-languagest::~languagest()
-{
-  delete language;
-}
+languagest::~languagest()=default;
diff --git a/src/langapi/languages.h b/src/langapi/languages.h
index 92cd5381ab3..67b04fcddd5 100644
--- a/src/langapi/languages.h
+++ b/src/langapi/languages.h
@@ -12,6 +12,8 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 
 #include <util/language.h>
 
+#include <memory> // unique_ptr
+
 class languagest
 {
 public:
@@ -37,12 +39,17 @@ class languagest
 
   // constructor / destructor
 
-  languagest(const namespacet &_ns, languaget *_language);
+  languagest(const namespacet &_ns, std::unique_ptr<languaget> _language):
+    ns(_ns),
+    language(std::move(_language))
+  {
+  }
+
   virtual ~languagest();
 
 protected:
   const namespacet &ns;
-  languaget *language;
+  std::unique_ptr<languaget> language;
 };
 
 #endif // CPROVER_LANGAPI_LANGUAGES_H
diff --git a/src/langapi/mode.cpp b/src/langapi/mode.cpp
index a558c9be5e9..d2de55e2191 100644
--- a/src/langapi/mode.cpp
+++ b/src/langapi/mode.cpp
@@ -38,7 +38,7 @@ void register_language(language_factoryt factory)
   languages.back().mode=l->id();
 }
 
-languaget *get_language_from_mode(const irep_idt &mode)
+std::unique_ptr<languaget> get_language_from_mode(const irep_idt &mode)
 {
   for(languagest::const_iterator it=languages.begin();
       it!=languages.end();
@@ -46,10 +46,11 @@ languaget *get_language_from_mode(const irep_idt &mode)
     if(mode==it->mode)
       return it->factory();
 
-  return NULL;
+  return nullptr;
 }
 
-languaget *get_language_from_filename(const std::string &filename)
+std::unique_ptr<languaget> get_language_from_filename(
+  const std::string &filename)
 {
   std::size_t ext_pos=filename.rfind('.');
 
@@ -80,10 +81,10 @@ languaget *get_language_from_filename(const std::string &filename)
     #endif
   }
 
-  return NULL;
+  return nullptr;
 }
 
-languaget *get_default_language()
+std::unique_ptr<languaget> get_default_language()
 {
   assert(!languages.empty());
   return languages.front().factory();
diff --git a/src/langapi/mode.h b/src/langapi/mode.h
index e8cf679d0e2..3edb7a30be8 100644
--- a/src/langapi/mode.h
+++ b/src/langapi/mode.h
@@ -12,13 +12,16 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 
 #include <util/irep.h>
 
+#include <memory> // unique_ptr
+
 class languaget;
 
-languaget *get_language_from_mode(const irep_idt &mode);
-languaget *get_language_from_filename(const std::string &filename);
-languaget *get_default_language();
+std::unique_ptr<languaget> get_language_from_mode(const irep_idt &mode);
+std::unique_ptr<languaget> get_language_from_filename(
+  const std::string &filename);
+std::unique_ptr<languaget> get_default_language();
 
-typedef languaget *(*language_factoryt)();
+typedef std::unique_ptr<languaget> (*language_factoryt)();
 void register_language(language_factoryt factory);
 
 #endif // CPROVER_LANGAPI_MODE_H
diff --git a/src/memory-models/mmcc_main.cpp b/src/memory-models/mmcc_main.cpp
index 9e73843b3ce..27e9b169495 100644
--- a/src/memory-models/mmcc_main.cpp
+++ b/src/memory-models/mmcc_main.cpp
@@ -16,7 +16,9 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifdef _MSC_VER
 int wmain(int argc, const wchar_t **argv_wide)
 {
-  const char **argv=narrow_argv(argc, argv_wide);
+  auto vec=narrow_argv(argc, argv_wide);
+  auto narrow=to_c_str_array(std::begin(vec), std::end(vec));
+  auto argv=narrow.data();
 #else
 int main(int argc, const char **argv)
 {
diff --git a/src/symex/symex_main.cpp b/src/symex/symex_main.cpp
index 2407aad561c..9dd7cdd1e25 100644
--- a/src/symex/symex_main.cpp
+++ b/src/symex/symex_main.cpp
@@ -16,14 +16,13 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifdef _MSC_VER
 int wmain(int argc, const wchar_t **argv_wide)
 {
-  const char **argv=narrow_argv(argc, argv_wide);
-  symex_parse_optionst parse_options(argc, argv);
-  return parse_options.main();
-}
+  auto vec=narrow_argv(argc, argv_wide);
+  auto narrow=to_c_str_array(std::begin(vec), std::end(vec));
+  auto argv=narrow.data();
 #else
 int main(int argc, const char **argv)
 {
+#endif
   symex_parse_optionst parse_options(argc, argv);
   return parse_options.main();
 }
-#endif
diff --git a/src/util/freer.h b/src/util/freer.h
new file mode 100644
index 00000000000..72b6faeab70
--- /dev/null
+++ b/src/util/freer.h
@@ -0,0 +1,33 @@
+/*******************************************************************\
+
+Module:
+
+Author: Reuben Thomas, reuben.thomas@diffblue.com
+
+\*******************************************************************/
+
+#ifndef CPROVER_UTIL_FREER_H
+#define CPROVER_UTIL_FREER_H
+
+#include <cstdlib>
+#include <utility>
+
+/// A functor wrapping `std::free`. Can be used as the deleter of a unique_ptr
+/// to free memory originally allocated by `std::malloc`. This is primarily
+/// useful for interfacing with C APIs in a memory-safe way.
+/// Note that the approach of using an empty functor as a unique_ptr deleter
+/// does not impose any space overhead on the unique_ptr instance, whereas
+/// using a function-pointer as the deleter requires the unique_ptr to store
+/// this function pointer internally, effectively doubling the size of the
+/// object. Therefore, `std::unique_ptr<T, freert>` should be preferred to
+/// `std::unique_ptr<T, decltype(&std::free)>`.
+struct freert
+{
+  template <typename T>
+  void operator()(T &&t) const
+  {
+    free(std::forward<T>(t));
+  }
+};
+
+#endif
diff --git a/src/util/invariant.cpp b/src/util/invariant.cpp
index b0047cccf40..61fdb3325a2 100644
--- a/src/util/invariant.cpp
+++ b/src/util/invariant.cpp
@@ -6,9 +6,11 @@ Author: Martin Brain, martin.brain@diffblue.com
 
 \*******************************************************************/
 
-
 #include "invariant.h"
 
+#include "util/freer.h"
+
+#include <memory>
 #include <string>
 #include <sstream>
 
@@ -56,18 +58,16 @@ static bool output_demangled_name(
     std::string mangled(working.substr(start+1, length));
 
     int demangle_success=1;
-    char *demangled=
-      abi::__cxa_demangle(mangled.c_str(), NULL, 0, &demangle_success);
+    std::unique_ptr<char, freert> demangled(
+      abi::__cxa_demangle(mangled.c_str(), NULL, 0, &demangle_success));
 
     if(demangle_success==0)
     {
       out << working.substr(0, start+1)
-          << demangled
+          << demangled.get()
           << working.substr(end);
       return_value=true;
     }
-
-    free(demangled);
   }
 
   return return_value;
@@ -115,17 +115,16 @@ void check_invariant(
     void * stack[50] = {};
 
     std::size_t entries=backtrace(stack, sizeof(stack) / sizeof(void *));
-    char **description=backtrace_symbols(stack, entries);
+    std::unique_ptr<char*, freert> description(
+      backtrace_symbols(stack, entries));
 
     for(std::size_t i=0; i<entries; i++)
     {
-      if(!output_demangled_name(out, description[i]))
-        out << description[i];
+      if(!output_demangled_name(out, description.get()[i]))
+        out << description.get()[i];
       out << '\n' << std::flush;
     }
 
-    free(description);
-
 #else
     out << "Backtraces not supported\n" << std::flush;
 #endif
diff --git a/src/util/json_expr.cpp b/src/util/json_expr.cpp
index a9135f9f5ce..9663075b41f 100644
--- a/src/util/json_expr.cpp
+++ b/src/util/json_expr.cpp
@@ -235,12 +235,17 @@ json_objectt json(
 
       std::unique_ptr<languaget> lang;
       if(mode==ID_unknown)
-        lang=std::unique_ptr<languaget>(get_default_language());
+      {
+        lang=get_default_language();
+      }
       else
       {
-        lang=std::unique_ptr<languaget>(get_language_from_mode(mode));
-        if(!lang)
-          lang=std::unique_ptr<languaget>(get_default_language());
+        lang=get_language_from_mode(mode);
+      }
+
+      if(!lang)
+      {
+        lang=get_default_language();
       }
 
       std::string type_string;
diff --git a/src/util/language.h b/src/util/language.h
index fac0e13aed7..4eb69894f54 100644
--- a/src/util/language.h
+++ b/src/util/language.h
@@ -15,6 +15,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <set>
 #include <iosfwd>
 #include <string>
+#include <memory> // unique_ptr
+
 #include <util/symbol.h>
 #include <util/std_types.h>
 #include <goto-programs/system_library_symbols.h>
@@ -114,7 +116,7 @@ class languaget:public messaget
     exprt &expr,
     const namespacet &ns)=0;
 
-  virtual languaget *new_language()=0;
+  virtual std::unique_ptr<languaget> new_language()=0;
 
   void set_should_generate_opaque_method_stubs(bool should_generate_stubs);
 
diff --git a/src/util/language_file.cpp b/src/util/language_file.cpp
index 891e70565b0..e01dbf42b9a 100644
--- a/src/util/language_file.cpp
+++ b/src/util/language_file.cpp
@@ -14,16 +14,18 @@ Author: Daniel Kroening, kroening@kroening.com
 
 language_filet::language_filet(const language_filet &rhs):
   modules(rhs.modules),
-  language(rhs.language==NULL?NULL:rhs.language->new_language()),
+  language(rhs.language?rhs.language->new_language():nullptr),
   filename(rhs.filename)
 {
 }
 
-language_filet::~language_filet()
-{
-  if(language!=NULL)
-    delete language;
-}
+/// To avoid compiler errors, the complete definition of a pointed-to type must
+/// be visible at the point at which the unique_ptr destructor is created.  In
+/// this case, the pointed-to type is forward-declared, so we have to place the
+/// destructor in the source file, where the full definition is availible.
+language_filet::~language_filet()=default;
+
+language_filet::language_filet()=default;
 
 void language_filet::get_modules()
 {
@@ -51,8 +53,9 @@ void language_filest::set_should_generate_opaque_method_stubs(
 {
   for(file_mapt::value_type &language_file_entry : file_map)
   {
-    languaget *language=language_file_entry.second.language;
-    language->set_should_generate_opaque_method_stubs(stubs_enabled);
+    assert(language_file_entry.second.language!=nullptr);
+    auto &language=*language_file_entry.second.language;
+    language.set_should_generate_opaque_method_stubs(stubs_enabled);
   }
 }
 
diff --git a/src/util/language_file.h b/src/util/language_file.h
index 6c4b8a07d06..fa0d7dbdef6 100644
--- a/src/util/language_file.h
+++ b/src/util/language_file.h
@@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <set>
 #include <map>
 #include <string>
+#include <memory> // unique_ptr
 
 #include "message.h"
 
@@ -21,7 +22,7 @@ class symbol_tablet;
 class language_filet;
 class languaget;
 
-class language_modulet
+class language_modulet final
 {
 public:
   std::string name;
@@ -32,13 +33,13 @@ class language_modulet
   { type_checked=in_progress=false; }
 };
 
-class language_filet
+class language_filet final
 {
 public:
   typedef std::set<std::string> modulest;
   modulest modules;
 
-  languaget *language;
+  std::unique_ptr<languaget> language;
   std::string filename;
 
   void get_modules();
@@ -47,12 +48,9 @@ class language_filet
     const irep_idt &id,
     symbol_tablet &symbol_table);
 
+  language_filet();
   language_filet(const language_filet &rhs);
 
-  language_filet():language(NULL)
-  {
-  }
-
   ~language_filet();
 };
 
diff --git a/src/util/make_unique.h b/src/util/make_unique.h
new file mode 100644
index 00000000000..0f4ba41ac3e
--- /dev/null
+++ b/src/util/make_unique.h
@@ -0,0 +1,24 @@
+/*******************************************************************\
+
+Module: Really simple unique_ptr utilities
+
+Author: Reuben Thomas, reuben.thomas@diffblue.com
+
+\*******************************************************************/
+
+#ifndef CPROVER_UTIL_MAKE_UNIQUE_H
+#define CPROVER_UTIL_MAKE_UNIQUE_H
+
+#include <memory> // unique_ptr
+
+// This is a stand-in for std::make_unique, which isn't part of the standard
+// library until C++14.  When we move to C++14, we should do a find-and-replace
+// on this to use std::make_unique instead.
+
+template<typename T, typename... Ts>
+std::unique_ptr<T> util_make_unique(Ts &&... ts)
+{
+  return std::unique_ptr<T>(new T(std::forward<Ts>(ts)...));
+}
+
+#endif
diff --git a/src/util/mp_arith.cpp b/src/util/mp_arith.cpp
index 6afa8451057..4ddefb9c0f6 100644
--- a/src/util/mp_arith.cpp
+++ b/src/util/mp_arith.cpp
@@ -10,6 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <cstdlib>
 #include <cctype>
 #include <cassert>
+#include <vector>
 
 #include <sstream>
 #include <ostream>
@@ -80,13 +81,11 @@ const std::string integer2binary(const mp_integer &n, std::size_t width)
   }
 
   std::size_t len = a.digits(2) + 2;
-  char *buffer=new char[len];
-  char *s = a.as_string(buffer, len, 2);
+  std::vector<char> buffer(len);
+  char *s = a.as_string(buffer.data(), len, 2);
 
   std::string result(s);
 
-  delete[] buffer;
-
   if(result.size()<width)
   {
     std::string fill;
@@ -108,13 +107,11 @@ const std::string integer2binary(const mp_integer &n, std::size_t width)
 const std::string integer2string(const mp_integer &n, unsigned base)
 {
   unsigned len = n.digits(base) + 2;
-  char *buffer=new char[len];
-  char *s = n.as_string(buffer, len, base);
+  std::vector<char> buffer(len);
+  char *s = n.as_string(buffer.data(), len, base);
 
   std::string result(s);
 
-  delete[] buffer;
-
   return result;
 }
 
diff --git a/src/util/pipe_stream.cpp b/src/util/pipe_stream.cpp
index 9a9c6297018..d908a2b9631 100644
--- a/src/util/pipe_stream.cpp
+++ b/src/util/pipe_stream.cpp
@@ -105,19 +105,17 @@ int pipe_streamt::run()
   for(const auto &s : args)
         command += L" " + ::widen(s);
 
-  LPWSTR lpCommandLine = new wchar_t[command.length()+1];
+  std::vector<wchar_t> lpCommandLine(command.length()+1);
 
   #ifdef _MSC_VER
-  wcscpy_s(lpCommandLine, command.length()+1, command.c_str());
+  wcscpy_s(lpCommandLine.data(), command.length()+1, command.c_str());
   #else
-  wcsncpy(lpCommandLine, command.c_str(), command.length()+1);
+  wcsncpy(lpCommandLine.data(), command.c_str(), command.length()+1);
   #endif
 
-  BOOL ret=CreateProcessW(NULL, lpCommandLine, NULL, NULL, TRUE,
+  BOOL ret=CreateProcessW(NULL, lpCommandLine.data(), NULL, NULL, TRUE,
                           CREATE_NO_WINDOW, NULL, NULL, &si, &pi);
 
-  delete lpCommandLine; // clean up
-
   if(!ret)
     return -1;
 
@@ -146,7 +144,7 @@ int pipe_streamt::run()
     dup2(in[0], STDIN_FILENO);
     dup2(out[1], STDOUT_FILENO);
 
-    char **_argv=new char * [args.size()+2];
+    std::vector<char *> _argv(args.size()+2);
 
     _argv[0]=strdup(executable.c_str());
 
@@ -160,7 +158,7 @@ int pipe_streamt::run()
 
     _argv[args.size()+1]=NULL;
 
-    int result=execvp(executable.c_str(), _argv);
+    int result=execvp(executable.c_str(), _argv.data());
 
     if(result==-1)
       perror(0);
@@ -217,14 +215,14 @@ int pipe_streamt::wait()
 filedescriptor_streambuft::filedescriptor_streambuft():
   #ifdef _WIN32
   proc_in(INVALID_HANDLE_VALUE),
-  proc_out(INVALID_HANDLE_VALUE)
+  proc_out(INVALID_HANDLE_VALUE),
   #else
   proc_in(STDOUT_FILENO),
-  proc_out(STDIN_FILENO)
+  proc_out(STDIN_FILENO),
   #endif
+  in_buffer(READ_BUFFER_SIZE)
 {
-  in_buffer=new char[READ_BUFFER_SIZE];
-  setg(in_buffer, in_buffer, in_buffer);
+  setg(in_buffer.data(), in_buffer.data(), in_buffer.data());
 }
 
 /// Destructor
@@ -247,8 +245,6 @@ filedescriptor_streambuft::~filedescriptor_streambuft()
     close(proc_out);
 
   #endif
-
-  delete in_buffer;
 }
 
 /// write one character to the piped process
diff --git a/src/util/pipe_stream.h b/src/util/pipe_stream.h
index e03169ffd1a..57993754d62 100644
--- a/src/util/pipe_stream.h
+++ b/src/util/pipe_stream.h
@@ -43,7 +43,7 @@ class filedescriptor_streambuft:public std::streambuf
 
 protected:
   HANDLE proc_in, proc_out;
-  char *in_buffer;
+  std::vector<char> in_buffer;
 
   int_type overflow(int_type);
   std::streamsize xsputn(const char *, std::streamsize);
diff --git a/src/util/run.cpp b/src/util/run.cpp
index d29082ea0b0..8987f534f4e 100644
--- a/src/util/run.cpp
+++ b/src/util/run.cpp
@@ -62,7 +62,7 @@ int run(
   for(std::size_t i=0; i<argv.size(); i++)
     wargv[i]=widen(argv[i]);
 
-  const wchar_t **_argv=new const wchar_t * [argv.size()+1];
+  std::vector<const wchar_t *> _argv(argv.size()+1);
 
   for(std::size_t i=0; i<wargv.size(); i++)
     _argv[i]=wargv[i].c_str();
@@ -73,9 +73,7 @@ int run(
 
   std::wstring wide_what=widen(what);
 
-  int status=_wspawnvp(_P_WAIT, wide_what.c_str(), _argv);
-
-  delete[] _argv;
+  int status=_wspawnvp(_P_WAIT, wide_what.c_str(), _argv.data());
 
   return status;
 
@@ -120,7 +118,7 @@ int run(
       remove_signal_catcher();
       sigprocmask(SIG_SETMASK, &old_mask, NULL);
 
-      char **_argv=new char * [argv.size()+1];
+      std::vector<char *> _argv(argv.size()+1);
       for(std::size_t i=0; i<argv.size(); i++)
         _argv[i]=strdup(argv[i].c_str());
 
@@ -130,7 +128,7 @@ int run(
         dup2(stdin_fd, STDIN_FILENO);
       if(stdout_fd!=STDOUT_FILENO)
         dup2(stdout_fd, STDOUT_FILENO);
-      execvp(what.c_str(), _argv);
+      execvp(what.c_str(), _argv.data());
 
       /* usually no return */
       return 1;
diff --git a/src/util/sharing_node.h b/src/util/sharing_node.h
index 9f8cc0a4416..c2501f7f345 100644
--- a/src/util/sharing_node.h
+++ b/src/util/sharing_node.h
@@ -64,7 +64,7 @@ class sharing_nodet
     d.k=std::make_shared<key_type>(k);
 
     _sn_assert(d.m==nullptr);
-    d.m.reset(new mapped_type(m));
+    d.m=std::make_shared<mapped_type>(m);
   }
 
   sharing_nodet(const self_type &other)
@@ -266,7 +266,7 @@ class sharing_nodet
       if(d.is_leaf())
       {
         _sn_assert(m==nullptr);
-        m.reset(new mapped_type(*d.m));
+        m=std::make_shared<mapped_type>(*d.m);
       }
     }
 
@@ -277,7 +277,7 @@ class sharing_nodet
     }
 
     std::shared_ptr<key_type> k;
-    std::unique_ptr<mapped_type> m;
+    std::shared_ptr<mapped_type> m;
 
     subt sub;
     containert con;
@@ -339,8 +339,8 @@ class sharing_nodet
 
 template <class keyT, class valueT, class predT, bool no_sharing>
 std::shared_ptr<typename sharing_nodet<keyT, valueT, predT, no_sharing>::dt>
-  sharing_nodet<keyT, valueT, predT, no_sharing>::empty_data(
-    new sharing_nodet<keyT, valueT, predT, no_sharing>::dt());
+  sharing_nodet<keyT, valueT, predT, no_sharing>::empty_data=
+    std::make_shared<sharing_nodet<keyT, valueT, predT, no_sharing>::dt>();
 
 template <class keyT, class valueT, class predT, bool no_sharing>
 sharing_nodet<keyT, valueT, predT, no_sharing>
diff --git a/src/util/unicode.cpp b/src/util/unicode.cpp
index bf8ce51531d..6f266b904a2 100644
--- a/src/util/unicode.cpp
+++ b/src/util/unicode.cpp
@@ -153,17 +153,15 @@ std::string utf32_to_utf8(const std::basic_string<unsigned int> &s)
   return result;
 }
 
-const char **narrow_argv(int argc, const wchar_t **argv_wide)
+std::vector<std::string> narrow_argv(int argc, const wchar_t **argv_wide)
 {
   if(argv_wide==NULL)
-    return NULL;
+    return std::vector<std::string>();
 
-  // the following never gets deleted
-  const char **argv_narrow=new const char *[argc+1];
-  argv_narrow[argc]=0;
+  std::vector<std::string> argv_narrow(argc);
 
-  for(int i=0; i<argc; i++)
-    argv_narrow[i]=strdup(narrow(argv_wide[i]).c_str());
+  for(int i=0; i!=argc; ++i)
+    argv_narrow[i]=narrow(argv_wide[i]);
 
   return argv_narrow;
 }
diff --git a/src/util/unicode.h b/src/util/unicode.h
index 93e83c5b64f..d30d978facb 100644
--- a/src/util/unicode.h
+++ b/src/util/unicode.h
@@ -10,7 +10,9 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_UTIL_UNICODE_H
 #define CPROVER_UTIL_UNICODE_H
 
+#include <algorithm>
 #include <string>
+#include <vector>
 
 // we follow the ideas suggested at
 // http://www.utf8everywhere.org/
@@ -26,6 +28,18 @@ std::wstring utf8_to_utf16_big_endian(const std::string &);
 std::wstring utf8_to_utf16_little_endian(const std::string &);
 std::string utf16_little_endian_to_ascii(const std::wstring &in);
 
-const char **narrow_argv(int argc, const wchar_t **argv_wide);
+std::vector<std::string> narrow_argv(int argc, const wchar_t **argv_wide);
+
+template <typename It>
+std::vector<const char *> to_c_str_array(It b, It e)
+{
+  // Assumes that walking the range will be faster than repeated allocation
+  std::vector<const char *> ret(std::distance(b, e) + 1, nullptr);
+  std::transform(b, e, std::begin(ret), [] (const std::string & s)
+    {
+      return s.c_str();
+    });
+  return ret;
+}
 
 #endif // CPROVER_UTIL_UNICODE_H