diff --git a/src/util/Makefile b/src/util/Makefile
index 74fc5aec412..6afa460e650 100644
--- a/src/util/Makefile
+++ b/src/util/Makefile
@@ -41,7 +41,6 @@ SRC = arith_tools.cpp \
       lispexpr.cpp \
       lispirep.cpp \
       memory_info.cpp \
-      memory_limit.cpp \
       merge_irep.cpp \
       message.cpp \
       mp_arith.cpp \
@@ -81,7 +80,6 @@ SRC = arith_tools.cpp \
       string_container.cpp \
       string_hash.cpp \
       string_utils.cpp \
-      substitute.cpp \
       symbol.cpp \
       symbol_table_base.cpp \
       symbol_table.cpp \
diff --git a/src/util/memory_limit.cpp b/src/util/memory_limit.cpp
deleted file mode 100644
index c312b6bea08..00000000000
--- a/src/util/memory_limit.cpp
+++ /dev/null
@@ -1,48 +0,0 @@
-/*******************************************************************\
-
-Module:
-
-Author: Peter Schrammel, peter.schrammel@diffblue.com
-
-\*******************************************************************/
-
-#include "memory_limit.h"
-
-#ifdef __linux__
-#include <sys/resource.h>
-#endif
-
-#include <ostream>
-
-/// Outputs the memory limits to the given output stream
-/// \param out: output stream
-void memory_limits(std::ostream &out)
-{
-#ifdef __linux__
-  struct rlimit mem_limit;
-  getrlimit(RLIMIT_AS, &mem_limit);
-
-  out << "  soft limit: " << mem_limit.rlim_cur << '\n';
-  out << "  hard limit: " << mem_limit.rlim_max;
-#else
-  out << "  not supported";
-#endif
-}
-
-/// Sets the soft memory limit of the current process
-/// \param soft_limit: the soft limit in bytes
-/// \return: true if setting the limit succeeded
-bool set_memory_limit(std::size_t soft_limit)
-{
-#ifdef __linux__
-  struct rlimit mem_limit;
-  getrlimit(RLIMIT_AS, &mem_limit);
-  mem_limit.rlim_cur = soft_limit;
-  setrlimit(RLIMIT_AS, &mem_limit);
-  getrlimit(RLIMIT_AS, &mem_limit);
-  return mem_limit.rlim_cur == soft_limit;
-#else
-  // not supported
-  return false;
-#endif
-}
diff --git a/src/util/memory_limit.h b/src/util/memory_limit.h
deleted file mode 100644
index 53aaef125e9..00000000000
--- a/src/util/memory_limit.h
+++ /dev/null
@@ -1,18 +0,0 @@
-/*******************************************************************\
-
-Module:
-
-Author: Peter Schrammel, peter.schrammel@diffblue.com
-
-\*******************************************************************/
-
-#ifndef CPROVER_UTIL_MEMORY_LIMIT_H
-#define CPROVER_UTIL_MEMORY_LIMIT_H
-
-#include <cstddef> // size_t
-#include <iosfwd>
-
-void memory_limits(std::ostream &);
-bool set_memory_limit(std::size_t soft_limit);
-
-#endif // CPROVER_UTIL_MEMORY_LIMIT_H
diff --git a/src/util/substitute.cpp b/src/util/substitute.cpp
deleted file mode 100644
index 39010d79676..00000000000
--- a/src/util/substitute.cpp
+++ /dev/null
@@ -1,31 +0,0 @@
-/*******************************************************************\
-
-Module:
-
-Author: Daniel Kroening, kroening@kroening.com
-
-\*******************************************************************/
-
-#include "substitute.h"
-
-#include <cassert>
-
-void substitute(
-  std::string &dest,
-  const std::string &what,
-  const std::string &by)
-{
-  assert(!what.empty());
-
-  while(true)
-  {
-    std::string::size_type pos=dest.find(what);
-
-    if(pos==std::string::npos)
-      return; // done
-
-    dest.replace(dest.begin()+pos,
-                 dest.begin()+pos+what.size(),
-                 by);
-  }
-}
diff --git a/src/util/substitute.h b/src/util/substitute.h
deleted file mode 100644
index ed3ea5293a0..00000000000
--- a/src/util/substitute.h
+++ /dev/null
@@ -1,20 +0,0 @@
-/*******************************************************************\
-
-Module:
-
-Author: Daniel Kroening, kroening@kroening.com
-
-\*******************************************************************/
-
-
-#ifndef CPROVER_UTIL_SUBSTITUTE_H
-#define CPROVER_UTIL_SUBSTITUTE_H
-
-#include <string>
-
-void substitute(
-  std::string &dest,
-  const std::string &what,
-  const std::string &by);
-
-#endif // CPROVER_UTIL_SUBSTITUTE_H