diff --git a/src/java_bytecode/java_bytecode_instrument.cpp b/src/java_bytecode/java_bytecode_instrument.cpp
index 909b839d8be..07f8c4dbb49 100644
--- a/src/java_bytecode/java_bytecode_instrument.cpp
+++ b/src/java_bytecode/java_bytecode_instrument.cpp
@@ -28,20 +28,20 @@ class java_bytecode_instrumentt:public messaget
 {
 public:
   java_bytecode_instrumentt(
-    symbol_tablet &_symbol_table,
+    symbol_table_baset &_symbol_table,
     const bool _throw_runtime_exceptions,
-    message_handlert &_message_handler):
-    messaget(_message_handler),
-    symbol_table(_symbol_table),
-    throw_runtime_exceptions(_throw_runtime_exceptions),
-    message_handler(_message_handler)
-    {
-    }
+    message_handlert &_message_handler)
+    : messaget(_message_handler),
+      symbol_table(_symbol_table),
+      throw_runtime_exceptions(_throw_runtime_exceptions),
+      message_handler(_message_handler)
+  {
+  }
 
   void operator()(exprt &expr);
 
 protected:
-  symbol_tablet &symbol_table;
+  symbol_table_baset &symbol_table;
   const bool throw_runtime_exceptions;
   message_handlert &message_handler;
 
@@ -577,7 +577,7 @@ void java_bytecode_instrumentt::operator()(exprt &expr)
 ///   this flag is set to true.
 /// \param message_handler: stream to report status and warnings
 void java_bytecode_instrument_symbol(
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   symbolt &symbol,
   const bool throw_runtime_exceptions,
   message_handlert &message_handler)
diff --git a/src/java_bytecode/java_bytecode_instrument.h b/src/java_bytecode/java_bytecode_instrument.h
index d5168a418ea..d48e7758611 100644
--- a/src/java_bytecode/java_bytecode_instrument.h
+++ b/src/java_bytecode/java_bytecode_instrument.h
@@ -12,7 +12,7 @@ Date:   June 2017
 #define CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_INSTRUMENT_H
 
 void java_bytecode_instrument_symbol(
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   symbolt &symbol,
   const bool throw_runtime_exceptions,
   message_handlert &_message_handler);
diff --git a/src/java_bytecode/java_bytecode_internal_additions.cpp b/src/java_bytecode/java_bytecode_internal_additions.cpp
index bc7715ecd9b..eddf0eae59e 100644
--- a/src/java_bytecode/java_bytecode_internal_additions.cpp
+++ b/src/java_bytecode/java_bytecode_internal_additions.cpp
@@ -12,7 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/cprover_prefix.h>
 #include <util/c_types.h>
 
-void java_internal_additions(symbol_tablet &dest)
+void java_internal_additions(symbol_table_baset &dest)
 {
   // add __CPROVER_rounding_mode
 
diff --git a/src/java_bytecode/java_bytecode_internal_additions.h b/src/java_bytecode/java_bytecode_internal_additions.h
index 70362d7d685..49ea3cf658a 100644
--- a/src/java_bytecode/java_bytecode_internal_additions.h
+++ b/src/java_bytecode/java_bytecode_internal_additions.h
@@ -10,8 +10,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_INTERNAL_ADDITIONS_H
 #define CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_INTERNAL_ADDITIONS_H
 
-#include <util/symbol_table.h>
+#include <util/symbol_table_base.h>
 
-void java_internal_additions(symbol_tablet &dest);
+void java_internal_additions(symbol_table_baset &dest);
 
 #endif // CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_INTERNAL_ADDITIONS_H
diff --git a/src/java_bytecode/java_bytecode_language.cpp b/src/java_bytecode/java_bytecode_language.cpp
index 9a7b9066cde..a275cfa6ec3 100644
--- a/src/java_bytecode/java_bytecode_language.cpp
+++ b/src/java_bytecode/java_bytecode_language.cpp
@@ -355,7 +355,7 @@ void java_bytecode_languaget::convert_lazy_method(
 /// generated by string_preprocess.
 /// \param context: a symbol table
 void java_bytecode_languaget::replace_string_methods(
-  symbol_tablet &context)
+  symbol_table_baset &context)
 {
   // Symbols that have code type are potentialy to be replaced
   std::list<symbolt> code_symbols;
@@ -386,7 +386,7 @@ void java_bytecode_languaget::replace_string_methods(
   }
 }
 
-bool java_bytecode_languaget::final(symbol_tablet &symbol_table)
+bool java_bytecode_languaget::final(symbol_table_baset &symbol_table)
 {
   PRECONDITION(language_options_initialized);
 
diff --git a/src/java_bytecode/java_bytecode_language.h b/src/java_bytecode/java_bytecode_language.h
index 1cd59afeee1..f10fee616e5 100644
--- a/src/java_bytecode/java_bytecode_language.h
+++ b/src/java_bytecode/java_bytecode_language.h
@@ -108,10 +108,9 @@ class java_bytecode_languaget:public languaget
     symbol_tablet &context,
     const std::string &module) override;
 
-  void replace_string_methods(symbol_tablet &context);
+  void replace_string_methods(symbol_table_baset &context);
 
-  virtual bool final(
-    symbol_tablet &context) override;
+  virtual bool final(symbol_table_baset &context) override;
 
   void show_parse(std::ostream &out) override;
 
diff --git a/src/java_bytecode/java_entry_point.cpp b/src/java_bytecode/java_entry_point.cpp
index 2c0bd5bb6d2..1a2b83911f1 100644
--- a/src/java_bytecode/java_entry_point.cpp
+++ b/src/java_bytecode/java_entry_point.cpp
@@ -36,7 +36,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "java_types.h"
 #include "java_utils.h"
 
-static void create_initialize(symbol_tablet &symbol_table)
+static void create_initialize(symbol_table_baset &symbol_table)
 {
   // If __CPROVER_initialize already exists, replace it. It may already exist
   // if a GOTO binary provided it. This behaviour mirrors the ANSI-C frontend.
@@ -89,8 +89,8 @@ static bool is_non_null_library_global(const irep_idt &symbolid)
   return non_null_globals.count(symbolid);
 }
 
-void java_static_lifetime_init(
-  symbol_tablet &symbol_table,
+static void java_static_lifetime_init(
+  symbol_table_baset &symbol_table,
   const source_locationt &source_location,
   bool assume_init_pointers_not_null,
   const object_factory_parameterst &object_factory_parameters,
@@ -162,7 +162,7 @@ void java_static_lifetime_init(
 exprt::operandst java_build_arguments(
   const symbolt &function,
   code_blockt &init_code,
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   bool assume_init_pointers_not_null,
   object_factory_parameterst object_factory_parameters,
   const select_pointer_typet &pointer_type_selector)
@@ -246,7 +246,7 @@ void java_record_outputs(
   const symbolt &function,
   const exprt::operandst &main_arguments,
   code_blockt &init_code,
-  symbol_tablet &symbol_table)
+  symbol_table_baset &symbol_table)
 {
   const code_typet::parameterst &parameters=
     to_code_type(function.type).parameters();
@@ -319,7 +319,7 @@ void java_record_outputs(
 }
 
 main_function_resultt get_main_symbol(
-  symbol_tablet &symbol_table,
+  const symbol_table_baset &symbol_table,
   const irep_idt &main_class,
   message_handlert &message_handler,
   bool allow_no_body)
@@ -445,7 +445,7 @@ main_function_resultt get_main_symbol(
 ///
 /// \returns true if error occurred on entry point search
 bool java_entry_point(
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   const irep_idt &main_class,
   message_handlert &message_handler,
   bool assume_init_pointers_not_null,
@@ -500,7 +500,7 @@ bool java_entry_point(
 /// \returns true if error occurred on entry point search, false otherwise
 bool generate_java_start_function(
   const symbolt &symbol,
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   message_handlert &message_handler,
   bool assume_init_pointers_not_null,
   const object_factory_parameterst& object_factory_parameters,
diff --git a/src/java_bytecode/java_entry_point.h b/src/java_bytecode/java_entry_point.h
index 2b644924858..8a21df6d389 100644
--- a/src/java_bytecode/java_entry_point.h
+++ b/src/java_bytecode/java_entry_point.h
@@ -19,7 +19,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #define JAVA_ENTRY_POINT_EXCEPTION_SYMBOL "uncaught_exception'"
 
 bool java_entry_point(
-  class symbol_tablet &symbol_table,
+  class symbol_table_baset &symbol_table,
   const irep_idt &main_class,
   class message_handlert &message_handler,
   bool assume_init_pointers_not_null,
@@ -61,14 +61,14 @@ struct main_function_resultt
 
 /// Figures out the entry point of the code to verify
 main_function_resultt get_main_symbol(
-  symbol_tablet &symbol_table,
+  const symbol_table_baset &symbol_table,
   const irep_idt &main_class,
   message_handlert &,
-  bool allow_no_body=false);
+  bool allow_no_body = false);
 
 bool generate_java_start_function(
   const symbolt &symbol,
-  class symbol_tablet &symbol_table,
+  class symbol_table_baset &symbol_table,
   class message_handlert &message_handler,
   bool assume_init_pointers_not_null,
   const object_factory_parameterst& object_factory_parameters,
diff --git a/src/java_bytecode/java_object_factory.cpp b/src/java_bytecode/java_object_factory.cpp
index 910c9e29692..19e944a3ca3 100644
--- a/src/java_bytecode/java_object_factory.cpp
+++ b/src/java_bytecode/java_object_factory.cpp
@@ -35,10 +35,10 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "java_root_class.h"
 
 static symbolt &new_tmp_symbol(
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   const source_locationt &loc,
   const typet &type,
-  const std::string &prefix="tmp_object_factory")
+  const std::string &prefix = "tmp_object_factory")
 {
   return get_fresh_aux_symbol(
     type,
@@ -69,7 +69,7 @@ class java_object_factoryt
   std::unordered_set<irep_idt, irep_id_hash> recursion_set;
 
   /// The symbol table.
-  symbol_tablet &symbol_table;
+  symbol_table_baset &symbol_table;
 
   /// A namespace built from exclusively one symbol table - the one above.
   namespacet ns;
@@ -102,9 +102,9 @@ class java_object_factoryt
     std::vector<const symbolt *> &_symbols_created,
     const source_locationt &loc,
     const object_factory_parameterst _object_factory_parameters,
-    symbol_tablet &_symbol_table,
-    const select_pointer_typet &pointer_type_selector):
-      symbols_created(_symbols_created),
+    symbol_table_baset &_symbol_table,
+    const select_pointer_typet &pointer_type_selector)
+    : symbols_created(_symbols_created),
       loc(loc),
       object_factory_parameters(_object_factory_parameters),
       symbol_table(_symbol_table),
@@ -182,7 +182,7 @@ class java_object_factoryt
 exprt allocate_dynamic_object(
   const exprt &target_expr,
   const typet &allocate_type,
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   const source_locationt &loc,
   code_blockt &output_code,
   std::vector<const symbolt *> &symbols_created,
@@ -241,7 +241,7 @@ exprt allocate_dynamic_object(
 /// \param output_code: code block to which the necessary code is added
 void allocate_dynamic_object_with_decl(
   const exprt &target_expr,
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   const source_locationt &loc,
   code_blockt &output_code)
 {
@@ -543,7 +543,7 @@ codet initialize_nondet_string_struct(
   const exprt &obj,
   const std::size_t &max_nondet_string_length,
   const source_locationt &loc,
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   bool printable)
 {
   PRECONDITION(
@@ -636,7 +636,7 @@ static bool add_nondet_string_pointer_initialization(
   const exprt &expr,
   const std::size_t &max_nondet_string_length,
   bool printable,
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   const source_locationt &loc,
   code_blockt &code)
 {
@@ -1361,7 +1361,7 @@ exprt object_factory(
   const irep_idt base_name,
   code_blockt &init_code,
   bool allow_null,
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   const object_factory_parameterst &parameters,
   allocation_typet alloc_type,
   const source_locationt &loc,
@@ -1457,7 +1457,7 @@ exprt object_factory(
 void gen_nondet_init(
   const exprt &expr,
   code_blockt &init_code,
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   const source_locationt &loc,
   bool skip_classid,
   allocation_typet alloc_type,
@@ -1521,7 +1521,7 @@ exprt object_factory(
 void gen_nondet_init(
   const exprt &expr,
   code_blockt &init_code,
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   const source_locationt &loc,
   bool skip_classid,
   allocation_typet alloc_type,
diff --git a/src/java_bytecode/java_object_factory.h b/src/java_bytecode/java_object_factory.h
index c6aeac7d3d3..7262f7dc652 100644
--- a/src/java_bytecode/java_object_factory.h
+++ b/src/java_bytecode/java_object_factory.h
@@ -91,7 +91,7 @@ exprt object_factory(
   const irep_idt base_name,
   code_blockt &init_code,
   bool allow_null,
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   const object_factory_parameterst &parameters,
   allocation_typet alloc_type,
   const source_locationt &location,
@@ -117,7 +117,7 @@ enum class update_in_placet
 void gen_nondet_init(
   const exprt &expr,
   code_blockt &init_code,
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   const source_locationt &loc,
   bool skip_classid,
   allocation_typet alloc_type,
@@ -129,7 +129,7 @@ void gen_nondet_init(
 void gen_nondet_init(
   const exprt &expr,
   code_blockt &init_code,
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   const source_locationt &loc,
   bool skip_classid,
   allocation_typet alloc_type,
@@ -140,15 +140,15 @@ void gen_nondet_init(
 exprt allocate_dynamic_object(
   const exprt &target_expr,
   const typet &allocate_type,
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   const source_locationt &loc,
   code_blockt &output_code,
   std::vector<const symbolt *> &symbols_created,
-  bool cast_needed=false);
+  bool cast_needed = false);
 
 void allocate_dynamic_object_with_decl(
   const exprt &target_expr,
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   const source_locationt &loc,
   code_blockt &output_code);
 
@@ -156,7 +156,7 @@ codet initialize_nondet_string_struct(
   const exprt &obj,
   const std::size_t &max_nondet_string_length,
   const source_locationt &loc,
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   bool printable);
 
 #endif // CPROVER_JAVA_BYTECODE_JAVA_OBJECT_FACTORY_H
diff --git a/src/java_bytecode/java_string_library_preprocess.cpp b/src/java_bytecode/java_string_library_preprocess.cpp
index 9135480da20..6c040a5a759 100644
--- a/src/java_bytecode/java_string_library_preprocess.cpp
+++ b/src/java_bytecode/java_string_library_preprocess.cpp
@@ -258,7 +258,7 @@ symbol_exprt java_string_library_preprocesst::fresh_array(
 exprt::operandst java_string_library_preprocesst::process_parameters(
   const code_typet::parameterst &params,
   const source_locationt &loc,
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   code_blockt &init_code)
 {
   exprt::operandst ops;
@@ -288,7 +288,7 @@ refined_string_exprt
 java_string_library_preprocesst::convert_exprt_to_string_exprt(
   const exprt &expr_to_process,
   const source_locationt &loc,
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   code_blockt &init_code)
 {
   PRECONDITION(implements_java_char_sequence_pointer(expr_to_process.type()));
@@ -313,7 +313,7 @@ java_string_library_preprocesst::convert_exprt_to_string_exprt(
 exprt::operandst java_string_library_preprocesst::process_operands(
   const exprt::operandst &operands,
   const source_locationt &loc,
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   code_blockt &init_code)
 {
   exprt::operandst ops;
@@ -340,10 +340,10 @@ exprt::operandst java_string_library_preprocesst::process_operands(
 ///   added
 /// \return a list of expressions
 exprt::operandst
-  java_string_library_preprocesst::process_equals_function_operands(
+java_string_library_preprocesst::process_equals_function_operands(
   const exprt::operandst &operands,
   const source_locationt &loc,
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   code_blockt &init_code)
 {
   PRECONDITION(operands.size()==2);
@@ -430,7 +430,7 @@ static exprt get_data(const exprt &expr, const symbol_tablet &symbol_table)
 refined_string_exprt java_string_library_preprocesst::replace_char_array(
   const exprt &array_pointer,
   const source_locationt &loc,
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   code_blockt &code)
 {
   // array is *array_pointer
@@ -464,7 +464,9 @@ refined_string_exprt java_string_library_preprocesst::replace_char_array(
 /// \param symbol_table: symbol table
 /// \return a new symbol
 symbol_exprt java_string_library_preprocesst::fresh_string(
-  const typet &type, const source_locationt &loc, symbol_tablet &symbol_table)
+  const typet &type,
+  const source_locationt &loc,
+  symbol_table_baset &symbol_table)
 {
   symbolt string_symbol=get_fresh_aux_symbol(
     type, "cprover_string", "cprover_string", loc, ID_java, symbol_table);
@@ -480,7 +482,7 @@ symbol_exprt java_string_library_preprocesst::fresh_string(
 /// \return refined string expr with fresh content and length symbols
 refined_string_exprt java_string_library_preprocesst::decl_string_expr(
   const source_locationt &loc,
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   code_blockt &code)
 {
   symbolt sym_length = get_fresh_aux_symbol(
@@ -514,7 +516,7 @@ refined_string_exprt java_string_library_preprocesst::decl_string_expr(
 /// \return a new string_expr
 refined_string_exprt java_string_library_preprocesst::make_nondet_string_expr(
   const source_locationt &loc,
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   code_blockt &code)
 {
   const refined_string_exprt str = decl_string_expr(loc, symbol_table, code);
@@ -548,7 +550,7 @@ refined_string_exprt java_string_library_preprocesst::make_nondet_string_expr(
 exprt java_string_library_preprocesst::allocate_fresh_string(
   const typet &type,
   const source_locationt &loc,
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   code_blockt &code)
 {
   exprt str=fresh_string(type, loc, symbol_table);
@@ -587,7 +589,7 @@ static codet code_assign_function_application(
   const exprt &lhs,
   const irep_idt &function_name,
   const exprt::operandst &arguments,
-  symbol_tablet &symbol_table)
+  symbol_table_baset &symbol_table)
 {
   exprt fun_app=make_function_application(
     function_name, arguments, lhs.type(), symbol_table);
@@ -607,7 +609,7 @@ codet java_string_library_preprocesst::code_return_function_application(
   const irep_idt &function_name,
   const exprt::operandst &arguments,
   const typet &type,
-  symbol_tablet &symbol_table)
+  symbol_table_baset &symbol_table)
 {
   exprt fun_app=make_function_application(
     function_name, arguments, type, symbol_table);
@@ -620,7 +622,7 @@ codet java_string_library_preprocesst::code_return_function_application(
 /// \param code [out] : code block where the declaration gets added
 /// \return created symbol expression
 exprt make_nondet_infinite_char_array(
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   const source_locationt &loc,
   code_blockt &code)
 {
@@ -650,7 +652,7 @@ exprt make_nondet_infinite_char_array(
 void add_pointer_to_array_association(
   const exprt &pointer,
   const exprt &array,
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   const source_locationt &loc,
   code_blockt &code)
 {
@@ -683,7 +685,7 @@ void add_pointer_to_array_association(
 void add_array_to_length_association(
   const exprt &array,
   const exprt &length,
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   const source_locationt &loc,
   code_blockt &code)
 {
@@ -718,7 +720,7 @@ void add_character_set_constraint(
   const exprt &pointer,
   const exprt &length,
   const irep_idt &char_set,
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   const source_locationt &loc,
   code_blockt &code)
 {
@@ -756,7 +758,7 @@ refined_string_exprt java_string_library_preprocesst::string_expr_of_function(
   const irep_idt &function_name,
   const exprt::operandst &arguments,
   const source_locationt &loc,
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   code_blockt &code)
 {
   // int return_code;
@@ -800,7 +802,7 @@ codet java_string_library_preprocesst::code_assign_components_to_java_string(
   const exprt &lhs,
   const exprt &rhs_array,
   const exprt &rhs_length,
-  symbol_tablet &symbol_table)
+  const symbol_table_baset &symbol_table)
 {
   PRECONDITION(implements_java_char_sequence_pointer(lhs.type()));
   dereference_exprt deref=checked_dereference(lhs, lhs.type().subtype());
@@ -831,7 +833,7 @@ codet java_string_library_preprocesst::code_assign_components_to_java_string(
 codet java_string_library_preprocesst::code_assign_string_expr_to_java_string(
   const exprt &lhs,
   const refined_string_exprt &rhs,
-  symbol_tablet &symbol_table)
+  const symbol_table_baset &symbol_table)
 {
   return code_assign_components_to_java_string(
     lhs, rhs.content(), rhs.length(), symbol_table);
@@ -850,7 +852,7 @@ void java_string_library_preprocesst::code_assign_java_string_to_string_expr(
   const refined_string_exprt &lhs,
   const exprt &rhs,
   const source_locationt &loc,
-  symbol_tablet &symbol_table,
+  const symbol_table_baset &symbol_table,
   code_blockt &code)
 {
   PRECONDITION(implements_java_char_sequence_pointer(rhs.type()));
@@ -887,7 +889,7 @@ refined_string_exprt
 java_string_library_preprocesst::string_literal_to_string_expr(
   const std::string &s,
   const source_locationt &loc,
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   code_blockt &code)
 {
   const constant_exprt expr(s, string_typet());
@@ -908,7 +910,7 @@ java_string_library_preprocesst::string_literal_to_string_expr(
 codet java_string_library_preprocesst::make_equals_function_code(
   const code_typet &type,
   const source_locationt &loc,
-  symbol_tablet &symbol_table)
+  symbol_table_baset &symbol_table)
 {
   // TODO: Code should return false if Object is not String.
   code_blockt code;
@@ -933,7 +935,7 @@ codet java_string_library_preprocesst::make_equals_function_code(
 codet java_string_library_preprocesst::make_float_to_string_code(
   const code_typet &type,
   const source_locationt &loc,
-  symbol_tablet &symbol_table)
+  symbol_table_baset &symbol_table)
 {
   // Getting the argument
   code_typet::parameterst params=type.parameters();
@@ -1075,7 +1077,7 @@ codet java_string_library_preprocesst::make_init_function_from_call(
   const irep_idt &function_name,
   const code_typet &type,
   const source_locationt &loc,
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   bool ignore_first_arg)
 {
   code_typet::parameterst params=type.parameters();
@@ -1116,7 +1118,7 @@ codet java_string_library_preprocesst::
     const irep_idt &function_name,
     const code_typet &type,
     const source_locationt &loc,
-    symbol_tablet &symbol_table)
+    symbol_table_baset &symbol_table)
 {
   // This is similar to assign functions except we return a pointer to `this`
   code_typet::parameterst params=type.parameters();
@@ -1137,10 +1139,10 @@ codet java_string_library_preprocesst::
 /// \return Code assigning result of a call to the function with given function
 ///   name.
 codet java_string_library_preprocesst::make_assign_function_from_call(
-    const irep_idt &function_name,
-    const code_typet &type,
-    const source_locationt &loc,
-    symbol_tablet &symbol_table)
+  const irep_idt &function_name,
+  const code_typet &type,
+  const source_locationt &loc,
+  symbol_table_baset &symbol_table)
 {
   // This is similar to initialization function except we do not ignore
   // the first argument
@@ -1172,7 +1174,7 @@ exprt java_string_library_preprocesst::get_primitive_value_of_object(
   const exprt &object,
   irep_idt type_name,
   const source_locationt &loc,
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   code_blockt &code)
 {
   symbol_typet object_type;
@@ -1314,7 +1316,7 @@ exprt java_string_library_preprocesst::make_argument_for_format(
   int index,
   const struct_typet &structured_type,
   const source_locationt &loc,
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   code_blockt &code)
 {
   // Declarations of the fields of arg_i_struct
@@ -1406,7 +1408,7 @@ exprt java_string_library_preprocesst::make_argument_for_format(
 codet java_string_library_preprocesst::make_string_format_code(
   const code_typet &type,
   const source_locationt &loc,
-  symbol_tablet &symbol_table)
+  symbol_table_baset &symbol_table)
 {
   PRECONDITION(type.parameters().size()==2);
   code_blockt code;
@@ -1460,9 +1462,9 @@ codet java_string_library_preprocesst::make_string_format_code(
 /// return class1
 /// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 codet java_string_library_preprocesst::make_object_get_class_code(
-    const code_typet &type,
-    const source_locationt &loc,
-    symbol_tablet &symbol_table)
+  const code_typet &type,
+  const source_locationt &loc,
+  symbol_table_baset &symbol_table)
 {
   code_typet::parameterst params=type.parameters();
   exprt this_obj=symbol_exprt(params[0].get_identifier(), params[0].type());
@@ -1540,7 +1542,7 @@ codet java_string_library_preprocesst::make_function_from_call(
   const irep_idt &function_name,
   const code_typet &type,
   const source_locationt &loc,
-  symbol_tablet &symbol_table)
+  symbol_table_baset &symbol_table)
 {
   code_blockt code;
   exprt::operandst args=process_parameters(
@@ -1563,12 +1565,11 @@ codet java_string_library_preprocesst::make_function_from_call(
 /// string = string_expr_to_string(string)
 /// return string
 /// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-codet java_string_library_preprocesst::
-  make_string_returning_function_from_call(
-    const irep_idt &function_name,
-    const code_typet &type,
-    const source_locationt &loc,
-    symbol_tablet &symbol_table)
+codet java_string_library_preprocesst::make_string_returning_function_from_call(
+  const irep_idt &function_name,
+  const code_typet &type,
+  const source_locationt &loc,
+  symbol_table_baset &symbol_table)
 {
   // Code for the output
   code_blockt code;
@@ -1607,7 +1608,7 @@ codet java_string_library_preprocesst::
 codet java_string_library_preprocesst::make_copy_string_code(
   const code_typet &type,
   const source_locationt &loc,
-  symbol_tablet &symbol_table)
+  symbol_table_baset &symbol_table)
 {
   // Code for the output
   code_blockt code;
@@ -1645,7 +1646,7 @@ codet java_string_library_preprocesst::make_copy_string_code(
 codet java_string_library_preprocesst::make_copy_constructor_code(
   const code_typet &type,
   const source_locationt &loc,
-  symbol_tablet &symbol_table)
+  symbol_table_baset &symbol_table)
 {
   // Code for the output
   code_blockt code;
@@ -1679,7 +1680,7 @@ codet java_string_library_preprocesst::make_copy_constructor_code(
 codet java_string_library_preprocesst::make_init_from_array_code(
   const code_typet &type,
   const source_locationt &loc,
-  symbol_tablet &symbol_table)
+  symbol_table_baset &symbol_table)
 {
   // Code for the output
   code_blockt code;
@@ -1734,7 +1735,7 @@ codet java_string_library_preprocesst::make_init_from_array_code(
 codet java_string_library_preprocesst::make_string_length_code(
   const code_typet &type,
   const source_locationt &loc,
-  symbol_tablet &symbol_table)
+  symbol_table_baset &symbol_table)
 {
   code_typet::parameterst params=type.parameters();
   symbol_exprt arg_this(params[0].get_identifier(), params[0].type());
@@ -1755,7 +1756,7 @@ exprt java_string_library_preprocesst::code_for_function(
   const irep_idt &function_id,
   const code_typet &type,
   const source_locationt &loc,
-  symbol_tablet &symbol_table)
+  symbol_table_baset &symbol_table)
 {
   auto it_id=cprover_equivalent_to_java_function.find(function_id);
   if(it_id!=cprover_equivalent_to_java_function.end())
diff --git a/src/java_bytecode/java_string_library_preprocess.h b/src/java_bytecode/java_string_library_preprocess.h
index d9915655fd4..ef9c7a5e3cf 100644
--- a/src/java_bytecode/java_string_library_preprocess.h
+++ b/src/java_bytecode/java_string_library_preprocess.h
@@ -47,7 +47,7 @@ class java_string_library_preprocesst:public messaget
     const irep_idt &function_id,
     const code_typet &type,
     const source_locationt &loc,
-    symbol_tablet &symbol_table);
+    symbol_table_baset &symbol_table);
 
   codet replace_character_call(code_function_callt call)
   {
@@ -94,9 +94,8 @@ class java_string_library_preprocesst:public messaget
   const typet index_type;
   const refined_string_typet refined_string_type;
 
-  typedef
-    std::function<codet(
-      const code_typet &, const source_locationt &, symbol_tablet &)>
+  typedef std::function<
+    codet(const code_typet &, const source_locationt &, symbol_table_baset &)>
     conversion_functiont;
 
   typedef std::unordered_map<irep_idt, irep_idt, irep_id_hash> id_mapt;
@@ -132,12 +131,12 @@ class java_string_library_preprocesst:public messaget
   codet make_equals_function_code(
     const code_typet &type,
     const source_locationt &loc,
-    symbol_tablet &symbol_table);
+    symbol_table_baset &symbol_table);
 
   codet make_float_to_string_code(
     const code_typet &type,
     const source_locationt &loc,
-    symbol_tablet &symbol_table);
+    symbol_table_baset &symbol_table);
 
   codet make_string_to_char_array_code(
     const code_typet &type,
@@ -147,33 +146,33 @@ class java_string_library_preprocesst:public messaget
   codet make_string_format_code(
     const code_typet &type,
     const source_locationt &loc,
-    symbol_tablet &symbol_table);
+    symbol_table_baset &symbol_table);
 
   codet make_copy_string_code(
     const code_typet &type,
     const source_locationt &loc,
-    symbol_tablet &symbol_table);
+    symbol_table_baset &symbol_table);
 
   codet make_copy_constructor_code(
     const code_typet &type,
     const source_locationt &loc,
-    symbol_tablet &symbol_table);
+    symbol_table_baset &symbol_table);
 
   codet make_string_length_code(
     const code_typet &type,
     const source_locationt &loc,
-    symbol_tablet &symbol_table);
+    symbol_table_baset &symbol_table);
 
   codet make_object_get_class_code(
     const code_typet &type,
     const source_locationt &loc,
-    symbol_tablet &symbol_table);
+    symbol_table_baset &symbol_table);
 
   // Helper functions
   exprt::operandst process_parameters(
     const code_typet::parameterst &params,
     const source_locationt &loc,
-    symbol_tablet &symbol_table,
+    symbol_table_baset &symbol_table,
     code_blockt &init_code);
 
   // Friending this function for unit testing convert_exprt_to_string_exprt
@@ -187,31 +186,31 @@ class java_string_library_preprocesst:public messaget
   refined_string_exprt convert_exprt_to_string_exprt(
     const exprt &deref,
     const source_locationt &loc,
-    symbol_tablet &symbol_table,
+    symbol_table_baset &symbol_table,
     code_blockt &init_code);
 
   exprt::operandst process_operands(
     const exprt::operandst &operands,
     const source_locationt &loc,
-    symbol_tablet &symbol_table,
+    symbol_table_baset &symbol_table,
     code_blockt &init_code);
 
   exprt::operandst process_equals_function_operands(
     const exprt::operandst &operands,
     const source_locationt &loc,
-    symbol_tablet &symbol_table,
+    symbol_table_baset &symbol_table,
     code_blockt &init_code);
 
   refined_string_exprt replace_char_array(
     const exprt &array_pointer,
     const source_locationt &loc,
-    symbol_tablet &symbol_table,
+    symbol_table_baset &symbol_table,
     code_blockt &code);
 
   symbol_exprt fresh_string(
     const typet &type,
     const source_locationt &loc,
-    symbol_tablet &symbol_table);
+    symbol_table_baset &symbol_table);
 
   symbol_exprt fresh_array(
     const typet &type,
@@ -220,18 +219,18 @@ class java_string_library_preprocesst:public messaget
 
   refined_string_exprt decl_string_expr(
     const source_locationt &loc,
-    symbol_tablet &symbol_table,
+    symbol_table_baset &symbol_table,
     code_blockt &code);
 
   refined_string_exprt make_nondet_string_expr(
     const source_locationt &loc,
-    symbol_tablet &symbol_table,
+    symbol_table_baset &symbol_table,
     code_blockt &code);
 
   exprt allocate_fresh_string(
     const typet &type,
     const source_locationt &loc,
-    symbol_tablet &symbol_table,
+    symbol_table_baset &symbol_table,
     code_blockt &code);
 
   exprt allocate_fresh_array(
@@ -244,82 +243,83 @@ class java_string_library_preprocesst:public messaget
     const irep_idt &function_name,
     const exprt::operandst &arguments,
     const typet &type,
-    symbol_tablet &symbol_table);
+    symbol_table_baset &symbol_table);
 
   refined_string_exprt string_expr_of_function(
     const irep_idt &function_name,
     const exprt::operandst &arguments,
     const source_locationt &loc,
-    symbol_tablet &symbol_table,
+    symbol_table_baset &symbol_table,
     code_blockt &code);
 
   codet code_assign_components_to_java_string(
     const exprt &lhs,
     const exprt &rhs_array,
     const exprt &rhs_length,
-    symbol_tablet &symbol_table);
+    const symbol_table_baset &symbol_table);
 
   codet code_assign_string_expr_to_java_string(
     const exprt &lhs,
     const refined_string_exprt &rhs,
-    symbol_tablet &symbol_table);
+    const symbol_table_baset &symbol_table);
 
   void code_assign_java_string_to_string_expr(
     const refined_string_exprt &lhs,
     const exprt &rhs,
     const source_locationt &loc,
-    symbol_tablet &symbol_table,
+    const symbol_table_baset &symbol_table,
     code_blockt &code);
 
   refined_string_exprt string_literal_to_string_expr(
     const std::string &s,
     const source_locationt &loc,
-    symbol_tablet &symbol_table,
+    symbol_table_baset &symbol_table,
     code_blockt &code);
 
   codet make_function_from_call(
     const irep_idt &function_name,
     const code_typet &type,
     const source_locationt &loc,
-    symbol_tablet &symbol_table);
+    symbol_table_baset &symbol_table);
 
   codet make_init_function_from_call(
     const irep_idt &function_name,
     const code_typet &type,
     const source_locationt &loc,
-    symbol_tablet &symbol_table,
-    bool ignore_first_arg=true);
+    symbol_table_baset &symbol_table,
+    bool ignore_first_arg = true);
 
   codet make_assign_and_return_function_from_call(
     const irep_idt &function_name,
     const code_typet &type,
     const source_locationt &loc,
-    symbol_tablet &symbol_table);
+    symbol_table_baset &symbol_table);
 
   codet make_assign_function_from_call(
     const irep_idt &function_name,
     const code_typet &type,
     const source_locationt &loc,
-    symbol_tablet &symbol_table);
+    symbol_table_baset &symbol_table);
 
   codet make_string_returning_function_from_call(
     const irep_idt &function_name,
     const code_typet &type,
     const source_locationt &loc,
-    symbol_tablet &symbol_table);
+    symbol_table_baset &symbol_table);
 
-  exprt make_argument_for_format(const exprt &argv,
+  exprt make_argument_for_format(
+    const exprt &argv,
     int index,
     const struct_typet &structured_type,
     const source_locationt &loc,
-    symbol_tablet &symbol_table,
+    symbol_table_baset &symbol_table,
     code_blockt &code);
 
   exprt get_primitive_value_of_object(
     const exprt &object,
     irep_idt type_name,
     const source_locationt &loc,
-    symbol_tablet &symbol_table,
+    symbol_table_baset &symbol_table,
     code_blockt &code);
 
   exprt get_object_at_index(const exprt &argv, int index);
@@ -327,25 +327,25 @@ class java_string_library_preprocesst:public messaget
   codet make_init_from_array_code(
     const code_typet &type,
     const source_locationt &loc,
-    symbol_tablet &symbol_table);
+    symbol_table_baset &symbol_table);
 };
 
 exprt make_nondet_infinite_char_array(
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   const source_locationt &loc,
   code_blockt &code);
 
 void add_pointer_to_array_association(
   const exprt &pointer,
   const exprt &array,
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   const source_locationt &loc,
   code_blockt &code);
 
 void add_array_to_length_association(
   const exprt &array,
   const exprt &length,
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   const source_locationt &loc,
   code_blockt &code);
 
@@ -353,7 +353,7 @@ void add_character_set_constraint(
   const exprt &pointer,
   const exprt &length,
   const irep_idt &char_set,
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   const source_locationt &loc,
   code_blockt &code);
 
diff --git a/src/java_bytecode/java_utils.cpp b/src/java_bytecode/java_utils.cpp
index e244247ca42..aba810677ce 100644
--- a/src/java_bytecode/java_utils.cpp
+++ b/src/java_bytecode/java_utils.cpp
@@ -64,7 +64,7 @@ const std::string java_class_to_package(const std::string &canonical_classname)
 
 void generate_class_stub(
   const irep_idt &class_name,
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   message_handlert &message_handler,
   const struct_union_typet::componentst &componentst)
 {
@@ -119,7 +119,7 @@ bool is_java_string_literal_id(const irep_idt &id)
 
 irep_idt resolve_friendly_method_name(
   const std::string &friendly_name,
-  const symbol_tablet &symbol_table,
+  const symbol_table_baset &symbol_table,
   std::string &error)
 {
   std::string qualified_name="java::"+friendly_name;
@@ -257,7 +257,7 @@ void java_add_components_to_class(
 void declare_function(
   irep_idt function_name,
   const typet &type,
-  symbol_tablet &symbol_table)
+  symbol_table_baset &symbol_table)
 {
   auxiliary_symbolt func_symbol;
   func_symbol.base_name=function_name;
@@ -280,7 +280,7 @@ exprt make_function_application(
   const irep_idt &function_name,
   const exprt::operandst &arguments,
   const typet &type,
-  symbol_tablet &symbol_table)
+  symbol_table_baset &symbol_table)
 {
   // Names of function to call
   std::string fun_name=id2string(function_name);
diff --git a/src/java_bytecode/java_utils.h b/src/java_bytecode/java_utils.h
index 1ed4cdcbb3d..f45df9ef62c 100644
--- a/src/java_bytecode/java_utils.h
+++ b/src/java_bytecode/java_utils.h
@@ -17,7 +17,7 @@ bool java_is_array_type(const typet &type);
 
 void generate_class_stub(
   const irep_idt &class_name,
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   message_handlert &message_handler,
   const struct_union_typet::componentst &componentst);
 
@@ -59,7 +59,7 @@ bool is_java_string_literal_id(const irep_idt &id);
 /// \param [out] error: gets error description on failure
 irep_idt resolve_friendly_method_name(
   const std::string &friendly_name,
-  const symbol_tablet &symbol_table,
+  const symbol_table_baset &symbol_table,
   std::string &error);
 
 /// Dereference an expression and flag it for a null-pointer check
@@ -84,12 +84,12 @@ size_t find_closing_delimiter(
 void declare_function(
   irep_idt function_name,
   const typet &type,
-  symbol_tablet &symbol_table);
+  symbol_table_baset &symbol_table);
 
 exprt make_function_application(
   const irep_idt &function_name,
   const exprt::operandst &arguments,
   const typet &type,
-  symbol_tablet &symbol_table);
+  symbol_table_baset &symbol_table);
 
 #endif // CPROVER_JAVA_BYTECODE_JAVA_UTILS_H
diff --git a/src/util/Makefile b/src/util/Makefile
index c51cd7e752a..4592c896966 100644
--- a/src/util/Makefile
+++ b/src/util/Makefile
@@ -80,6 +80,7 @@ SRC = arith_tools.cpp \
       string_utils.cpp \
       substitute.cpp \
       symbol.cpp \
+      symbol_table_base.cpp \
       symbol_table.cpp \
       tempdir.cpp \
       tempfile.cpp \
diff --git a/src/util/fresh_symbol.cpp b/src/util/fresh_symbol.cpp
index 596fb245440..34cef89a30f 100644
--- a/src/util/fresh_symbol.cpp
+++ b/src/util/fresh_symbol.cpp
@@ -36,7 +36,7 @@ symbolt &get_fresh_aux_symbol(
   const std::string &basename_prefix,
   const source_locationt &source_location,
   const irep_idt &symbol_mode,
-  symbol_tablet &symbol_table)
+  symbol_table_baset &symbol_table)
 {
   // Loop until find a name that doesn't clash with a non-auxilliary symbol
   while(true)
diff --git a/src/util/fresh_symbol.h b/src/util/fresh_symbol.h
index 7e659076f62..18d91164248 100644
--- a/src/util/fresh_symbol.h
+++ b/src/util/fresh_symbol.h
@@ -27,6 +27,6 @@ symbolt &get_fresh_aux_symbol(
   const std::string &basename_prefix,
   const source_locationt &source_location,
   const irep_idt &symbol_mode,
-  symbol_tablet &symbol_table);
+  symbol_table_baset &symbol_table);
 
 #endif // CPROVER_UTIL_FRESH_SYMBOL_H
diff --git a/src/util/journalling_symbol_table.h b/src/util/journalling_symbol_table.h
new file mode 100644
index 00000000000..2258b0ea203
--- /dev/null
+++ b/src/util/journalling_symbol_table.h
@@ -0,0 +1,161 @@
+
+// Copyright 2016-2017 DiffBlue Limited. All Rights Reserved.
+
+/// \file
+/// A symbol table writer that records which entries have been updated
+
+#ifndef CPROVER_UTIL_JOURNALLING_SYMBOL_TABLE_H
+#define CPROVER_UTIL_JOURNALLING_SYMBOL_TABLE_H
+
+#include <utility>
+#include <unordered_set>
+#include "irep.h"
+#include "symbol_table.h"
+
+/// \brief A symbol table wrapper that records which entries have been
+/// updated/removed
+/// \ingroup gr_symbol_table
+/// A caller can pass a `journalling_symbol_tablet` into a callee that is
+/// expected to mutate it somehow, then after it has run inspect the recording
+/// table's journal to determine what has changed more cheaply than examining
+/// every symbol.
+///
+/// Example of usage:
+/// ```
+/// symbol_tablet real_table;
+/// init_table(real_table);
+///
+/// journalling_symbol_tablet journal(actual_table); // Wraps real_table
+/// alter_table(journal);
+
+/// for(const auto &added : journal.added())
+/// {
+///   printf("%s was added\n", added.name);
+/// }
+class journalling_symbol_tablet : public symbol_table_baset
+{
+public:
+  typedef std::unordered_set<irep_idt, irep_id_hash> changesett;
+
+private:
+  symbol_tablet &base_symbol_table;
+  // Symbols originally in the table will never be marked inserted
+  changesett inserted;
+  // get_writeable marks an existing symbol updated
+  // Inserted symbols are marked updated, removed ones aren't
+  changesett updated;
+  // Symbols not originally in the table will never be marked removed
+  changesett removed;
+
+private:
+  explicit journalling_symbol_tablet(symbol_tablet &base_symbol_table)
+    : symbol_table_baset(
+        base_symbol_table.symbols,
+        base_symbol_table.symbol_base_map,
+        base_symbol_table.symbol_module_map),
+      base_symbol_table(base_symbol_table)
+  {
+  }
+
+public:
+  journalling_symbol_tablet(const journalling_symbol_tablet &other) = delete;
+
+  journalling_symbol_tablet(journalling_symbol_tablet &&other)
+    : symbol_table_baset(
+        other.symbols,
+        other.symbol_base_map,
+        other.symbol_module_map),
+      base_symbol_table(other.base_symbol_table),
+      inserted(std::move(other.inserted)),
+      updated(std::move(other.updated)),
+      removed(std::move(other.removed))
+  {
+  }
+
+  virtual const symbol_tablet &get_symbol_table() const override
+  {
+    return base_symbol_table;
+  }
+
+  static journalling_symbol_tablet wrap(symbol_tablet &base_symbol_table)
+  {
+    return journalling_symbol_tablet(base_symbol_table);
+  }
+
+  virtual bool move(symbolt &symbol, symbolt *&new_symbol) override
+  {
+    bool ret = base_symbol_table.move(symbol, new_symbol);
+    if(!ret)
+      on_insert(symbol.name);
+    else
+      on_update(symbol.name);
+    return ret;
+  }
+
+  virtual symbolt *get_writeable(const irep_idt &identifier) override
+  {
+    symbolt *result = base_symbol_table.get_writeable(identifier);
+    if(result)
+      on_update(identifier);
+    return result;
+  }
+
+  virtual std::pair<symbolt &, bool> insert(symbolt symbol) override
+  {
+    std::pair<symbolt &, bool> result =
+      base_symbol_table.insert(std::move(symbol));
+    if(result.second)
+      on_insert(result.first.name);
+    return result;
+  }
+
+  virtual void
+  erase(const symbol_tablet::symbolst::const_iterator &entry) override
+  {
+    const irep_idt entry_name = entry->first;
+    base_symbol_table.erase(entry);
+    on_remove(entry_name);
+  }
+
+  virtual void clear() override
+  {
+    for(const auto &named_symbol : base_symbol_table.symbols)
+      on_remove(named_symbol.first);
+    base_symbol_table.clear();
+  }
+
+  const changesett &get_inserted() const
+  {
+    return inserted;
+  }
+  const changesett &get_updated() const
+  {
+    return updated;
+  }
+  const changesett &get_removed() const
+  {
+    return removed;
+  }
+
+private:
+  void on_insert(const irep_idt &id)
+  {
+    if(removed.erase(id) == 0)
+      inserted.insert(id);
+    updated.insert(id);
+  }
+
+  void on_update(const irep_idt &id)
+  {
+    updated.insert(id);
+  }
+
+  void on_remove(const irep_idt &id)
+  {
+    if(inserted.erase(id) == 0)
+      removed.insert(id);
+    updated.erase(id);
+  }
+};
+
+#endif // CPROVER_UTIL_JOURNALLING_SYMBOL_TABLE_H
diff --git a/src/util/language.cpp b/src/util/language.cpp
index 62f77edc40b..60ea1262646 100644
--- a/src/util/language.cpp
+++ b/src/util/language.cpp
@@ -18,7 +18,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/cprover_prefix.h>
 #include <util/std_types.h>
 
-bool languaget::final(symbol_tablet &symbol_table)
+bool languaget::final(symbol_table_baset &symbol_table)
 {
   return false;
 }
diff --git a/src/util/language.h b/src/util/language.h
index ee3cd40c827..817a522b9c7 100644
--- a/src/util/language.h
+++ b/src/util/language.h
@@ -23,6 +23,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "message.h"
 
 class symbol_tablet;
+class symbol_table_baset;
 class exprt;
 class namespacet;
 class typet;
@@ -84,8 +85,7 @@ class languaget:public messaget
 
   /// Final adjustments, e.g. initializing stub functions and globals that
   /// were discovered during function loading
-  virtual bool final(
-    symbol_tablet &symbol_table);
+  virtual bool final(symbol_table_baset &symbol_table);
 
   // type check interfaces of currently parsed file
 
diff --git a/src/util/language_file.cpp b/src/util/language_file.cpp
index a90fb6f3e9e..5eb6b2c654a 100644
--- a/src/util/language_file.cpp
+++ b/src/util/language_file.cpp
@@ -174,8 +174,7 @@ bool language_filest::generate_support_functions(
   return false;
 }
 
-bool language_filest::final(
-  symbol_tablet &symbol_table)
+bool language_filest::final(symbol_table_baset &symbol_table)
 {
   std::set<std::string> languages;
 
diff --git a/src/util/language_file.h b/src/util/language_file.h
index c00e4155252..19f644b8d44 100644
--- a/src/util/language_file.h
+++ b/src/util/language_file.h
@@ -19,6 +19,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "message.h"
 
 class symbol_tablet;
+class symbol_table_baset;
 class language_filet;
 class languaget;
 
@@ -87,7 +88,7 @@ class language_filest:public messaget
 
   bool typecheck(symbol_tablet &symbol_table);
 
-  bool final(symbol_tablet &symbol_table);
+  bool final(symbol_table_baset &symbol_table);
 
   bool interfaces(symbol_tablet &symbol_table);
 
diff --git a/src/util/symbol_table.cpp b/src/util/symbol_table.cpp
index ed8b67b1bb2..4d26d1de9c9 100644
--- a/src/util/symbol_table.cpp
+++ b/src/util/symbol_table.cpp
@@ -1,19 +1,9 @@
-// Copyright 2016-2017 DiffBlue Limited. All Rights Reserved.
+// Copyright 2016-2017 Diffblue Limited. All Rights Reserved.
 
 #include "symbol_table.h"
 
-#include <ostream>
 #include <util/invariant.h>
 
-/// Add a new symbol to the symbol table
-/// \param symbol: The symbol to be added to the symbol table
-/// \return Returns true if the process failed, which should only happen if
-///   there is a symbol with the same name already in the symbol table.
-bool symbol_tablet::add(const symbolt &symbol)
-{
-  return !insert(symbol).second;
-}
-
 /// Move or copy a new symbol to the symbol table
 /// \remark: This is a nicer interface than move and achieves the same
 /// result as both move and add
@@ -56,7 +46,7 @@ std::pair<symbolt &, bool> symbol_tablet::insert(symbolt symbol)
 /// Move a symbol into the symbol table. If there is already a symbol with the
 /// same name then symbol is unchanged, new_symbol points to the symbol with the
 /// same name and true is returned. Otherwise, the symbol is moved into the
-/// symbol table, symbol is set to be empty, new_symbol points to its new
+/// symbol table, symbol is destroyed, new_symbol points to its new
 /// location in the symbol table and false is returned
 /// \param symbol: The symbol to be added to the symbol table
 /// \param new_symbol: Pointer which the function will set to either point to
@@ -89,19 +79,6 @@ bool symbol_tablet::move(symbolt &symbol, symbolt *&new_symbol)
   return !result.second;
 }
 
-/// Remove a symbol from the symbol table
-/// \param name: The name of the symbol to remove
-/// \return Returns a boolean indicating whether the process failed
-///   i.e. false if the symbol was removed, or true if it didn't exist.
-bool symbol_tablet::remove(const irep_idt &name)
-{
-  symbolst::const_iterator entry=symbols.find(name);
-  if(entry==symbols.end())
-    return true;
-  erase(entry);
-  return false;
-}
-
 /// Remove a symbol from the symbol table
 /// \param entry: an iterator pointing at the symbol to remove
 void symbol_tablet::erase(const symbolst::const_iterator &entry)
@@ -137,22 +114,3 @@ void symbol_tablet::erase(const symbolst::const_iterator &entry)
 
   internal_symbols.erase(entry);
 }
-
-/// Print the contents of the symbol table
-/// \param out: The ostream to direct output to
-void symbol_tablet::show(std::ostream &out) const
-{
-  out << "\n" << "Symbols:" << "\n";
-
-  forall_symbols(it, symbols)
-    out << it->second;
-}
-
-/// Print the contents of the symbol table
-/// \param out: The ostream to direct output to
-/// \param symbol_table: The symbol table to print out
-std::ostream &operator << (std::ostream &out, const symbol_tablet &symbol_table)
-{
-  symbol_table.show(out);
-  return out;
-}
diff --git a/src/util/symbol_table.h b/src/util/symbol_table.h
index 42893a0882d..a9a083f5f4e 100644
--- a/src/util/symbol_table.h
+++ b/src/util/symbol_table.h
@@ -1,29 +1,17 @@
-// Copyright 2016-2017 DiffBlue Limited. All Rights Reserved.
+// Copyright 2016-2017 Diffblue Limited. All Rights Reserved.
 
 /// \file
 /// Symbol table
 
-/// \defgroup gr_symbol_table Symbol Table
-
 #ifndef CPROVER_UTIL_SYMBOL_TABLE_H
 #define CPROVER_UTIL_SYMBOL_TABLE_H
 
-#include <iosfwd>
-#include <map>
-#include <unordered_map>
-
-#include <util/optional.h>
-
-#include "symbol.h"
-
+#include "symbol_table_base.h"
 
 #define forall_symbols(it, expr) \
   for(symbol_tablet::symbolst::const_iterator it=(expr).begin(); \
       it!=(expr).end(); ++it)
 
-typedef std::multimap<irep_idt, irep_idt> symbol_base_mapt;
-typedef std::multimap<irep_idt, irep_idt> symbol_module_mapt;
-
 #define forall_symbol_base_map(it, expr, base_name) \
   for(symbol_base_mapt::const_iterator it=(expr).lower_bound(base_name), \
                                        it_end=(expr).upper_bound(base_name); \
@@ -37,35 +25,30 @@ typedef std::multimap<irep_idt, irep_idt> symbol_module_mapt;
 
 /// \brief The symbol table
 /// \ingroup gr_symbol_table
-class symbol_tablet
+class symbol_tablet : public symbol_table_baset
 {
-public:
-  typedef std::unordered_map<irep_idt, symbolt, irep_id_hash> symbolst;
-
 private:
   symbolst internal_symbols;
   symbol_base_mapt internal_symbol_base_map;
   symbol_module_mapt internal_symbol_module_map;
 
 public:
-  const symbolst &symbols;
-  const symbol_base_mapt &symbol_base_map;
-  const symbol_module_mapt &symbol_module_map;
-
   symbol_tablet()
-    : symbols(internal_symbols),
-      symbol_base_map(internal_symbol_base_map),
-      symbol_module_map(internal_symbol_module_map)
+    : symbol_table_baset(
+        internal_symbols,
+        internal_symbol_base_map,
+        internal_symbol_module_map)
   {
   }
 
   symbol_tablet(const symbol_tablet &other)
-    : internal_symbols(other.internal_symbols),
+    : symbol_table_baset(
+        internal_symbols,
+        internal_symbol_base_map,
+        internal_symbol_module_map),
+      internal_symbols(other.internal_symbols),
       internal_symbol_base_map(other.internal_symbol_base_map),
-      internal_symbol_module_map(other.symbol_module_map),
-      symbols(internal_symbols),
-      symbol_base_map(internal_symbol_base_map),
-      symbol_module_map(internal_symbol_module_map)
+      internal_symbol_module_map(other.internal_symbol_module_map)
   {
   }
 
@@ -76,96 +59,56 @@ class symbol_tablet
   }
 
   symbol_tablet(symbol_tablet &&other)
-    : internal_symbols(std::move(other.internal_symbols)),
+    : symbol_table_baset(
+        internal_symbols,
+        internal_symbol_base_map,
+        internal_symbol_module_map),
+      internal_symbols(std::move(other.internal_symbols)),
       internal_symbol_base_map(std::move(other.internal_symbol_base_map)),
-      internal_symbol_module_map(std::move(other.symbol_module_map)),
-      symbols(internal_symbols),
-      symbol_base_map(internal_symbol_base_map),
-      symbol_module_map(internal_symbol_module_map)
+      internal_symbol_module_map(std::move(other.internal_symbol_module_map))
   {
   }
 
   symbol_tablet &operator=(symbol_tablet &&other)
   {
-    internal_symbols=std::move(other.internal_symbols);
-    internal_symbol_base_map=std::move(other.internal_symbol_base_map);
-    internal_symbol_module_map=std::move(other.symbol_module_map);
+    internal_symbols = std::move(other.internal_symbols);
+    internal_symbol_base_map = std::move(other.internal_symbol_base_map);
+    internal_symbol_module_map = std::move(other.internal_symbol_module_map);
     return *this;
   }
 
-  bool has_symbol(const irep_idt &name) const
+  void swap(symbol_tablet &other)
   {
-    return symbols.find(name)!=symbols.end();
+    internal_symbols.swap(other.internal_symbols);
+    internal_symbol_base_map.swap(other.internal_symbol_base_map);
+    internal_symbol_module_map.swap(other.internal_symbol_module_map);
   }
 
-  /// Find a symbol in the symbol table for read-only access.
-  /// \param id: The name of the symbol to look for
-  /// \return an optional reference, set if found, nullptr otherwise.
-  const symbolt *lookup(const irep_idt &id) const { return lookup_impl(id); }
-
-  /// Find a symbol in the symbol table for read-write access.
-  /// \param id: The name of the symbol to look for
-  /// \return an optional reference, set if found, unset otherwise.
-  symbolt *get_writeable(const irep_idt &id) { return lookup_impl(id); }
-
-  /// Find a symbol in the symbol table for read-only access.
-  /// \param id: The name of the symbol to look for
-  /// \return A reference to the symbol
-  /// \throw `std::out_of_range` if no such symbol exists
-  const symbolt &lookup_ref(const irep_idt &id) const
-    { return internal_symbols.at(id); }
-
-  /// Find a symbol in the symbol table for read-write access.
-  /// \param id: The name of the symbol to look for
-  /// \return A reference to the symbol
-  /// \throw `std::out_of_range` if no such symbol exists
-  symbolt &get_writeable_ref(const irep_idt &id)
-    { return internal_symbols.at(id); }
-
-  bool add(const symbolt &symbol);
-
-  std::pair<symbolt &, bool> insert(symbolt symbol);
-
-  bool move(symbolt &symbol, symbolt *&new_symbol);
-
-  void clear()
+public:
+  virtual const symbol_tablet &get_symbol_table() const override
   {
-    internal_symbols.clear();
-    internal_symbol_base_map.clear();
-    internal_symbol_module_map.clear();
+    return *this;
   }
 
-  bool remove(const irep_idt &name);
-
-  void erase(const symbolst::const_iterator &entry);
-
-  void show(std::ostream &out) const;
-
-  void swap(symbol_tablet &other)
+  /// Find a symbol in the symbol table for read-write access.
+  /// \param name: The name of the symbol to look for
+  /// \return a pointer to the found symbol if it exists, nullptr otherwise.
+  virtual symbolt *get_writeable(const irep_idt &name) override
   {
-    internal_symbols.swap(other.internal_symbols);
-    internal_symbol_base_map.swap(other.internal_symbol_base_map);
-    internal_symbol_module_map.swap(other.internal_symbol_module_map);
+    symbolst::iterator it = internal_symbols.find(name);
+    return it != internal_symbols.end() ? &it->second : nullptr;
   }
 
-private:
-  const symbolt *lookup_impl(const irep_idt &id) const
-    { return lookup_impl(*this, id); }
-
-  symbolt *lookup_impl(const irep_idt &id)
-    { return lookup_impl(*this, id); }
+  virtual std::pair<symbolt &, bool> insert(symbolt symbol) override;
+  virtual bool move(symbolt &symbol, symbolt *&new_symbol) override;
 
-  template<typename T>
-  static auto lookup_impl(T &t, const irep_idt &id)
-    -> decltype(std::declval<T>().lookup_impl(id))
+  virtual void erase(const symbolst::const_iterator &entry) override;
+  virtual void clear() override
   {
-    const auto it=t.internal_symbols.find(id);
-    return it==t.internal_symbols.end()?nullptr:&it->second;
+    internal_symbols.clear();
+    internal_symbol_base_map.clear();
+    internal_symbol_module_map.clear();
   }
 };
 
-std::ostream &operator << (
-  std::ostream &out,
-  const symbol_tablet &symbol_table);
-
 #endif // CPROVER_UTIL_SYMBOL_TABLE_H
diff --git a/src/util/symbol_table_base.cpp b/src/util/symbol_table_base.cpp
new file mode 100644
index 00000000000..fbefd8d1080
--- /dev/null
+++ b/src/util/symbol_table_base.cpp
@@ -0,0 +1,60 @@
+// Copyright 2017 Diffblue Limited. All Rights Reserved.
+
+#include "symbol_table_base.h"
+
+#include <ostream>
+#include <algorithm>
+
+/// Add a new symbol to the symbol table
+/// \param symbol: The symbol to be added to the symbol table
+/// \return Returns true if the process failed, which should only happen if
+///   there is a symbol with the same name already in the symbol table.
+bool symbol_table_baset::add(const symbolt &symbol)
+{
+  return !insert(symbol).second;
+}
+
+/// Remove a symbol from the symbol table
+/// \param name: The name of the symbol to remove
+/// \return Returns a boolean indicating whether the process failed
+///   i.e. false if the symbol was removed, or true if it didn't exist.
+bool symbol_table_baset::remove(const irep_idt &name)
+{
+  symbolst::const_iterator entry = symbols.find(name);
+  if(entry == symbols.end())
+    return true;
+  erase(entry);
+  return false;
+}
+
+/// Print the contents of the symbol table
+/// \param out: The ostream to direct output to
+void symbol_table_baset::show(std::ostream &out) const
+{
+  std::vector<irep_idt> sorted_names;
+  sorted_names.reserve(symbols.size());
+  for(const auto &elem : symbols)
+    sorted_names.push_back(elem.first);
+  std::sort(
+    sorted_names.begin(),
+    sorted_names.end(),
+    [](const irep_idt &a, const irep_idt &b)
+    {
+      return as_string(a) < as_string(b);
+    });
+  out << "\n"
+      << "Symbols:"
+      << "\n";
+  for(const auto &name : sorted_names)
+    out << symbols.at(name);
+}
+
+/// Print the contents of the symbol table
+/// \param out: The ostream to direct output to
+/// \param symbol_table: The symbol table to print out
+std::ostream &
+operator<<(std::ostream &out, const symbol_table_baset &symbol_table)
+{
+  symbol_table.show(out);
+  return out;
+}
diff --git a/src/util/symbol_table_base.h b/src/util/symbol_table_base.h
new file mode 100644
index 00000000000..9b8327741e1
--- /dev/null
+++ b/src/util/symbol_table_base.h
@@ -0,0 +1,125 @@
+// Copyright 2017 Diffblue Limited. All Rights Reserved.
+
+/// \file
+/// Symbol table base class interface
+
+/// \defgroup gr_symbol_table Symbol Table
+
+#ifndef CPROVER_UTIL_SYMBOL_TABLE_BASE_H
+#define CPROVER_UTIL_SYMBOL_TABLE_BASE_H
+
+#include <iosfwd>
+#include <map>
+#include <unordered_map>
+
+#include <util/optional.h>
+
+#include "symbol.h"
+
+typedef std::multimap<irep_idt, irep_idt> symbol_base_mapt;
+typedef std::multimap<irep_idt, irep_idt> symbol_module_mapt;
+
+class symbol_tablet;
+
+/// \brief The symbol table base class interface
+/// \ingroup gr_symbol_table
+class symbol_table_baset
+{
+public:
+  typedef std::unordered_map<irep_idt, symbolt, irep_id_hash> symbolst;
+
+public:
+  const symbolst &symbols;
+  const symbol_base_mapt &symbol_base_map;
+  const symbol_module_mapt &symbol_module_map;
+
+public:
+  symbol_table_baset(
+    const symbolst &symbols,
+    const symbol_base_mapt &symbol_base_map,
+    const symbol_module_mapt &symbol_module_map)
+    : symbols(symbols),
+      symbol_base_map(symbol_base_map),
+      symbol_module_map(symbol_module_map)
+  {
+  }
+
+  symbol_table_baset(const symbol_table_baset &other) = delete;
+  symbol_table_baset &operator=(const symbol_table_baset &other) = delete;
+
+public:
+  /// Permits implicit cast to const symbol_tablet &
+  operator const symbol_tablet &() const
+  {
+    return get_symbol_table();
+  }
+  virtual const symbol_tablet &get_symbol_table() const = 0;
+
+  /// Check whether a symbol exists in the symbol table
+  /// \param name: The name of the symbol to look for
+  /// \return true if the symbol exists
+  bool has_symbol(const irep_idt &name) const
+  {
+    return symbols.find(name) != symbols.end();
+  }
+
+  /// Find a symbol in the symbol table for read-only access.
+  /// \param name: The name of the symbol to look for
+  /// \return a pointer to the found symbol if it exists, nullptr otherwise.
+  const symbolt *lookup(const irep_idt &name) const
+  {
+    symbolst::const_iterator it = symbols.find(name);
+    return it != symbols.end() ? &it->second : nullptr;
+  }
+
+  /// Find a symbol in the symbol table for read-only access.
+  /// \param name: The name of the symbol to look for
+  /// \return A reference to the symbol
+  /// \throw `std::out_of_range` if no such symbol exists
+  const symbolt &lookup_ref(const irep_idt &name) const
+  {
+    return symbols.at(name);
+  }
+
+  /// Find a symbol in the symbol table for read-write access.
+  /// \param name: The name of the symbol to look for
+  /// \return a pointer to the found symbol if it exists, nullptr otherwise.
+  virtual symbolt *get_writeable(const irep_idt &name) = 0;
+
+  /// Find a symbol in the symbol table for read-write access.
+  /// \param name: The name of the symbol to look for
+  /// \return A reference to the symbol
+  /// \throw `std::out_of_range` if no such symbol exists
+  symbolt &get_writeable_ref(const irep_idt &name)
+  {
+    symbolt *symbol = get_writeable(name);
+    if(symbol == nullptr)
+      throw std::out_of_range("name not found in symbol_table");
+    return *symbol;
+  }
+
+  bool add(const symbolt &symbol);
+  /// Move or copy a new symbol to the symbol table
+  /// \remark: This is a nicer interface than move and achieves the same
+  /// result as both move and add
+  /// \param symbol: The symbol to be added to the symbol table - can be
+  /// moved or copied in
+  /// \return Returns a reference to the newly inserted symbol or to the
+  /// existing symbol if a symbol with the same name already exists in the
+  /// symbol table, along with a bool that is true if a new symbol was inserted.
+  virtual std::pair<symbolt &, bool> insert(symbolt symbol) = 0;
+  virtual bool move(symbolt &symbol, symbolt *&new_symbol) = 0;
+
+  bool remove(const irep_idt &name);
+  /// Remove a symbol from the symbol table
+  /// \param entry: an iterator pointing at the symbol to remove
+  virtual void erase(const symbolst::const_iterator &entry) = 0;
+  virtual void clear() = 0;
+
+  void show(std::ostream &out) const;
+};
+
+std::ostream &
+operator<<(std::ostream &out, const symbol_table_baset &symbol_table);
+
+#endif // CPROVER_UTIL_SYMBOL_TABLE_BASE_H
diff --git a/src/util/symbol_table_writer.h b/src/util/symbol_table_writer.h
deleted file mode 100644
index 4dd62a5e2dd..00000000000
--- a/src/util/symbol_table_writer.h
+++ /dev/null
@@ -1,169 +0,0 @@
-
-// Copyright 2016-2017 DiffBlue Limited. All Rights Reserved.
-
-/// \file
-/// A symbol table writer that records which entries have been updated
-
-#ifndef CPROVER_UTIL_SYMBOL_TABLE_WRITER_H
-#define CPROVER_UTIL_SYMBOL_TABLE_WRITER_H
-
-#include <utility>
-#include <unordered_set>
-#include "irep.h"
-#include "symbol_table.h"
-
-/// \brief A symbol table wrapper that records which entries have been
-/// updated/removed
-/// \ingroup gr_symbol_table
-/// A caller can pass a `journalling_symbol_table_writert` into a callee that is
-/// expected to mutate it somehow, then after it has run inspect the recording
-/// table's journal to determine what has changed more cheaply than examining
-/// every symbol.
-///
-/// Example of usage:
-/// ```
-/// symbol_tablet real_table;
-/// init_table(real_table);
-///
-/// journalling_symbol_table_writert journal(actual_table); // Wraps real_table
-/// alter_table(journal);
-
-/// for(const auto &added : journal.added())
-/// {
-///   printf("%s was added\n", added.name);
-/// }
-class journalling_symbol_table_writert
-{
-public:
-  typedef std::unordered_set<irep_idt, irep_id_hash> changesett;
-private:
-  symbol_tablet &base_symbol_table;
-  // Symbols originally in the table will never be marked inserted
-  changesett inserted;
-  // get_writeable marks an existing symbol updated
-  // Inserted symbols are marked updated, removed ones aren't
-  changesett updated;
-  // Symbols not originally in the table will never be marked removed
-  changesett removed;
-
-private:
-  explicit journalling_symbol_table_writert(symbol_tablet &base_symbol_table):
-    base_symbol_table(base_symbol_table)
-  {
-  }
-
-public:
-  journalling_symbol_table_writert(
-    const journalling_symbol_table_writert &other)=delete;
-
-  journalling_symbol_table_writert(journalling_symbol_table_writert &&other)
-  : base_symbol_table(other.base_symbol_table),
-    inserted(std::move(other.inserted)),
-    updated(std::move(other.updated)),
-    removed(std::move(other.removed))
-  {
-  }
-
-  /// Permits implicit cast to const symbol_tablet &
-  operator const symbol_tablet &() const
-  {
-    return base_symbol_table;
-  }
-
-  static journalling_symbol_table_writert wrap(
-    symbol_tablet &base_symbol_table)
-  {
-    return journalling_symbol_table_writert(base_symbol_table);
-  }
-
-  bool add(const symbolt &symbol)
-  {
-    bool ret=base_symbol_table.add(symbol);
-    if(!ret)
-      on_insert(symbol.name);
-    return ret;
-  }
-
-  bool move(symbolt &symbol, symbolt *&new_symbol)
-  {
-    bool ret=base_symbol_table.move(symbol, new_symbol);
-    if(!ret)
-      on_insert(symbol.name);
-    else
-      on_update(symbol.name);
-    return ret;
-  }
-
-  symbolt *get_writeable(const irep_idt &identifier)
-  {
-    symbolt *result=base_symbol_table.get_writeable(identifier);
-    if(result)
-      on_update(identifier);
-    return result;
-  }
-
-  symbolt &get_writeable_ref(const irep_idt &identifier)
-  {
-    // Run on_update *after* the get-ref operation in case it throws
-    symbolt &result=base_symbol_table.get_writeable_ref(identifier);
-    on_update(identifier);
-    return result;
-  }
-
-  std::pair<symbolt &, bool> insert(symbolt symbol)
-  {
-    std::pair<symbolt &, bool> result=
-      base_symbol_table.insert(std::move(symbol));
-    if(result.second)
-      on_insert(result.first.name);
-    return result;
-  }
-
-  bool remove(const irep_idt &id)
-  {
-    bool ret=base_symbol_table.remove(id);
-    if(!ret)
-      on_remove(id);
-    return ret;
-  }
-
-  void erase(const symbol_tablet::symbolst::const_iterator &entry)
-  {
-    const irep_idt entry_name=entry->first;
-    base_symbol_table.erase(entry);
-    on_remove(entry_name);
-  }
-
-  void clear()
-  {
-    for(const auto &named_symbol : base_symbol_table.symbols)
-      on_remove(named_symbol.first);
-    base_symbol_table.clear();
-  }
-
-  const changesett &get_inserted() const { return inserted; }
-  const changesett &get_updated() const { return updated; }
-  const changesett &get_removed() const { return removed; }
-
-private:
-  void on_insert(const irep_idt &id)
-  {
-    if(removed.erase(id)==0)
-      inserted.insert(id);
-    updated.insert(id);
-  }
-
-  void on_update(const irep_idt &id)
-  {
-    updated.insert(id);
-  }
-
-  void on_remove(const irep_idt &id)
-  {
-    if(inserted.erase(id)==0)
-      removed.insert(id);
-    updated.erase(id);
-  }
-};
-
-#endif // CPROVER_UTIL_SYMBOL_TABLE_WRITER_H
diff --git a/unit/util/symbol_table.cpp b/unit/util/symbol_table.cpp
index 981a86b8b2a..e16b93e3507 100644
--- a/unit/util/symbol_table.cpp
+++ b/unit/util/symbol_table.cpp
@@ -3,7 +3,7 @@
 /// \file Tests for symbol_tablet
 
 #include <testing-utils/catch.hpp>
-#include <util/symbol_table_writer.h>
+#include <util/journalling_symbol_table.h>
 
 SCENARIO("journalling_symbol_table_writer",
   "[core][utils][journalling_symbol_table_writer]")
@@ -11,8 +11,8 @@ SCENARIO("journalling_symbol_table_writer",
   GIVEN("A journalling_symbol_table_writert wrapping an empty symbol_tablet")
   {
     symbol_tablet base_symbol_table;
-    journalling_symbol_table_writert symbol_table=
-      journalling_symbol_table_writert::wrap(base_symbol_table);
+    journalling_symbol_tablet symbol_table =
+      journalling_symbol_tablet::wrap(base_symbol_table);
     const symbol_tablet &read_symbol_table=symbol_table;
 
     irep_idt symbol_name="Test";