diff --git a/src/goto-programs/convert_nondet.cpp b/src/goto-programs/convert_nondet.cpp
index 6e6950f95ce..56215c07cd1 100644
--- a/src/goto-programs/convert_nondet.cpp
+++ b/src/goto-programs/convert_nondet.cpp
@@ -32,7 +32,7 @@ Author: Reuben Thomas, reuben.thomas@diffblue.com
 static goto_programt::targett insert_nondet_init_code(
   goto_programt &goto_program,
   const goto_programt::targett &target,
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   message_handlert &message_handler,
   const object_factory_parameterst &object_factory_parameters)
 {
@@ -113,7 +113,7 @@ static goto_programt::targett insert_nondet_init_code(
 /// \param max_nondet_array_length: Maximum size of new nondet arrays.
 void convert_nondet(
   goto_programt &goto_program,
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   message_handlert &message_handler,
   const object_factory_parameterst &object_factory_parameters)
 {
@@ -146,7 +146,7 @@ void convert_nondet(
 
 void convert_nondet(
   goto_functionst &goto_functions,
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   message_handlert &message_handler,
   const object_factory_parameterst &object_factory_parameters)
 {
diff --git a/src/goto-programs/convert_nondet.h b/src/goto-programs/convert_nondet.h
index 14a2840eb68..51355d8d904 100644
--- a/src/goto-programs/convert_nondet.h
+++ b/src/goto-programs/convert_nondet.h
@@ -15,7 +15,7 @@ Author: Reuben Thomas, reuben.thomas@diffblue.com
 #include <cstddef> // size_t
 
 class goto_functionst;
-class symbol_tablet;
+class symbol_table_baset;
 class goto_modelt;
 class goto_model_functiont;
 class message_handlert;
@@ -30,7 +30,7 @@ struct object_factory_parameterst;
 ///   objects.
 void convert_nondet(
   goto_functionst &,
-  symbol_tablet &,
+  symbol_table_baset &,
   message_handlert &,
   const object_factory_parameterst &object_factory_parameters);
 
diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp
index d624b48b45b..23135646621 100644
--- a/src/goto-programs/goto_convert.cpp
+++ b/src/goto-programs/goto_convert.cpp
@@ -2178,7 +2178,7 @@ const symbolt &goto_convertt::lookup(const irep_idt &identifier)
 
 void goto_convert(
   const codet &code,
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   goto_programt &dest,
   message_handlert &message_handler)
 {
@@ -2212,7 +2212,7 @@ void goto_convert(
 }
 
 void goto_convert(
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   goto_programt &dest,
   message_handlert &message_handler)
 {
diff --git a/src/goto-programs/goto_convert.h b/src/goto-programs/goto_convert.h
index c0196486ae4..814731fbdb4 100644
--- a/src/goto-programs/goto_convert.h
+++ b/src/goto-programs/goto_convert.h
@@ -20,13 +20,13 @@ Author: Daniel Kroening, kroening@kroening.com
 // start from given code
 void goto_convert(
   const codet &code,
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   goto_programt &dest,
   message_handlert &message_handler);
 
 // start from "main"
 void goto_convert(
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   goto_programt &dest,
   message_handlert &message_handler);
 
diff --git a/src/goto-programs/goto_convert_class.h b/src/goto-programs/goto_convert_class.h
index f6d1ba411f5..8944e0dc3e6 100644
--- a/src/goto-programs/goto_convert_class.h
+++ b/src/goto-programs/goto_convert_class.h
@@ -29,7 +29,7 @@ class goto_convertt:public messaget
   void goto_convert(const codet &code, goto_programt &dest);
 
   goto_convertt(
-    symbol_tablet &_symbol_table,
+    symbol_table_baset &_symbol_table,
     message_handlert &_message_handler):
     messaget(_message_handler),
     symbol_table(_symbol_table),
@@ -44,7 +44,7 @@ class goto_convertt:public messaget
   }
 
 protected:
-  symbol_tablet &symbol_table;
+  symbol_table_baset &symbol_table;
   namespacet ns;
   unsigned temporary_counter;
   std::string tmp_symbol_prefix;
diff --git a/src/goto-programs/goto_convert_functions.cpp b/src/goto-programs/goto_convert_functions.cpp
index 4aa3c8d90ee..88563287512 100644
--- a/src/goto-programs/goto_convert_functions.cpp
+++ b/src/goto-programs/goto_convert_functions.cpp
@@ -21,7 +21,7 @@ Date: June 2003
 #include "goto_inline.h"
 
 goto_convert_functionst::goto_convert_functionst(
-  symbol_tablet &_symbol_table,
+  symbol_table_baset &_symbol_table,
   message_handlert &_message_handler):
   goto_convertt(_symbol_table, _message_handler)
 {
@@ -234,7 +234,7 @@ void goto_convert(
 }
 
 void goto_convert(
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   goto_functionst &functions,
   message_handlert &message_handler)
 {
@@ -269,7 +269,7 @@ void goto_convert(
 
 void goto_convert(
   const irep_idt &identifier,
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   goto_functionst &functions,
   message_handlert &message_handler)
 {
diff --git a/src/goto-programs/goto_convert_functions.h b/src/goto-programs/goto_convert_functions.h
index 310d5e3c62c..537f34ec017 100644
--- a/src/goto-programs/goto_convert_functions.h
+++ b/src/goto-programs/goto_convert_functions.h
@@ -20,7 +20,7 @@ Date: June 2003
 
 // convert it all!
 void goto_convert(
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   goto_functionst &functions,
   message_handlert &);
 
@@ -32,7 +32,7 @@ void goto_convert(
 // just convert a specific function
 void goto_convert(
   const irep_idt &identifier,
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   goto_functionst &functions,
   message_handlert &);
 
@@ -45,7 +45,7 @@ class goto_convert_functionst:public goto_convertt
     goto_functionst::goto_functiont &result);
 
   goto_convert_functionst(
-    symbol_tablet &_symbol_table,
+    symbol_table_baset &_symbol_table,
     message_handlert &_message_handler);
 
   virtual ~goto_convert_functionst();
diff --git a/src/goto-programs/goto_model.h b/src/goto-programs/goto_model.h
index f81dae1c162..a04d7aa5bc8 100644
--- a/src/goto-programs/goto_model.h
+++ b/src/goto-programs/goto_model.h
@@ -13,6 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #define CPROVER_GOTO_PROGRAMS_GOTO_MODEL_H
 
 #include <util/symbol_table.h>
+#include <util/journalling_symbol_table.h>
 
 #include "goto_functions.h"
 
@@ -82,9 +83,12 @@ class goto_model_functiont
   ///   goto programs, specifically incrementing its unused_location_number
   ///   member each time a program is re-numbered.
   /// \param goto_function: function to wrap.
-  explicit goto_model_functiont(
-    goto_modelt &goto_model, goto_functionst::goto_functiont &goto_function):
-  goto_model(goto_model),
+  goto_model_functiont(
+    journalling_symbol_tablet &symbol_table,
+    goto_functionst &goto_functions,
+    goto_functionst::goto_functiont &goto_function):
+  symbol_table(symbol_table),
+  goto_functions(goto_functions),
   goto_function(goto_function)
   {
   }
@@ -94,14 +98,16 @@ class goto_model_functiont
   /// program order within the program.
   void compute_location_numbers()
   {
-    goto_model.goto_functions.compute_location_numbers(goto_function.body);
+    goto_functions.compute_location_numbers(goto_function.body);
   }
 
   /// Get symbol table
-  /// \return symbol table from the associated GOTO model
-  symbol_tablet &get_symbol_table()
+  /// \return journalling symbol table that (a) wraps the global symbol table,
+  ///   and (b) has recorded all symbol mutations (insertions, updates and
+  ///   deletions) that resulted from creating `goto_function`.
+  journalling_symbol_tablet &get_symbol_table()
   {
-    return goto_model.symbol_table;
+    return symbol_table;
   }
 
   /// Get GOTO function
@@ -111,17 +117,9 @@ class goto_model_functiont
     return goto_function;
   }
 
-  /// Get GOTO model. This returns a const reference because this interface is
-  /// intended for use where non-const access to the whole model should not be
-  /// allowed.
-  /// \return const view of the whole GOTO model.
-  const goto_modelt &get_goto_model()
-  {
-    return goto_model;
-  }
-
 private:
-  goto_modelt &goto_model;
+  journalling_symbol_tablet &symbol_table;
+  goto_functionst &goto_functions;
   goto_functionst::goto_functiont &goto_function;
 };
 
diff --git a/src/goto-programs/lazy_goto_functions_map.h b/src/goto-programs/lazy_goto_functions_map.h
index 5dbcf9a22ea..2ee31010f75 100644
--- a/src/goto-programs/lazy_goto_functions_map.h
+++ b/src/goto-programs/lazy_goto_functions_map.h
@@ -11,7 +11,7 @@
 #include "goto_convert_functions.h"
 #include <util/message.h>
 #include <util/language_file.h>
-
+#include <util/journalling_symbol_table.h>
 
 /// Provides a wrapper for a map of lazily loaded goto_functiont.
 /// This incrementally builds a goto-functions object, while permitting
@@ -48,7 +48,9 @@ class lazy_goto_functions_mapt final
   typedef std::size_t size_type;
 
   typedef
-  std::function<void(goto_functionst::goto_functiont &function)>
+    std::function<void(
+      goto_functionst::goto_functiont &function,
+      journalling_symbol_tablet &function_symbols)>
     post_process_functiont;
 
 private:
@@ -61,11 +63,8 @@ class lazy_goto_functions_mapt final
 
   language_filest &language_files;
   symbol_tablet &symbol_table;
-  // This is mutable because it has internal state that it changes during the
-  // course of conversion. Strictly it should make that state mutable or
-  // recreate it for each conversion, but it's easier just to store it mutable.
-  mutable goto_convert_functionst convert_functions;
   const post_process_functiont post_process_function;
+  message_handlert &message_handler;
 
 public:
   /// Creates a lazy_goto_functions_mapt.
@@ -78,8 +77,8 @@ class lazy_goto_functions_mapt final
   : goto_functions(goto_functions),
     language_files(language_files),
     symbol_table(symbol_table),
-    convert_functions(symbol_table, message_handler),
-    post_process_function(std::move(post_process_function))
+    post_process_function(std::move(post_process_function)),
+    message_handler(message_handler)
   {
   }
 
@@ -122,12 +121,14 @@ class lazy_goto_functions_mapt final
   // const first
   reference ensure_function_loaded_internal(const key_type &name) const
   {
-    reference named_function=ensure_entry_converted(name);
+    journalling_symbol_tablet journalling_table =
+      journalling_symbol_tablet::wrap(symbol_table);
+    reference named_function=ensure_entry_converted(name, journalling_table);
     mapped_type function=named_function.second;
     if(processed_functions.count(name)==0)
     {
       // Run function-pass conversions
-      post_process_function(function);
+      post_process_function(function, journalling_table);
       // Assign procedure-local location numbers for now
       function.body.compute_location_numbers();
       processed_functions.insert(name);
@@ -135,16 +136,28 @@ class lazy_goto_functions_mapt final
     return named_function;
   }
 
-  reference ensure_entry_converted(const key_type &name) const
+  /// Convert a function if not already converted, then return a reference to
+  /// its goto_functionst map entry.
+  /// \param name: ID of the function to convert
+  /// \param function_symbol_table: mutable symbol table reference to be used
+  ///   when converting the function (e.g. to add new local variables).
+  ///   Note we should not use a global pre-cached symbol table reference for
+  ///   this so that our callers can insert a journalling table here if needed.
+  /// \return reference to the new or existing goto_functions map entry.
+  reference ensure_entry_converted(
+    const key_type &name,
+    symbol_table_baset &function_symbol_table) const
   {
     typename underlying_mapt::iterator it=goto_functions.find(name);
     if(it!=goto_functions.end())
       return *it;
     // Fill in symbol table entry body if not already done
     // If this returns false then it's a stub
-    language_files.convert_lazy_method(name, symbol_table);
+    language_files.convert_lazy_method(name, function_symbol_table);
     // Create goto_functiont
     goto_functionst::goto_functiont function;
+    goto_convert_functionst convert_functions(
+      function_symbol_table, message_handler);
     convert_functions.convert_function(name, function);
     // Add to map
     return *goto_functions.emplace(name, std::move(function)).first;
diff --git a/src/goto-programs/lazy_goto_model.cpp b/src/goto-programs/lazy_goto_model.cpp
index cbd61295820..a2f86cef74d 100644
--- a/src/goto-programs/lazy_goto_model.cpp
+++ b/src/goto-programs/lazy_goto_model.cpp
@@ -28,9 +28,14 @@ lazy_goto_modelt::lazy_goto_modelt(
       goto_model->goto_functions.function_map,
       language_files,
       symbol_table,
-      [this] (goto_functionst::goto_functiont &function) -> void
+      [this] (
+        goto_functionst::goto_functiont &function,
+        journalling_symbol_tablet &journalling_symbol_table) -> void
       {
-        goto_model_functiont model_function(*goto_model, function);
+        goto_model_functiont model_function(
+          journalling_symbol_table,
+          goto_model->goto_functions,
+          function);
         this->post_process_function(model_function, *this);
       },
       message_handler),
@@ -48,9 +53,14 @@ lazy_goto_modelt::lazy_goto_modelt(lazy_goto_modelt &&other)
       goto_model->goto_functions.function_map,
       language_files,
       symbol_table,
-      [this] (goto_functionst::goto_functiont &function) -> void
+      [this] (
+        goto_functionst::goto_functiont &function,
+        journalling_symbol_tablet &journalling_symbol_table) -> void
       {
-        goto_model_functiont model_function(*goto_model, function);
+        goto_model_functiont model_function(
+          journalling_symbol_table,
+          goto_model->goto_functions,
+          function);
         this->post_process_function(model_function, *this);
       },
       other.message_handler),
diff --git a/src/goto-programs/remove_instanceof.cpp b/src/goto-programs/remove_instanceof.cpp
index 0e0999cf0d0..50166e33d03 100644
--- a/src/goto-programs/remove_instanceof.cpp
+++ b/src/goto-programs/remove_instanceof.cpp
@@ -22,7 +22,7 @@ Author: Chris Smowton, chris.smowton@diffblue.com
 class remove_instanceoft
 {
 public:
-  explicit remove_instanceoft(symbol_tablet &symbol_table)
+  explicit remove_instanceoft(symbol_table_baset &symbol_table)
   : symbol_table(symbol_table), ns(symbol_table)
   {
     class_hierarchy(symbol_table);
@@ -35,7 +35,7 @@ class remove_instanceoft
   bool lower_instanceof(goto_programt &, goto_programt::targett);
 
 protected:
-  symbol_tablet &symbol_table;
+  symbol_table_baset &symbol_table;
   namespacet ns;
   class_hierarchyt class_hierarchy;
 
@@ -183,7 +183,7 @@ bool remove_instanceoft::lower_instanceof(goto_programt &goto_program)
 void remove_instanceof(
   goto_programt::targett target,
   goto_programt &goto_program,
-  symbol_tablet &symbol_table)
+  symbol_table_baset &symbol_table)
 {
   remove_instanceoft rem(symbol_table);
   rem.lower_instanceof(goto_program, target);
@@ -196,7 +196,7 @@ void remove_instanceof(
 /// \param symbol_table: The symbol table to add symbols to.
 void remove_instanceof(
   goto_functionst::goto_functiont &function,
-  symbol_tablet &symbol_table)
+  symbol_table_baset &symbol_table)
 {
   remove_instanceoft rem(symbol_table);
   rem.lower_instanceof(function.body);
@@ -209,7 +209,7 @@ void remove_instanceof(
 /// \param symbol_table: The symbol table to add symbols to.
 void remove_instanceof(
   goto_functionst &goto_functions,
-  symbol_tablet &symbol_table)
+  symbol_table_baset &symbol_table)
 {
   remove_instanceoft rem(symbol_table);
   bool changed=false;
diff --git a/src/goto-programs/remove_instanceof.h b/src/goto-programs/remove_instanceof.h
index 0cc6957734a..b492de5dc6b 100644
--- a/src/goto-programs/remove_instanceof.h
+++ b/src/goto-programs/remove_instanceof.h
@@ -19,15 +19,15 @@ Author: Chris Smowton, chris.smowton@diffblue.com
 void remove_instanceof(
   goto_programt::targett target,
   goto_programt &goto_program,
-  symbol_tablet &symbol_table);
+  symbol_table_baset &symbol_table);
 
 void remove_instanceof(
   goto_functionst::goto_functiont &function,
-  symbol_tablet &symbol_table);
+  symbol_table_baset &symbol_table);
 
 void remove_instanceof(
   goto_functionst &goto_functions,
-  symbol_tablet &symbol_table);
+  symbol_table_baset &symbol_table);
 
 void remove_instanceof(goto_modelt &model);
 
diff --git a/src/goto-programs/remove_returns.cpp b/src/goto-programs/remove_returns.cpp
index e5235071190..3894dae6ba3 100644
--- a/src/goto-programs/remove_returns.cpp
+++ b/src/goto-programs/remove_returns.cpp
@@ -19,7 +19,7 @@ Date:   September 2009
 class remove_returnst
 {
 public:
-  explicit remove_returnst(symbol_tablet &_symbol_table):
+  explicit remove_returnst(symbol_table_baset &_symbol_table):
     symbol_table(_symbol_table)
   {
   }
@@ -35,7 +35,7 @@ class remove_returnst
     goto_functionst &goto_functions);
 
 protected:
-  symbol_tablet &symbol_table;
+  symbol_table_baset &symbol_table;
 
   void replace_returns(
     const irep_idt &function_id,
@@ -251,7 +251,7 @@ void remove_returnst::operator()(
 
 /// removes returns
 void remove_returns(
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   goto_functionst &goto_functions)
 {
   remove_returnst rr(symbol_table);
@@ -290,7 +290,7 @@ void remove_returns(goto_modelt &goto_model)
 /// \return the function's type with its `return_type()` restored to its
 ///   original value if a \#return_value variable exists, or nil otherwise
 code_typet original_return_type(
-  const symbol_tablet &symbol_table,
+  const symbol_table_baset &symbol_table,
   const irep_idt &function_id)
 {
   code_typet type;
diff --git a/src/goto-programs/remove_returns.h b/src/goto-programs/remove_returns.h
index 50bbf22e246..f2017111478 100644
--- a/src/goto-programs/remove_returns.h
+++ b/src/goto-programs/remove_returns.h
@@ -22,7 +22,7 @@ Date:   September 2009
 // unless the function returns void,
 // and a 'goto the_end_of_the_function'.
 
-void remove_returns(symbol_tablet &, goto_functionst &);
+void remove_returns(symbol_table_baset &, goto_functionst &);
 
 typedef std::function<bool(const irep_idt &)> function_is_stubt;
 
@@ -31,12 +31,12 @@ void remove_returns(goto_model_functiont &, function_is_stubt);
 void remove_returns(goto_modelt &);
 
 // reverse the above operations
-void restore_returns(symbol_tablet &, goto_functionst &);
+void restore_returns(symbol_table_baset &, goto_functionst &);
 
 void restore_returns(goto_modelt &);
 
 code_typet original_return_type(
-  const symbol_tablet &symbol_table,
+  const symbol_table_baset &symbol_table,
   const irep_idt &function_id);
 
 #endif // CPROVER_GOTO_PROGRAMS_REMOVE_RETURNS_H
diff --git a/src/goto-programs/remove_virtual_functions.cpp b/src/goto-programs/remove_virtual_functions.cpp
index b25a7b1c81e..ba97916ff78 100644
--- a/src/goto-programs/remove_virtual_functions.cpp
+++ b/src/goto-programs/remove_virtual_functions.cpp
@@ -24,7 +24,7 @@ class remove_virtual_functionst
 {
 public:
   remove_virtual_functionst(
-    const symbol_tablet &_symbol_table);
+    const symbol_table_baset &_symbol_table);
 
   void operator()(goto_functionst &goto_functions);
 
@@ -38,7 +38,7 @@ class remove_virtual_functionst
 
 protected:
   const namespacet ns;
-  const symbol_tablet &symbol_table;
+  const symbol_table_baset &symbol_table;
 
   class_hierarchyt class_hierarchy;
 
@@ -64,7 +64,7 @@ class remove_virtual_functionst
 };
 
 remove_virtual_functionst::remove_virtual_functionst(
-  const symbol_tablet &_symbol_table):
+  const symbol_table_baset &_symbol_table):
   ns(_symbol_table),
   symbol_table(_symbol_table)
 {
@@ -431,7 +431,7 @@ void remove_virtual_functionst::operator()(goto_functionst &functions)
 }
 
 void remove_virtual_functions(
-  const symbol_tablet &symbol_table,
+  const symbol_table_baset &symbol_table,
   goto_functionst &goto_functions)
 {
   remove_virtual_functionst rvf(symbol_table);
diff --git a/src/goto-programs/remove_virtual_functions.h b/src/goto-programs/remove_virtual_functions.h
index aeab4713564..bd5b396341a 100644
--- a/src/goto-programs/remove_virtual_functions.h
+++ b/src/goto-programs/remove_virtual_functions.h
@@ -22,7 +22,7 @@ void remove_virtual_functions(
   goto_modelt &goto_model);
 
 void remove_virtual_functions(
-  const symbol_tablet &symbol_table,
+  const symbol_table_baset &symbol_table,
   goto_functionst &goto_functions);
 
 /// Remove virtual functions from one function.
diff --git a/src/java_bytecode/java_bytecode_language.cpp b/src/java_bytecode/java_bytecode_language.cpp
index 73c23711f03..44a745026f1 100644
--- a/src/java_bytecode/java_bytecode_language.cpp
+++ b/src/java_bytecode/java_bytecode_language.cpp
@@ -379,7 +379,7 @@ void java_bytecode_languaget::methods_provided(id_sett &methods) const
 /// \param symtab: global symbol table
 void java_bytecode_languaget::convert_lazy_method(
   const irep_idt &function_id,
-  symbol_tablet &symtab)
+  symbol_table_baset &symtab)
 {
   const symbolt &symbol = symtab.lookup_ref(function_id);
   if(symbol.value.is_not_nil())
diff --git a/src/java_bytecode/java_bytecode_language.h b/src/java_bytecode/java_bytecode_language.h
index 905c56afb6e..a637fc5f556 100644
--- a/src/java_bytecode/java_bytecode_language.h
+++ b/src/java_bytecode/java_bytecode_language.h
@@ -152,7 +152,7 @@ class java_bytecode_languaget:public languaget
   virtual void methods_provided(id_sett &methods) const override;
   virtual void convert_lazy_method(
     const irep_idt &function_id,
-    symbol_tablet &symbol_table) override;
+    symbol_table_baset &symbol_table) override;
 
 protected:
   void convert_single_method(
diff --git a/src/jbmc/jbmc_parse_options.cpp b/src/jbmc/jbmc_parse_options.cpp
index 3bf13fc6951..29eeb903919 100644
--- a/src/jbmc/jbmc_parse_options.cpp
+++ b/src/jbmc/jbmc_parse_options.cpp
@@ -573,6 +573,10 @@ int jbmc_parse_optionst::get_goto_program(
       *this, options, get_message_handler());
     lazy_goto_model.initialize(cmdline);
 
+    // Add failed symbols for any symbol created prior to loading any
+    // particular function:
+    add_failed_symbols(lazy_goto_model.symbol_table);
+
     status() << "Generating GOTO Program" << messaget::eom;
     lazy_goto_model.load_all_functions();
 
@@ -646,14 +650,11 @@ void jbmc_parse_optionst::process_goto_function(
   const can_produce_functiont &available_functions,
   const optionst &options)
 {
-  symbol_tablet &symbol_table = function.get_symbol_table();
+  journalling_symbol_tablet &symbol_table = function.get_symbol_table();
   namespacet ns(symbol_table);
   goto_functionst::goto_functiont &goto_function = function.get_goto_function();
   try
   {
-    // Remove inline assembler; this needs to happen before
-    // adding the library.
-    remove_asm(goto_function, symbol_table);
     // Removal of RTTI inspection:
     remove_instanceof(goto_function, symbol_table);
     // Java virtual functions -> explicit dispatch tables:
@@ -696,6 +697,17 @@ void jbmc_parse_optionst::process_goto_function(
 
     // checks don't know about adjusted float expressions
     adjust_float_expressions(goto_function, ns);
+
+    // add failed symbols for anything created relating to this particular
+    // function (note this means subseqent passes mustn't create more!):
+    journalling_symbol_tablet::changesett new_symbols =
+      symbol_table.get_inserted();
+    for(const irep_idt &new_symbol_name : new_symbols)
+    {
+      add_failed_symbol_if_needed(
+        symbol_table.lookup_ref(new_symbol_name),
+        symbol_table);
+    }
   }
 
   catch(const char *e)
@@ -742,10 +754,6 @@ bool jbmc_parse_optionst::process_goto_functions(
       nondet_static(goto_model);
     }
 
-    // add failed symbols
-    // needs to be done before pointer analysis
-    add_failed_symbols(goto_model.symbol_table);
-
     // recalculate numbers, etc.
     goto_model.goto_functions.update();
 
diff --git a/src/pointer-analysis/add_failed_symbols.cpp b/src/pointer-analysis/add_failed_symbols.cpp
index 16e4131339e..fe64957bf29 100644
--- a/src/pointer-analysis/add_failed_symbols.cpp
+++ b/src/pointer-analysis/add_failed_symbols.cpp
@@ -15,12 +15,20 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/namespace.h>
 #include <util/std_expr.h>
 
+/// Get the name of the special symbol used to denote an unknown referee pointed
+/// to by a given pointer-typed symbol.
+/// \param id: base symbol id
+/// \return id of the corresponding unknown-object ("failed") symbol.
 irep_idt failed_symbol_id(const irep_idt &id)
 {
   return id2string(id)+"$object";
 }
 
-void add_failed_symbol(symbolt &symbol, symbol_tablet &symbol_table)
+/// Create a failed-dereference symbol for the given base symbol if it is
+/// pointer-typed; if not, do nothing.
+/// \param symbol: symbol to created a failed symbol for
+/// \param symbol_table: global symbol table
+void add_failed_symbol(symbolt &symbol, symbol_table_baset &symbol_table)
 {
   if(symbol.type.id()==ID_pointer)
   {
@@ -43,7 +51,13 @@ void add_failed_symbol(symbolt &symbol, symbol_tablet &symbol_table)
   }
 }
 
-void add_failed_symbol(const symbolt &symbol, symbol_tablet &symbol_table)
+/// Create a failed-dereference symbol for the given base symbol if it is
+/// pointer-typed, an lvalue, and doesn't already have one. If any of these
+/// conditions are not met, do nothing.
+/// \param symbol: symbol to created a failed symbol for
+/// \param symbol_table: global symbol table
+void add_failed_symbol_if_needed(
+  const symbolt &symbol, symbol_table_baset &symbol_table)
 {
   if(!symbol.is_lvalue)
     return;
@@ -54,7 +68,10 @@ void add_failed_symbol(const symbolt &symbol, symbol_tablet &symbol_table)
   add_failed_symbol(*symbol_table.get_writeable(symbol.name), symbol_table);
 }
 
-void add_failed_symbols(symbol_tablet &symbol_table)
+/// Create a failed-dereference symbol for all symbols in the given table that
+/// need one (i.e. pointer-typed lvalues).
+/// \param symbol_table: global symbol table
+void add_failed_symbols(symbol_table_baset &symbol_table)
 {
   // the symbol table iterators are not stable, and
   // we are adding new symbols, this
@@ -64,9 +81,14 @@ void add_failed_symbols(symbol_tablet &symbol_table)
     symbol_list.push_back(&(named_symbol.second));
 
   for(const symbolt *symbol : symbol_list)
-    add_failed_symbol(*symbol, symbol_table);
+    add_failed_symbol_if_needed(*symbol, symbol_table);
 }
 
+/// Get the failed-dereference symbol for the given symbol
+/// \param expr: symbol expression to get a failed symbol for
+/// \param ns: global namespace
+/// \return symbol expression for the failed-dereference symbol, or nil_exprt
+///   if none exists.
 exprt get_failed_symbol(
   const symbol_exprt &expr,
   const namespacet &ns)
diff --git a/src/pointer-analysis/add_failed_symbols.h b/src/pointer-analysis/add_failed_symbols.h
index 2ae2228f564..94c8bd94059 100644
--- a/src/pointer-analysis/add_failed_symbols.h
+++ b/src/pointer-analysis/add_failed_symbols.h
@@ -14,12 +14,16 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/irep.h>
 
-class symbol_tablet;
+class symbol_table_baset;
+class symbolt;
 class exprt;
 class namespacet;
 class symbol_exprt;
 
-void add_failed_symbols(symbol_tablet &symbol_table);
+void add_failed_symbols(symbol_table_baset &symbol_table);
+
+void add_failed_symbol_if_needed(
+  const symbolt &symbol, symbol_table_baset &symbol_table);
 
 irep_idt failed_symbol_id(const irep_idt &identifier);
 
diff --git a/src/util/journalling_symbol_table.h b/src/util/journalling_symbol_table.h
index 2258b0ea203..2b9893bb0b7 100644
--- a/src/util/journalling_symbol_table.h
+++ b/src/util/journalling_symbol_table.h
@@ -38,7 +38,7 @@ class journalling_symbol_tablet : public symbol_table_baset
   typedef std::unordered_set<irep_idt, irep_id_hash> changesett;
 
 private:
-  symbol_tablet &base_symbol_table;
+  symbol_table_baset &base_symbol_table;
   // Symbols originally in the table will never be marked inserted
   changesett inserted;
   // get_writeable marks an existing symbol updated
@@ -48,7 +48,7 @@ class journalling_symbol_tablet : public symbol_table_baset
   changesett removed;
 
 private:
-  explicit journalling_symbol_tablet(symbol_tablet &base_symbol_table)
+  explicit journalling_symbol_tablet(symbol_table_baset &base_symbol_table)
     : symbol_table_baset(
         base_symbol_table.symbols,
         base_symbol_table.symbol_base_map,
@@ -74,10 +74,10 @@ class journalling_symbol_tablet : public symbol_table_baset
 
   virtual const symbol_tablet &get_symbol_table() const override
   {
-    return base_symbol_table;
+    return base_symbol_table.get_symbol_table();
   }
 
-  static journalling_symbol_tablet wrap(symbol_tablet &base_symbol_table)
+  static journalling_symbol_tablet wrap(symbol_table_baset &base_symbol_table)
   {
     return journalling_symbol_tablet(base_symbol_table);
   }
diff --git a/src/util/language.h b/src/util/language.h
index f1ee81f84a9..fe23e5b3186 100644
--- a/src/util/language.h
+++ b/src/util/language.h
@@ -83,7 +83,8 @@ class languaget:public messaget
 
   // populate a lazy method
   virtual void
-  convert_lazy_method(const irep_idt &function_id, symbol_tablet &symbol_table)
+  convert_lazy_method(
+    const irep_idt &function_id, symbol_table_baset &symbol_table)
   { }
 
   /// Final adjustments, e.g. initializing stub functions and globals that
diff --git a/src/util/language_file.cpp b/src/util/language_file.cpp
index 559648182aa..59637ca829e 100644
--- a/src/util/language_file.cpp
+++ b/src/util/language_file.cpp
@@ -37,7 +37,7 @@ void language_filet::get_modules()
 
 void language_filet::convert_lazy_method(
   const irep_idt &id,
-  symbol_tablet &symbol_table)
+  symbol_table_baset &symbol_table)
 {
   language->convert_lazy_method(id, symbol_table);
 }
diff --git a/src/util/language_file.h b/src/util/language_file.h
index ecdce4a1b91..fb71b06a336 100644
--- a/src/util/language_file.h
+++ b/src/util/language_file.h
@@ -49,7 +49,7 @@ class language_filet final
 
   void convert_lazy_method(
     const irep_idt &id,
-    symbol_tablet &symbol_table);
+    symbol_table_baset &symbol_table);
 
   explicit language_filet(const std::string &filename);
   language_filet(const language_filet &rhs);
@@ -119,7 +119,7 @@ class language_filest:public messaget
   // for this to be legal.
   void convert_lazy_method(
     const irep_idt &id,
-    symbol_tablet &symbol_table)
+    symbol_table_baset &symbol_table)
   {
     PRECONDITION(symbol_table.has_symbol(id));
     lazy_method_mapt::iterator it=lazy_method_map.find(id);