diff --git a/src/goto-harness/recursive_initialization.cpp b/src/goto-harness/recursive_initialization.cpp
index 5bc87a30b19..92c0e4d11ea 100644
--- a/src/goto-harness/recursive_initialization.cpp
+++ b/src/goto-harness/recursive_initialization.cpp
@@ -164,7 +164,8 @@ void recursive_initializationt::initialize_nondet(
     lhs.id() != ID_symbol ||
     !is_array_size_parameter(to_symbol_expr(lhs).get_identifier()))
   {
-    body.add(code_assignt{lhs, side_effect_expr_nondett{lhs.type()}});
+    body.add(code_assignt{
+      lhs, side_effect_expr_nondett{lhs.type(), source_locationt{}}});
   }
 }
 
diff --git a/src/goto-instrument/cover.cpp b/src/goto-instrument/cover.cpp
index dfe80ef25bc..41897b67826 100644
--- a/src/goto-instrument/cover.cpp
+++ b/src/goto-instrument/cover.cpp
@@ -18,7 +18,6 @@ Date: May 2016
 #include <util/make_unique.h>
 #include <util/cmdline.h>
 #include <util/options.h>
-#include <util/deprecate.h>
 
 #include <goto-programs/remove_skip.h>
 
@@ -49,33 +48,6 @@ void instrument_cover_goals(
   instrumenters(function_id, goto_program, *basic_blocks);
 }
 
-/// Instruments goto program for a given coverage criterion
-/// \param symbol_table: the symbol table
-/// \param function_id: name of \p goto_program
-/// \param goto_program: the goto program
-/// \param criterion: the coverage criterion
-/// \param message_handler: a message handler
-/// \deprecated use instrument_cover_goals(goto_programt &goto_program,
-/// const cover_instrumenterst &instrumenters,
-/// message_handlert &message_handler, const irep_idt mode) instead
-DEPRECATED(SINCE(2018, 2, 9, "use instrument_cover_goals goto_programt &..."))
-void instrument_cover_goals(
-  const symbol_tablet &symbol_table,
-  const irep_idt &function_id,
-  goto_programt &goto_program,
-  coverage_criteriont criterion,
-  message_handlert &message_handler)
-{
-  goal_filterst goal_filters;
-  goal_filters.add(util_make_unique<internal_goals_filtert>(message_handler));
-
-  cover_instrumenterst instrumenters;
-  instrumenters.add_from_criterion(criterion, symbol_table, goal_filters);
-
-  instrument_cover_goals(
-    function_id, goto_program, instrumenters, ID_unknown, message_handler);
-}
-
 /// Create and add an instrumenter based on the given criterion
 /// \param criterion: the coverage criterion
 /// \param symbol_table: the symbol table
diff --git a/src/goto-symex/ssa_step.cpp b/src/goto-symex/ssa_step.cpp
index 02a6199494f..496d5a438a2 100644
--- a/src/goto-symex/ssa_step.cpp
+++ b/src/goto-symex/ssa_step.cpp
@@ -7,120 +7,8 @@ Author: Romain Brenguier <romain.brenguier@diffblue.com>
 *******************************************************************/
 
 #include "ssa_step.h"
-#include <langapi/language_util.h>
-#include <util/format_expr.h>
-
-void SSA_stept::output(const namespacet &ns, std::ostream &out) const
-{
-  out << "Thread " << source.thread_nr;
-
-  if(source.pc->source_location.is_not_nil())
-    out << " " << source.pc->source_location << '\n';
-  else
-    out << '\n';
 
-  switch(type)
-  {
-  case goto_trace_stept::typet::ASSERT:
-    out << "ASSERT " << from_expr(ns, source.function_id, cond_expr) << '\n';
-    break;
-  case goto_trace_stept::typet::ASSUME:
-    out << "ASSUME " << from_expr(ns, source.function_id, cond_expr) << '\n';
-    break;
-  case goto_trace_stept::typet::LOCATION:
-    out << "LOCATION" << '\n';
-    break;
-  case goto_trace_stept::typet::INPUT:
-    out << "INPUT" << '\n';
-    break;
-  case goto_trace_stept::typet::OUTPUT:
-    out << "OUTPUT" << '\n';
-    break;
-
-  case goto_trace_stept::typet::DECL:
-    out << "DECL" << '\n';
-    out << from_expr(ns, source.function_id, ssa_lhs) << '\n';
-    break;
-
-  case goto_trace_stept::typet::ASSIGNMENT:
-    out << "ASSIGNMENT (";
-    switch(assignment_type)
-    {
-    case symex_targett::assignment_typet::HIDDEN:
-      out << "HIDDEN";
-      break;
-    case symex_targett::assignment_typet::STATE:
-      out << "STATE";
-      break;
-    case symex_targett::assignment_typet::VISIBLE_ACTUAL_PARAMETER:
-      out << "VISIBLE_ACTUAL_PARAMETER";
-      break;
-    case symex_targett::assignment_typet::HIDDEN_ACTUAL_PARAMETER:
-      out << "HIDDEN_ACTUAL_PARAMETER";
-      break;
-    case symex_targett::assignment_typet::PHI:
-      out << "PHI";
-      break;
-    case symex_targett::assignment_typet::GUARD:
-      out << "GUARD";
-      break;
-    default:
-    {
-    }
-    }
-
-    out << ")\n";
-    break;
-
-  case goto_trace_stept::typet::DEAD:
-    out << "DEAD\n";
-    break;
-  case goto_trace_stept::typet::FUNCTION_CALL:
-    out << "FUNCTION_CALL\n";
-    break;
-  case goto_trace_stept::typet::FUNCTION_RETURN:
-    out << "FUNCTION_RETURN\n";
-    break;
-  case goto_trace_stept::typet::CONSTRAINT:
-    out << "CONSTRAINT\n";
-    break;
-  case goto_trace_stept::typet::SHARED_READ:
-    out << "SHARED READ\n";
-    break;
-  case goto_trace_stept::typet::SHARED_WRITE:
-    out << "SHARED WRITE\n";
-    break;
-  case goto_trace_stept::typet::ATOMIC_BEGIN:
-    out << "ATOMIC_BEGIN\n";
-    break;
-  case goto_trace_stept::typet::ATOMIC_END:
-    out << "AUTOMIC_END\n";
-    break;
-  case goto_trace_stept::typet::SPAWN:
-    out << "SPAWN\n";
-    break;
-  case goto_trace_stept::typet::MEMORY_BARRIER:
-    out << "MEMORY_BARRIER\n";
-    break;
-  case goto_trace_stept::typet::GOTO:
-    out << "IF " << from_expr(ns, source.function_id, cond_expr) << " GOTO\n";
-    break;
-
-  default:
-    UNREACHABLE;
-  }
-
-  if(is_assert() || is_assume() || is_assignment() || is_constraint())
-    out << from_expr(ns, source.function_id, cond_expr) << '\n';
-
-  if(is_assert() || is_constraint())
-    out << comment << '\n';
-
-  if(is_shared_read() || is_shared_write())
-    out << from_expr(ns, source.function_id, ssa_lhs) << '\n';
-
-  out << "Guard: " << from_expr(ns, source.function_id, guard) << '\n';
-}
+#include <util/format_expr.h>
 
 void SSA_stept::output(std::ostream &out) const
 {
diff --git a/src/goto-symex/ssa_step.h b/src/goto-symex/ssa_step.h
index 702d62b5417..6d2262e6daf 100644
--- a/src/goto-symex/ssa_step.h
+++ b/src/goto-symex/ssa_step.h
@@ -191,9 +191,6 @@ class SSA_stept
   {
   }
 
-  DEPRECATED(SINCE(2018, 4, 23, "Use output without ns param"))
-  void output(const namespacet &ns, std::ostream &out) const;
-
   void output(std::ostream &out) const;
 
   void validate(const namespacet &ns, const validation_modet vm) const;
diff --git a/src/goto-symex/symex_target_equation.cpp b/src/goto-symex/symex_target_equation.cpp
index 8b64487adad..9eb7d711071 100644
--- a/src/goto-symex/symex_target_equation.cpp
+++ b/src/goto-symex/symex_target_equation.cpp
@@ -17,9 +17,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/throw_with_nested.h>
 #include <util/unwrap_nested_exception.h>
 
-// Can be removed once deprecated SSA_stept::output is removed
-#include <langapi/language_util.h>
-
 #include <solvers/flattening/bv_conversion_exceptions.h>
 #include <solvers/prop/literal_expr.h>
 #include <solvers/prop/prop.h>
@@ -682,13 +679,11 @@ void symex_target_equationt::merge_ireps(SSA_stept &SSA_step)
   // converted_io_args is merged in convert_io
 }
 
-void symex_target_equationt::output(
-  std::ostream &out,
-  const namespacet &ns) const
+void symex_target_equationt::output(std::ostream &out) const
 {
   for(const auto &step : SSA_steps)
   {
-    step.output(ns, out);
+    step.output(out);
     out << "--------------\n";
   }
 }
diff --git a/src/goto-symex/symex_target_equation.h b/src/goto-symex/symex_target_equation.h
index c74440c3778..0776967602f 100644
--- a/src/goto-symex/symex_target_equation.h
+++ b/src/goto-symex/symex_target_equation.h
@@ -255,7 +255,7 @@ class symex_target_equationt:public symex_targett
     return it;
   }
 
-  void output(std::ostream &out, const namespacet &ns) const;
+  void output(std::ostream &out) const;
 
   void clear()
   {
diff --git a/src/util/mp_arith.cpp b/src/util/mp_arith.cpp
index 9d3cde196e4..b9a7ad4f55a 100644
--- a/src/util/mp_arith.cpp
+++ b/src/util/mp_arith.cpp
@@ -186,28 +186,6 @@ const mp_integer binary2integer(const std::string &n, bool is_signed)
   #endif
 }
 
-mp_integer::ullong_t integer2ulong(const mp_integer &n)
-{
-  PRECONDITION(n.is_ulong());
-  return n.to_ulong();
-}
-
-std::size_t integer2size_t(const mp_integer &n)
-{
-  PRECONDITION(n>=0 && n<=std::numeric_limits<std::size_t>::max());
-  PRECONDITION(n.is_ulong());
-  mp_integer::ullong_t ull = n.to_ulong();
-  return (std::size_t) ull;
-}
-
-unsigned integer2unsigned(const mp_integer &n)
-{
-  PRECONDITION(n>=0 && n<=std::numeric_limits<unsigned>::max());
-  PRECONDITION(n.is_ulong());
-  mp_integer::ullong_t ull = n.to_ulong();
-  return (unsigned)ull;
-}
-
 /// bitwise binary operation over two integers, given as a functor
 /// \param a: the first integer
 /// \param b: the second integer
diff --git a/src/util/mp_arith.h b/src/util/mp_arith.h
index 674a6228d3e..99a6175c2b7 100644
--- a/src/util/mp_arith.h
+++ b/src/util/mp_arith.h
@@ -14,7 +14,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <string>
 
 #include "big-int/bigint.hh"
-#include "deprecate.h"
 
 // NOLINTNEXTLINE(readability/identifiers)
 typedef BigInt mp_integer;
@@ -49,17 +48,4 @@ const mp_integer string2integer(const std::string &, unsigned base=10);
 const std::string integer2binary(const mp_integer &, std::size_t width);
 const mp_integer binary2integer(const std::string &, bool is_signed);
 
-/// \deprecated use numeric_cast_v<unsigned long long> instead
-DEPRECATED(
-  SINCE(2017, 11, 13, "Use numeric_cast_v<unsigned long long> instead"))
-mp_integer::ullong_t integer2ulong(const mp_integer &);
-
-/// \deprecated use numeric_cast_v<std::size_t> instead
-DEPRECATED(SINCE(2017, 11, 13, "Use numeric_cast_v<std::size_t> instead"))
-std::size_t integer2size_t(const mp_integer &);
-
-/// \deprecated use numeric_cast_v<unsigned> instead
-DEPRECATED(SINCE(2017, 11, 13, "Use numeric_cast_v<unsigned> instead"))
-unsigned integer2unsigned(const mp_integer &);
-
 #endif // CPROVER_UTIL_MP_ARITH_H
diff --git a/src/util/std_code.h b/src/util/std_code.h
index 8e80cf2f753..5bc2934f782 100644
--- a/src/util/std_code.h
+++ b/src/util/std_code.h
@@ -34,11 +34,6 @@ Author: Daniel Kroening, kroening@kroening.com
 class codet:public exprt
 {
 public:
-  DEPRECATED(SINCE(2018, 6, 28, "use codet(statement) instead"))
-  codet() : exprt(ID_code, empty_typet())
-  {
-  }
-
   /// \param statement: Specifies the type of the `codet` to be constructed,
   ///   e.g. `ID_block` for a \ref code_blockt or `ID_assign` for a
   ///   \ref code_assignt.
@@ -537,12 +532,6 @@ inline code_deadt &to_code_dead(codet &code)
 class code_assumet:public codet
 {
 public:
-  DEPRECATED(SINCE(2018, 6, 28, "use code_assumet(expr) instead"))
-  code_assumet():codet(ID_assume)
-  {
-    operands().resize(1);
-  }
-
   explicit code_assumet(exprt expr) : codet(ID_assume, {std::move(expr)})
   {
   }
@@ -595,12 +584,6 @@ inline code_assumet &to_code_assume(codet &code)
 class code_assertt:public codet
 {
 public:
-  DEPRECATED(SINCE(2018, 6, 28, "use code_assertt(expr) instead"))
-  code_assertt():codet(ID_assert)
-  {
-    operands().resize(1);
-  }
-
   explicit code_assertt(exprt expr) : codet(ID_assert, {std::move(expr)})
   {
   }
@@ -767,12 +750,6 @@ inline code_ifthenelset &to_code_ifthenelse(codet &code)
 class code_switcht:public codet
 {
 public:
-  DEPRECATED(SINCE(2018, 6, 28, "use code_switcht(value, body) instead"))
-  code_switcht():codet(ID_switch)
-  {
-    operands().resize(2);
-  }
-
   code_switcht(exprt _value, codet _body)
     : codet(ID_switch, {std::move(_value), std::move(_body)})
   {
@@ -835,12 +812,6 @@ inline code_switcht &to_code_switch(codet &code)
 class code_whilet:public codet
 {
 public:
-  DEPRECATED(SINCE(2018, 6, 28, "use code_whilet(cond, body) instead"))
-  code_whilet():codet(ID_while)
-  {
-    operands().resize(2);
-  }
-
   code_whilet(exprt _cond, codet _body)
     : codet(ID_while, {std::move(_cond), std::move(_body)})
   {
@@ -903,12 +874,6 @@ inline code_whilet &to_code_while(codet &code)
 class code_dowhilet:public codet
 {
 public:
-  DEPRECATED(SINCE(2018, 6, 28, "use code_dowhilet(cond, body) instead"))
-  code_dowhilet():codet(ID_dowhile)
-  {
-    operands().resize(2);
-  }
-
   code_dowhilet(exprt _cond, codet _body)
     : codet(ID_dowhile, {std::move(_cond), std::move(_body)})
   {
@@ -1068,11 +1033,6 @@ inline code_fort &to_code_for(codet &code)
 class code_gotot:public codet
 {
 public:
-  DEPRECATED(SINCE(2018, 6, 28, "use code_gotot(label) instead"))
-  code_gotot():codet(ID_goto)
-  {
-  }
-
   explicit code_gotot(const irep_idt &label):codet(ID_goto)
   {
     set_destination(label);
@@ -1129,14 +1089,6 @@ inline code_gotot &to_code_goto(codet &code)
 class code_function_callt:public codet
 {
 public:
-  DEPRECATED(SINCE(2018, 8, 26, "Use code_function_callt(...) instead"))
-  code_function_callt():codet(ID_function_call)
-  {
-    operands().resize(3);
-    lhs().make_nil();
-    op2().id(ID_arguments);
-  }
-
   explicit code_function_callt(exprt _function)
     : codet(
         ID_function_call,
@@ -1329,12 +1281,6 @@ inline code_returnt &to_code_return(codet &code)
 class code_labelt:public codet
 {
 public:
-  DEPRECATED(SINCE(2018, 6, 28, "use code_labelt(label, _code) instead"))
-  code_labelt():codet(ID_label)
-  {
-    operands().resize(1);
-  }
-
   DEPRECATED(SINCE(2019, 2, 6, "use code_labelt(label, _code) instead"))
   explicit code_labelt(const irep_idt &_label):codet(ID_label)
   {
@@ -1406,12 +1352,6 @@ inline code_labelt &to_code_label(codet &code)
 class code_switch_caset:public codet
 {
 public:
-  DEPRECATED(SINCE(2018, 6, 28, "use code_switch_caset(case_op, code) instead"))
-  code_switch_caset():codet(ID_switch_case)
-  {
-    operands().resize(2);
-  }
-
   code_switch_caset(exprt _case_op, codet _code)
     : codet(ID_switch_case, {std::move(_case_op), std::move(_code)})
   {
@@ -1783,12 +1723,6 @@ inline const code_asm_gcct &to_code_asm_gcc(const codet &code)
 class code_expressiont:public codet
 {
 public:
-  DEPRECATED(SINCE(2018, 6, 28, "use code_expressiont(expr) instead"))
-  code_expressiont():codet(ID_expression)
-  {
-    operands().resize(1);
-  }
-
   explicit code_expressiont(exprt expr)
     : codet(ID_expression, {std::move(expr)})
   {
@@ -1845,13 +1779,6 @@ inline const code_expressiont &to_code_expression(const codet &code)
 class side_effect_exprt : public exprt
 {
 public:
-  DEPRECATED(
-    SINCE(2018, 6, 28, "use side_effect_exprt(statement, type, loc) instead"))
-  explicit side_effect_exprt(const irep_idt &statement) : exprt(ID_side_effect)
-  {
-    set_statement(statement);
-  }
-
   DEPRECATED(
     SINCE(2018, 8, 9, "use side_effect_exprt(statement, type, loc) instead"))
   side_effect_exprt(const irep_idt &statement, const typet &_type)
@@ -1931,16 +1858,6 @@ inline const side_effect_exprt &to_side_effect_expr(const exprt &expr)
 class side_effect_expr_nondett:public side_effect_exprt
 {
 public:
-  DEPRECATED(SINCE(
-    2018,
-    6,
-    28,
-    "use side_effect_expr_nondett(statement, type, loc) instead"))
-  side_effect_expr_nondett():side_effect_exprt(ID_nondet)
-  {
-    set_nullable(true);
-  }
-
   DEPRECATED(SINCE(
     2018,
     8,
@@ -2067,36 +1984,6 @@ to_side_effect_expr_assign(const exprt &expr)
 class side_effect_expr_function_callt:public side_effect_exprt
 {
 public:
-  DEPRECATED(SINCE(
-    2018,
-    6,
-    28,
-    "use side_effect_expr_function_callt("
-    "function, arguments, type, loc) instead"))
-  side_effect_expr_function_callt()
-    : side_effect_exprt(ID_function_call, typet(), source_locationt())
-  {
-    operands().resize(2);
-    op1().id(ID_arguments);
-  }
-
-  DEPRECATED(SINCE(
-    2018,
-    8,
-    9,
-    "use side_effect_expr_function_callt("
-    "function, arguments, type, loc) instead"))
-  side_effect_expr_function_callt(
-    const exprt &_function,
-    const exprt::operandst &_arguments)
-    : side_effect_exprt(ID_function_call)
-  {
-    operands().resize(2);
-    op1().id(ID_arguments);
-    function() = _function;
-    arguments() = _arguments;
-  }
-
   DEPRECATED(SINCE(
     2018,
     8,
@@ -2180,12 +2067,6 @@ inline const side_effect_expr_function_callt
 class side_effect_expr_throwt:public side_effect_exprt
 {
 public:
-  DEPRECATED(
-    SINCE(2018, 6, 28, "use side_effect_expr_throwt(exception_list) instead"))
-  side_effect_expr_throwt():side_effect_exprt(ID_throw)
-  {
-  }
-
   side_effect_expr_throwt(
     irept exception_list,
     typet type,
diff --git a/src/util/std_types.h b/src/util/std_types.h
index a6d9c21271b..85390988cc3 100644
--- a/src/util/std_types.h
+++ b/src/util/std_types.h
@@ -34,18 +34,6 @@ class bool_typet:public typet
   }
 };
 
-/// The NIL type, i.e., an invalid type, no value.
-/// \deprecated Use `optional<typet>` instead.
-// NOLINTNEXTLINE
-class DEPRECATED(SINCE(2018, 8, 22, "Use `optional<typet>` instead.")) nil_typet
-  : public typet
-{
-public:
-  nil_typet():typet(static_cast<const typet &>(get_nil_irep()))
-  {
-  }
-};
-
 /// The empty type
 class empty_typet:public typet
 {
@@ -749,16 +737,6 @@ class code_typet:public typet
     return_type().swap(_return_type);
   }
 
-  /// \deprecated
-  DEPRECATED(SINCE(2018, 6, 4, "Use the two argument constructor instead"))
-  code_typet():typet(ID_code)
-  {
-    // make sure these properties are always there to avoid problems
-    // with irept comparisons
-    add(ID_parameters);
-    add_type(ID_return_type);
-  }
-
   // used to be argumentt -- now uses standard terminology
 
   class parametert:public exprt