diff --git a/regression/jbmc-strings/StaticCharMethods05/test.desc b/regression/jbmc-strings/StaticCharMethods05/test.desc
index e6f2a0e6ee8..41218e79141 100644
--- a/regression/jbmc-strings/StaticCharMethods05/test.desc
+++ b/regression/jbmc-strings/StaticCharMethods05/test.desc
@@ -3,7 +3,6 @@ StaticCharMethods05.class
 --refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
-null-pointer-exception\.14\] Throw null: FAILURE
 ^\[.*assertion\.1\] .* line 12 .* FAILURE$
 ^\[.*assertion\.2\] .* line 22 .* FAILURE$
 ^VERIFICATION FAILED$
diff --git a/src/clobber/clobber_parse_options.cpp b/src/clobber/clobber_parse_options.cpp
index bfad81dd7da..fe5886721a0 100644
--- a/src/clobber/clobber_parse_options.cpp
+++ b/src/clobber/clobber_parse_options.cpp
@@ -32,6 +32,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <goto-programs/link_to_library.h>
 #include <goto-programs/goto_inline.h>
 #include <goto-programs/xml_goto_trace.h>
+#include <goto-programs/remove_java_new.h>
 
 #include <goto-instrument/dump_c.h>
 
@@ -207,6 +208,8 @@ bool clobber_parse_optionst::process_goto_program(
   goto_modelt &goto_model)
 {
   {
+    remove_java_new(goto_model, get_message_handler());
+
     // do partial inlining
     status() << "Partial Inlining" << eom;
     goto_partial_inline(goto_model, get_message_handler());
diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp
index f8d1fc1d331..c9f3548e7df 100644
--- a/src/goto-analyzer/goto_analyzer_parse_options.cpp
+++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp
@@ -37,6 +37,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <goto-programs/read_goto_binary.h>
 #include <goto-programs/goto_inline.h>
 #include <goto-programs/link_to_library.h>
+#include <goto-programs/remove_java_new.h>
 
 #include <analyses/is_threaded.h>
 #include <analyses/goto_check.h>
@@ -735,6 +736,8 @@ bool goto_analyzer_parse_optionst::process_goto_program(
     link_to_library(goto_model, ui_message_handler);
     #endif
 
+    remove_java_new(goto_model, get_message_handler());
+
     // remove function pointers
     status() << "Removing function pointers and virtual functions" << eom;
     remove_function_pointers(
diff --git a/src/goto-cc/compile.cpp b/src/goto-cc/compile.cpp
index 9ace2924747..63ef74ee201 100644
--- a/src/goto-cc/compile.cpp
+++ b/src/goto-cc/compile.cpp
@@ -483,14 +483,7 @@ bool compilet::parse(const std::string &file_name)
 
   languagep->set_message_handler(get_message_handler());
 
-  language_filet language_file;
-
-  std::pair<language_filest::file_mapt::iterator, bool>
-  res=language_files.file_map.insert(
-    std::pair<std::string, language_filet>(file_name, language_file));
-
-  language_filet &lf=res.first->second;
-  lf.filename=file_name;
+  language_filet &lf=language_files.add_file(file_name);
   lf.language=std::move(languagep);
 
   if(mode==PREPROCESS_ONLY)
@@ -640,7 +633,7 @@ bool compilet::parse_source(const std::string &file_name)
     return true;
 
   // so we remove it from the list afterwards
-  language_files.file_map.erase(file_name);
+  language_files.remove_file(file_name);
   return false;
 }
 
@@ -691,7 +684,7 @@ void compilet::add_compiler_specific_defines(configt &config) const
 
 void compilet::convert_symbols(goto_functionst &dest)
 {
-  goto_convert_functionst converter(symbol_table, dest, get_message_handler());
+  goto_convert_functionst converter(symbol_table, get_message_handler());
 
   // the compilation may add symbols!
 
@@ -724,7 +717,7 @@ void compilet::convert_symbols(goto_functionst &dest)
           s_it->second.value.is_not_nil())
       {
         debug() << "Compiling " << s_it->first << eom;
-        converter.convert_function(s_it->first);
+        converter.convert_function(s_it->first, dest.function_map[s_it->first]);
         symbol_table.get_writeable_ref(*it).value=exprt("compiled");
       }
     }
diff --git a/src/goto-diff/goto_diff_parse_options.cpp b/src/goto-diff/goto_diff_parse_options.cpp
index d439f1b9aa0..ea8b8cd1622 100644
--- a/src/goto-diff/goto_diff_parse_options.cpp
+++ b/src/goto-diff/goto_diff_parse_options.cpp
@@ -37,6 +37,7 @@ Author: Peter Schrammel
 #include <goto-programs/string_instrumentation.h>
 #include <goto-programs/loop_ids.h>
 #include <goto-programs/link_to_library.h>
+#include <goto-programs/remove_java_new.h>
 
 #include <pointer-analysis/add_failed_symbols.h>
 
@@ -394,9 +395,11 @@ bool goto_diff_parse_optionst::process_goto_program(
   {
     namespacet ns(symbol_table);
 
+    remove_java_new(goto_model, get_message_handler());
+
     // Remove inline assembler; this needs to happen before
     // adding the library.
-    remove_asm(symbol_table, goto_functions);
+    remove_asm(goto_model);
 
     // add the library
     link_to_library(symbol_table, goto_functions, ui_message_handler);
diff --git a/src/goto-programs/Makefile b/src/goto-programs/Makefile
index 2474a7d7e8b..bf4e5bb2491 100644
--- a/src/goto-programs/Makefile
+++ b/src/goto-programs/Makefile
@@ -27,6 +27,7 @@ SRC = basic_blocks.cpp \
       interpreter.cpp \
       interpreter_evaluate.cpp \
       json_goto_trace.cpp \
+      lazy_goto_model.cpp \
       link_goto_model.cpp \
       link_to_library.cpp \
       loop_ids.cpp \
@@ -44,6 +45,7 @@ SRC = basic_blocks.cpp \
       remove_exceptions.cpp \
       remove_function_pointers.cpp \
       remove_instanceof.cpp \
+      remove_java_new.cpp \
       remove_returns.cpp \
       remove_skip.cpp \
       remove_static_init_loops.cpp \
diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp
index 5f28a25e150..6a5826da46d 100644
--- a/src/goto-programs/builtin_functions.cpp
+++ b/src/goto-programs/builtin_functions.cpp
@@ -33,6 +33,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <ansi-c/string_constant.h>
 
 #include "format_strings.h"
+#include "class_identifier.h"
 
 void goto_convertt::do_prob_uniform(
   const exprt &lhs,
@@ -539,68 +540,6 @@ void goto_convertt::do_cpp_new(
   dest.destructive_append(tmp_initializer);
 }
 
-void set_class_identifier(
-  struct_exprt &expr,
-  const namespacet &ns,
-  const symbol_typet &class_type)
-{
-  const struct_typet &struct_type=
-    to_struct_type(ns.follow(expr.type()));
-  const struct_typet::componentst &components=struct_type.components();
-
-  if(components.empty())
-    return;
-  assert(!expr.operands().empty());
-
-  if(components.front().get_name()=="@class_identifier")
-  {
-    assert(expr.op0().id()==ID_constant);
-    expr.op0()=constant_exprt(class_type.get_identifier(), string_typet());
-  }
-  else
-  {
-    assert(expr.op0().id()==ID_struct);
-    set_class_identifier(to_struct_expr(expr.op0()), ns, class_type);
-  }
-}
-
-void goto_convertt::do_java_new(
-  const exprt &lhs,
-  const side_effect_exprt &rhs,
-  goto_programt &dest)
-{
-  PRECONDITION(!lhs.is_nil());
-  PRECONDITION(rhs.operands().empty());
-  PRECONDITION(rhs.type().id() == ID_pointer);
-  source_locationt location=rhs.source_location();
-  typet object_type=rhs.type().subtype();
-
-  // build size expression
-  exprt object_size=size_of_expr(object_type, ns);
-  CHECK_RETURN(object_size.is_not_nil());
-
-  // we produce a malloc side-effect, which stays
-  side_effect_exprt malloc_expr(ID_allocate);
-  malloc_expr.copy_to_operands(object_size);
-  // could use true and get rid of the code below
-  malloc_expr.copy_to_operands(false_exprt());
-  malloc_expr.type()=rhs.type();
-
-  goto_programt::targett t_n=dest.add_instruction(ASSIGN);
-  t_n->code=code_assignt(lhs, malloc_expr);
-  t_n->source_location=location;
-
-  // zero-initialize the object
-  dereference_exprt deref(lhs, object_type);
-  exprt zero_object=
-    zero_initializer(object_type, location, ns, get_message_handler());
-  set_class_identifier(
-    to_struct_expr(zero_object), ns, to_symbol_type(object_type));
-  goto_programt::targett t_i=dest.add_instruction(ASSIGN);
-  t_i->code=code_assignt(deref, zero_object);
-  t_i->source_location=location;
-}
-
 void goto_convertt::do_java_new_array(
   const exprt &lhs,
   const side_effect_exprt &rhs,
diff --git a/src/goto-programs/class_identifier.cpp b/src/goto-programs/class_identifier.cpp
index 3e92586e759..44683e847ce 100644
--- a/src/goto-programs/class_identifier.cpp
+++ b/src/goto-programs/class_identifier.cpp
@@ -71,3 +71,39 @@ exprt get_class_identifier_field(
   exprt deref=dereference_exprt(this_expr, this_expr.type().subtype());
   return build_class_identifier(deref, ns);
 }
+
+/// If expr has its components filled in then sets the `@class_identifier`
+/// member of the struct
+/// \remarks Follows through base class members until it gets to the object
+/// type that contains the `@class_identifier` member
+/// \param expr: An expression that represents a struct
+/// \param ns: The namespace used to resolve symbol referencess in the type of
+/// the struct
+/// \param class_type: A symbol whose identifier is the name of the class
+void set_class_identifier(
+  struct_exprt &expr,
+  const namespacet &ns,
+  const symbol_typet &class_type)
+{
+  const struct_typet &struct_type=to_struct_type(ns.follow(expr.type()));
+  const struct_typet::componentst &components=struct_type.components();
+
+  if(components.empty())
+    // Presumably this means the type has not yet been determined
+    return;
+  PRECONDITION(!expr.operands().empty());
+
+  if(components.front().get_name()=="@class_identifier")
+  {
+    INVARIANT(
+      expr.op0().id()==ID_constant, "@class_identifier must be a constant");
+    expr.op0()=constant_exprt(class_type.get_identifier(), string_typet());
+  }
+  else
+  {
+    // The first member must be the base class
+    INVARIANT(
+      expr.op0().id()==ID_struct, "Non @class_identifier must be a structure");
+    set_class_identifier(to_struct_expr(expr.op0()), ns, class_type);
+  }
+}
diff --git a/src/goto-programs/class_identifier.h b/src/goto-programs/class_identifier.h
index ccc679b8e1f..277c99895d2 100644
--- a/src/goto-programs/class_identifier.h
+++ b/src/goto-programs/class_identifier.h
@@ -15,10 +15,16 @@ Author: Chris Smowton, chris.smowton@diffblue.com
 class exprt;
 class namespacet;
 class symbol_typet;
+class struct_exprt;
 
 exprt get_class_identifier_field(
   const exprt &this_expr,
   const symbol_typet &suggested_type,
   const namespacet &ns);
 
+void set_class_identifier(
+  struct_exprt &expr,
+  const namespacet &ns,
+  const symbol_typet &class_type);
+
 #endif
diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp
index 85ffe47a4a4..4234e855cd1 100644
--- a/src/goto-programs/goto_convert.cpp
+++ b/src/goto-programs/goto_convert.cpp
@@ -756,10 +756,7 @@ void goto_convertt::convert_assign(
   else if(rhs.id()==ID_side_effect &&
           rhs.get(ID_statement)==ID_java_new)
   {
-    Forall_operands(it, rhs)
-      clean_expr(*it, dest);
-
-    do_java_new(lhs, to_side_effect_expr(rhs), dest);
+    copy(code, ASSIGN, dest);
   }
   else if(rhs.id()==ID_side_effect &&
           rhs.get(ID_statement)==ID_java_new_array)
diff --git a/src/goto-programs/goto_convert_class.h b/src/goto-programs/goto_convert_class.h
index fe227986a71..21fcd1d0140 100644
--- a/src/goto-programs/goto_convert_class.h
+++ b/src/goto-programs/goto_convert_class.h
@@ -142,11 +142,6 @@ class goto_convertt:public messaget
     const side_effect_exprt &rhs,
     goto_programt &dest);
 
-  void do_java_new(
-    const exprt &lhs,
-    const side_effect_exprt &rhs,
-    goto_programt &dest);
-
   void do_java_new_array(
     const exprt &lhs,
     const side_effect_exprt &rhs,
diff --git a/src/goto-programs/goto_convert_functions.cpp b/src/goto-programs/goto_convert_functions.cpp
index 3efae701a9c..8a4f28c4dd7 100644
--- a/src/goto-programs/goto_convert_functions.cpp
+++ b/src/goto-programs/goto_convert_functions.cpp
@@ -21,10 +21,8 @@ Date: June 2003
 
 goto_convert_functionst::goto_convert_functionst(
   symbol_tablet &_symbol_table,
-  goto_functionst &_functions,
   message_handlert &_message_handler):
-  goto_convertt(_symbol_table, _message_handler),
-  functions(_functions)
+  goto_convertt(_symbol_table, _message_handler)
 {
 }
 
@@ -32,7 +30,7 @@ goto_convert_functionst::~goto_convert_functionst()
 {
 }
 
-void goto_convert_functionst::goto_convert()
+void goto_convert_functionst::goto_convert(goto_functionst &functions)
 {
   // warning! hash-table iterators are not stable
 
@@ -53,7 +51,7 @@ void goto_convert_functionst::goto_convert()
 
   for(const auto &id : symbol_list)
   {
-    convert_function(id);
+    convert_function(id, functions.function_map[id]);
   }
 
   functions.compute_location_numbers();
@@ -135,10 +133,11 @@ void goto_convert_functionst::add_return(
   t->source_location=source_location;
 }
 
-void goto_convert_functionst::convert_function(const irep_idt &identifier)
+void goto_convert_functionst::convert_function(
+  const irep_idt &identifier,
+  goto_functionst::goto_functiont &f)
 {
   const symbolt &symbol=ns.lookup(identifier);
-  goto_functionst::goto_functiont &f=functions.function_map[identifier];
 
   if(f.body_available())
     return; // already converted
@@ -240,12 +239,11 @@ void goto_convert(
   const unsigned errors_before=
     message_handler.get_message_count(messaget::M_ERROR);
 
-  goto_convert_functionst goto_convert_functions(
-    symbol_table, functions, message_handler);
+  goto_convert_functionst goto_convert_functions(symbol_table, message_handler);
 
   try
   {
-    goto_convert_functions.goto_convert();
+    goto_convert_functions.goto_convert(functions);
   }
 
   catch(int)
@@ -276,12 +274,12 @@ void goto_convert(
   const unsigned errors_before=
     message_handler.get_message_count(messaget::M_ERROR);
 
-  goto_convert_functionst goto_convert_functions(
-    symbol_table, functions, message_handler);
+  goto_convert_functionst goto_convert_functions(symbol_table, message_handler);
 
   try
   {
-    goto_convert_functions.convert_function(identifier);
+    goto_convert_functions.convert_function(
+      identifier, functions.function_map[identifier]);
   }
 
   catch(int)
diff --git a/src/goto-programs/goto_convert_functions.h b/src/goto-programs/goto_convert_functions.h
index 3162b453d0f..310d5e3c62c 100644
--- a/src/goto-programs/goto_convert_functions.h
+++ b/src/goto-programs/goto_convert_functions.h
@@ -16,6 +16,7 @@ Date: June 2003
 
 #include "goto_model.h"
 #include "goto_convert_class.h"
+#include "goto_functions.h"
 
 // convert it all!
 void goto_convert(
@@ -38,19 +39,18 @@ void goto_convert(
 class goto_convert_functionst:public goto_convertt
 {
 public:
-  void goto_convert();
-  void convert_function(const irep_idt &identifier);
+  void goto_convert(goto_functionst &functions);
+  void convert_function(
+    const irep_idt &identifier,
+    goto_functionst::goto_functiont &result);
 
   goto_convert_functionst(
     symbol_tablet &_symbol_table,
-    goto_functionst &_functions,
     message_handlert &_message_handler);
 
   virtual ~goto_convert_functionst();
 
 protected:
-  goto_functionst &functions;
-
   static bool hide(const goto_programt &);
 
   //
diff --git a/src/goto-programs/goto_functions_template.h b/src/goto-programs/goto_functions_template.h
index 1a95d670f60..f2551c72483 100644
--- a/src/goto-programs/goto_functions_template.h
+++ b/src/goto-programs/goto_functions_template.h
@@ -121,6 +121,8 @@ class goto_functions_templatet
     return *this;
   }
 
+  void unload(const irep_idt &name) { function_map.erase(name); }
+
   void clear()
   {
     function_map.clear();
diff --git a/src/goto-programs/goto_model.h b/src/goto-programs/goto_model.h
index 2f9c5939bc2..1d819c233ad 100644
--- a/src/goto-programs/goto_model.h
+++ b/src/goto-programs/goto_model.h
@@ -63,6 +63,8 @@ class goto_modelt
     goto_functions=std::move(other.goto_functions);
     return *this;
   }
+
+  void unload(const irep_idt &name) { goto_functions.unload(name); }
 };
 
 #endif // CPROVER_GOTO_PROGRAMS_GOTO_MODEL_H
diff --git a/src/goto-programs/initialize_goto_model.cpp b/src/goto-programs/initialize_goto_model.cpp
index fd3fa158207..13953d721b4 100644
--- a/src/goto-programs/initialize_goto_model.cpp
+++ b/src/goto-programs/initialize_goto_model.cpp
@@ -72,13 +72,7 @@ goto_modelt initialize_goto_model(
         throw 0;
       }
 
-      std::pair<language_filest::file_mapt::iterator, bool>
-        result=language_files.file_map.insert(
-          std::pair<std::string, language_filet>(filename, language_filet()));
-
-      language_filet &lf=result.first->second;
-
-      lf.filename=filename;
+      language_filet &lf=language_files.add_file(filename);
       lf.language=get_language_from_filename(filename);
 
       if(lf.language==nullptr)
@@ -132,10 +126,9 @@ goto_modelt initialize_goto_model(
     // Rebuild the entry-point, using the language annotation of the
     // existing __CPROVER_start function:
     rebuild_goto_start_functiont rebuild_existing_start(
-      msg.get_message_handler(),
       cmdline,
-      goto_model.symbol_table,
-      goto_model.goto_functions);
+      goto_model,
+      msg.get_message_handler());
     entry_point_generation_failed=rebuild_existing_start();
   }
   else if(!binaries_provided_start)
diff --git a/src/goto-programs/lazy_goto_functions_map.h b/src/goto-programs/lazy_goto_functions_map.h
new file mode 100644
index 00000000000..5df717b5088
--- /dev/null
+++ b/src/goto-programs/lazy_goto_functions_map.h
@@ -0,0 +1,144 @@
+// Copyright 2016-2017 Diffblue Limited. All Rights Reserved.
+
+/// \file
+/// A lazy wrapper for goto_functionst.
+
+#ifndef CPROVER_GOTO_PROGRAMS_LAZY_GOTO_FUNCTIONS_MAP_H
+#define CPROVER_GOTO_PROGRAMS_LAZY_GOTO_FUNCTIONS_MAP_H
+
+#include <unordered_set>
+#include "goto_functions.h"
+#include "goto_convert_functions.h"
+#include <util/message.h>
+#include <util/language_file.h>
+
+
+/// Provides a wrapper for a map of lazily loaded goto_functiont.
+/// This incrementally builds a goto-functions object, while permitting
+/// access to goto programs while they are still under construction.
+/// The intended workflow:
+/// 1. The front-end registers the functions that are potentially
+///   available, probably by use of util/language_files.h
+/// 2. The main function registers functions that should be run on
+///   each program, in sequence, after it is converted.
+/// 3. Analyses will then access functions using the `at` function
+/// \tparam bodyt: The type of the function bodies, usually goto_programt
+template<typename bodyt>
+class lazy_goto_functions_mapt final
+{
+public:
+  // NOLINTNEXTLINE(readability/identifiers)  - name matches those used in STL
+  typedef irep_idt key_type;
+  // NOLINTNEXTLINE(readability/identifiers)  - name matches those used in STL
+  typedef goto_function_templatet<bodyt> &mapped_type;
+  /// The type of elements returned by const members
+  // NOLINTNEXTLINE(readability/identifiers)  - name matches mapped_type
+  typedef const goto_function_templatet<bodyt> &const_mapped_type;
+  // NOLINTNEXTLINE(readability/identifiers)  - name matches those used in STL
+  typedef std::pair<const key_type, goto_function_templatet<bodyt>> value_type;
+  // NOLINTNEXTLINE(readability/identifiers)  - name matches those used in STL
+  typedef value_type &reference;
+  // NOLINTNEXTLINE(readability/identifiers)  - name matches those used in STL
+  typedef const value_type &const_reference;
+  // NOLINTNEXTLINE(readability/identifiers)  - name matches those used in STL
+  typedef value_type *pointer;
+  // NOLINTNEXTLINE(readability/identifiers)  - name matches those used in STL
+  typedef const value_type *const_pointer;
+  // NOLINTNEXTLINE(readability/identifiers)  - name matches those used in STL
+  typedef std::size_t size_type;
+
+  typedef
+  std::function<void(goto_functionst::goto_functiont &function)>
+    post_process_functiont;
+
+private:
+  typedef std::map<key_type, goto_function_templatet<bodyt>> underlying_mapt;
+  underlying_mapt &goto_functions;
+  /// Names of functions that are already fully available in the programt state.
+  /// \remarks These functions do not need processing before being returned
+  /// whenever they are requested
+  mutable std::unordered_set<irep_idt, irep_id_hash> processed_functions;
+
+  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;
+
+public:
+  /// Creates a lazy_goto_functions_mapt.
+  lazy_goto_functions_mapt(
+    underlying_mapt &goto_functions,
+    language_filest &language_files,
+    symbol_tablet &symbol_table,
+    post_process_functiont post_process_function,
+    message_handlert &message_handler)
+  : 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))
+  {
+  }
+
+  /// Gets the body for a given function.
+  /// \param name: The name of the function to search for.
+  /// \return The function body corresponding to the given function.
+  const_mapped_type at(const key_type &name) const
+  {
+    return ensure_function_loaded_internal(name).second;
+  }
+
+  /// Gets the body for a given function.
+  /// \param name: The name of the function to search for.
+  /// \return The function body corresponding to the given function.
+  mapped_type at(const key_type &name)
+  {
+    return ensure_function_loaded_internal(name).second;
+  }
+
+  void unload(const key_type &name) const { goto_functions.erase(name); }
+
+  void ensure_function_loaded(const key_type &name) const
+  {
+    ensure_function_loaded_internal(name);
+  }
+
+private:
+  // This returns a non-const reference, but if you use this method from a
+  // const method then you should not return such a reference without making it
+  // const first
+  reference ensure_function_loaded_internal(const key_type &name) const
+  {
+    reference named_function=ensure_entry_converted(name);
+    mapped_type function=named_function.second;
+    if(processed_functions.count(name)==0)
+    {
+      // Run function-pass conversions
+      post_process_function(function);
+      // Assign procedure-local location numbers for now
+      function.body.compute_location_numbers();
+      processed_functions.insert(name);
+    }
+    return named_function;
+  }
+
+  reference ensure_entry_converted(const key_type &name) 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);
+    // Create goto_functiont
+    goto_functionst::goto_functiont function;
+    convert_functions.convert_function(name, function);
+    // Add to map
+    return *goto_functions.emplace(name, std::move(function)).first;
+  }
+};
+
+#endif  // CPROVER_GOTO_PROGRAMS_LAZY_GOTO_FUNCTIONS_MAP_H
diff --git a/src/goto-programs/lazy_goto_model.cpp b/src/goto-programs/lazy_goto_model.cpp
new file mode 100644
index 00000000000..bc6c52a6f55
--- /dev/null
+++ b/src/goto-programs/lazy_goto_model.cpp
@@ -0,0 +1,239 @@
+// Copyright 2017 Diffblue Limited. All Rights Reserved.
+
+/// \file
+/// Model for lazy loading of functions
+
+#include "lazy_goto_model.h"
+#include "read_goto_binary.h"
+#include "rebuild_goto_start_function.h"
+
+#include <langapi/mode.h>
+
+#include <util/cmdline.h>
+#include <util/config.h>
+#include <util/journalling_symbol_table.h>
+#include <util/language.h>
+#include <util/unicode.h>
+
+#include <fstream>
+
+//! @cond Doxygen_suppress_Lambda_in_initializer_list
+lazy_goto_modelt::lazy_goto_modelt(
+  post_process_functiont post_process_function,
+  post_process_functionst post_process_functions,
+  message_handlert &message_handler)
+  : goto_model(new goto_modelt()),
+    symbol_table(goto_model->symbol_table),
+    goto_functions(
+      goto_model->goto_functions.function_map,
+      language_files,
+      symbol_table,
+      [this] (goto_functionst::goto_functiont &function) -> void
+      {
+        this->post_process_function(function, symbol_table);
+      },
+      message_handler),
+    post_process_function(std::move(post_process_function)),
+    post_process_functions(std::move(post_process_functions)),
+    message_handler(message_handler)
+{
+  language_files.set_message_handler(message_handler);
+}
+
+lazy_goto_modelt::lazy_goto_modelt(lazy_goto_modelt &&other)
+  : goto_model(std::move(other.goto_model)),
+    symbol_table(goto_model->symbol_table),
+    goto_functions(
+      goto_model->goto_functions.function_map,
+      language_files,
+      symbol_table,
+      [this] (goto_functionst::goto_functiont &function) -> void
+      {
+        this->post_process_function(function, symbol_table);
+      },
+      other.message_handler),
+    language_files(std::move(other.language_files)),
+    post_process_function(std::move(other.post_process_function)),
+    post_process_functions(std::move(other.post_process_functions)),
+    message_handler(other.message_handler)
+{
+}
+//! @endcond
+
+void lazy_goto_modelt::initialize(const cmdlinet &cmdline)
+{
+  messaget msg(message_handler);
+
+  const std::vector<std::string> &files=cmdline.args;
+  if(files.empty())
+  {
+    msg.error() << "Please provide a program" << messaget::eom;
+    throw 0;
+  }
+
+  std::vector<std::string> binaries, sources;
+  binaries.reserve(files.size());
+  sources.reserve(files.size());
+
+  for(const auto &file : files)
+  {
+    if(is_goto_binary(file))
+      binaries.push_back(file);
+    else
+      sources.push_back(file);
+  }
+
+  if(!sources.empty())
+  {
+    for(const auto &filename : sources)
+    {
+#ifdef _MSC_VER
+      std::ifstream infile(widen(filename));
+#else
+      std::ifstream infile(filename);
+#endif
+
+      if(!infile)
+      {
+        msg.error() << "failed to open input file `" << filename
+                    << '\'' << messaget::eom;
+        throw 0;
+      }
+
+      language_filet &lf=add_language_file(filename);
+      lf.language=get_language_from_filename(filename);
+
+      if(lf.language==nullptr)
+      {
+        source_locationt location;
+        location.set_file(filename);
+        msg.error().source_location=location;
+        msg.error() << "failed to figure out type of file" << messaget::eom;
+        throw 0;
+      }
+
+      languaget &language=*lf.language;
+      language.set_message_handler(message_handler);
+      language.get_language_options(cmdline);
+
+      msg.status() << "Parsing " << filename << messaget::eom;
+
+      if(language.parse(infile, filename))
+      {
+        msg.error() << "PARSING ERROR" << messaget::eom;
+        throw 0;
+      }
+
+      lf.get_modules();
+    }
+
+    msg.status() << "Converting" << messaget::eom;
+
+    if(language_files.typecheck(symbol_table))
+    {
+      msg.error() << "CONVERSION ERROR" << messaget::eom;
+      throw 0;
+    }
+  }
+
+  for(const std::string &file : binaries)
+  {
+    msg.status() << "Reading GOTO program from file" << messaget::eom;
+
+    if(read_object_and_link(file, *goto_model, message_handler))
+      throw 0;
+  }
+
+  bool binaries_provided_start =
+    symbol_table.has_symbol(goto_functionst::entry_point());
+
+  bool entry_point_generation_failed=false;
+
+  if(binaries_provided_start && cmdline.isset("function"))
+  {
+    // Rebuild the entry-point, using the language annotation of the
+    // existing __CPROVER_start function:
+    rebuild_lazy_goto_start_functiont rebuild_existing_start(
+      cmdline, *this, message_handler);
+    entry_point_generation_failed=rebuild_existing_start();
+  }
+  else if(!binaries_provided_start)
+  {
+    // Unsure of the rationale for only generating stubs when there are no
+    // GOTO binaries in play; simply mirroring old code in language_uit here.
+    if(binaries.empty())
+    {
+      // Enable/disable stub generation for opaque methods
+      bool stubs_enabled=cmdline.isset("generate-opaque-stubs");
+      language_files.set_should_generate_opaque_method_stubs(stubs_enabled);
+    }
+
+    // Allow all language front-ends to try to provide the user-specified
+    // (--function) entry-point, or some language-specific default:
+    entry_point_generation_failed=
+      language_files.generate_support_functions(symbol_table);
+  }
+
+  if(entry_point_generation_failed)
+  {
+    msg.error() << "SUPPORT FUNCTION GENERATION ERROR" << messaget::eom;
+    throw 0;
+  }
+
+  // stupid hack
+  config.set_object_bits_from_symbol_table(symbol_table);
+}
+
+/// Eagerly loads all functions from the symbol table.
+void lazy_goto_modelt::load_all_functions() const
+{
+  symbol_tablet::symbolst::size_type table_size;
+  symbol_tablet::symbolst::size_type new_table_size=symbol_table.symbols.size();
+  do
+  {
+    table_size=new_table_size;
+
+    // Find symbols that correspond to functions
+    std::vector<irep_idt> fn_ids_to_convert;
+    for(const auto &named_symbol : symbol_table.symbols)
+    {
+      if(named_symbol.second.is_function())
+        fn_ids_to_convert.push_back(named_symbol.first);
+    }
+
+    for(const irep_idt &symbol_name : fn_ids_to_convert)
+      goto_functions.ensure_function_loaded(symbol_name);
+
+    // Repeat while new symbols are being added in case any of those are
+    // stubbed functions. Even stubs can create new stubs while being
+    // converted if they are special stubs (e.g. string functions)
+    new_table_size=symbol_table.symbols.size();
+  } while(new_table_size!=table_size);
+
+  goto_model->goto_functions.compute_location_numbers();
+}
+
+bool lazy_goto_modelt::finalize()
+{
+  messaget msg(message_handler);
+  journalling_symbol_tablet symbol_table=
+    journalling_symbol_tablet::wrap(this->symbol_table);
+  if(language_files.final(symbol_table))
+  {
+    msg.error() << "CONVERSION ERROR" << messaget::eom;
+    return true;
+  }
+  for(const irep_idt &updated_symbol_id : symbol_table.get_updated())
+  {
+    if(symbol_table.lookup_ref(updated_symbol_id).is_function())
+    {
+      // Re-convert any that already exist
+      goto_functions.unload(updated_symbol_id);
+      goto_functions.ensure_function_loaded(updated_symbol_id);
+    }
+  }
+
+  language_files.clear();
+
+  return post_process_functions(*goto_model);
+}
diff --git a/src/goto-programs/lazy_goto_model.h b/src/goto-programs/lazy_goto_model.h
new file mode 100644
index 00000000000..1d91891638d
--- /dev/null
+++ b/src/goto-programs/lazy_goto_model.h
@@ -0,0 +1,116 @@
+// Copyright 2016-2017 Diffblue Limited. All Rights Reserved.
+
+/// \file
+/// Model for lazy loading of functions
+
+#ifndef CPROVER_GOTO_PROGRAMS_LAZY_GOTO_MODEL_H
+#define CPROVER_GOTO_PROGRAMS_LAZY_GOTO_MODEL_H
+
+#include <util/language_file.h>
+
+#include "goto_model.h"
+#include "lazy_goto_functions_map.h"
+#include "goto_convert_functions.h"
+
+class cmdlinet;
+class optionst;
+
+
+/// Model that holds partially loaded map of functions
+class lazy_goto_modelt
+{
+public:
+  typedef std::function<void(
+    goto_functionst::goto_functiont &function,
+    symbol_tablet &symbol_table)> post_process_functiont;
+  typedef std::function<bool(goto_modelt &goto_model)> post_process_functionst;
+
+  explicit lazy_goto_modelt(
+    post_process_functiont post_process_function,
+    post_process_functionst post_process_functions,
+    message_handlert &message_handler);
+
+  lazy_goto_modelt(lazy_goto_modelt &&other);
+
+  lazy_goto_modelt &operator=(lazy_goto_modelt &&other)
+  {
+    goto_model = std::move(other.goto_model);
+    language_files = std::move(other.language_files);
+    return *this;
+  }
+
+  /// Create a lazy_goto_modelt from a object that defines function/module pass
+  /// handlers
+  /// \param handler: An object that defines the handlers
+  /// \param options: The options passed to process_goto_functions
+  /// \param message_handler: The message_handler to use for logging
+  /// \tparam THandler a type that defines methods process_goto_function and
+  /// process_goto_functions
+  template<typename THandler>
+  static lazy_goto_modelt from_handler_object(
+    THandler &handler,
+    const optionst &options,
+    message_handlert &message_handler)
+  {
+    return lazy_goto_modelt(
+      [&handler] (
+        goto_functionst::goto_functiont &function,
+        symbol_tablet &symbol_table) -> void
+      {
+        handler.process_goto_function(function, symbol_table);
+      },
+      [&handler, &options] (goto_modelt &goto_model) -> bool
+      {
+        return handler.process_goto_functions(goto_model, options);
+      },
+      message_handler);
+  }
+
+  void initialize(const cmdlinet &cmdline);
+
+  /// Eagerly loads all functions from the symbol table.
+  void load_all_functions() const;
+
+  void unload(const irep_idt &name) const { goto_functions.unload(name); }
+
+  language_filet &add_language_file(const std::string &filename)
+  {
+    return language_files.add_file(filename);
+  }
+
+  /// The model returned here has access to the functions we've already
+  /// loaded but is frozen in the sense that, with regard to the facility to
+  /// load new functions, it has let it go.
+  /// Before freezing the functions all module-level passes are run
+  /// \param model: The lazy_goto_modelt to freeze
+  /// \returns The frozen goto_modelt or an empty optional if freezing fails
+  static std::unique_ptr<goto_modelt> process_whole_model_and_freeze(
+    lazy_goto_modelt &&model)
+  {
+    if(model.finalize())
+      return nullptr;
+    return std::move(model.goto_model);
+  }
+
+private:
+  std::unique_ptr<goto_modelt> goto_model;
+
+public:
+  /// Reference to symbol_table in the internal goto_model
+  symbol_tablet &symbol_table;
+
+private:
+  const lazy_goto_functions_mapt<goto_programt> goto_functions;
+  language_filest language_files;
+
+  // Function/module processing functions
+  const post_process_functiont post_process_function;
+  const post_process_functionst post_process_functions;
+
+  /// Logging helper field
+  message_handlert &message_handler;
+
+  bool finalize();
+};
+
+#endif // CPROVER_GOTO_PROGRAMS_LAZY_GOTO_MODEL_H
diff --git a/src/goto-programs/rebuild_goto_start_function.cpp b/src/goto-programs/rebuild_goto_start_function.cpp
index 230490318dc..8621ff4a44c 100644
--- a/src/goto-programs/rebuild_goto_start_function.cpp
+++ b/src/goto-programs/rebuild_goto_start_function.cpp
@@ -8,7 +8,6 @@
 
 #include "rebuild_goto_start_function.h"
 
-#include <goto-programs/goto_functions.h>
 #include <util/language.h>
 #include <util/symbol.h>
 #include <util/symbol_table.h>
@@ -17,22 +16,21 @@
 #include <langapi/mode.h>
 #include <memory>
 
-/// To rebuild the _start funciton in the event the program was compiled into
+/// To rebuild the _start function in the event the program was compiled into
 /// GOTO with a different entry function selected.
+/// \param goto_model: The goto functions (to replace the body of the _start
+///   function) and symbol table (to replace the _start function symbol) of the
+///   program.
 /// \param _message_handler: The message handler to report any messages with
-/// \param symbol_table: The symbol table of the program (to replace the _start
-///   functions symbo)
-/// \param goto_functions: The goto functions of the program (to replace the
-///   body of the _start function).
-rebuild_goto_start_functiont::rebuild_goto_start_functiont(
-  message_handlert &_message_handler,
+template<typename maybe_lazy_goto_modelt>
+rebuild_goto_start_function_baset<maybe_lazy_goto_modelt>::
+rebuild_goto_start_function_baset(
   const cmdlinet &cmdline,
-  symbol_tablet &symbol_table,
-  goto_functionst &goto_functions):
-    messaget(_message_handler),
+  maybe_lazy_goto_modelt &goto_model,
+  message_handlert &message_handler):
+    messaget(message_handler),
     cmdline(cmdline),
-    symbol_table(symbol_table),
-    goto_functions(goto_functions)
+    goto_model(goto_model)
 {
 }
 
@@ -44,7 +42,8 @@ rebuild_goto_start_functiont::rebuild_goto_start_functiont(
 /// called from _start
 /// \return Returns true if either the symbol is not found, or something went
 ///   wrong with generating the start_function. False otherwise.
-bool rebuild_goto_start_functiont::operator()()
+template<typename maybe_lazy_goto_modelt>
+bool rebuild_goto_start_function_baset<maybe_lazy_goto_modelt>::operator()()
 {
   const irep_idt &mode=get_entry_point_mode();
 
@@ -58,19 +57,12 @@ bool rebuild_goto_start_functiont::operator()()
   remove_existing_entry_point();
 
   bool return_code=
-    language->generate_support_functions(symbol_table);
+    language->generate_support_functions(goto_model.symbol_table);
 
-  // Remove the function from the goto_functions so it is copied back in
+  // Remove the function from the goto functions so it is copied back in
   // from the symbol table during goto_convert
   if(!return_code)
-  {
-    const auto &start_function=
-      goto_functions.function_map.find(goto_functionst::entry_point());
-    if(start_function!=goto_functions.function_map.end())
-    {
-      goto_functions.function_map.erase(start_function);
-    }
-  }
+    goto_model.unload(goto_functionst::entry_point());
 
   return return_code;
 }
@@ -78,23 +70,27 @@ bool rebuild_goto_start_functiont::operator()()
 /// Find out the mode of the current entry point to determine the mode of the
 /// replacement entry point
 /// \return A mode string saying which language to use
-irep_idt rebuild_goto_start_functiont::get_entry_point_mode() const
+template<typename maybe_lazy_goto_modelt>
+irep_idt rebuild_goto_start_function_baset<maybe_lazy_goto_modelt>::
+get_entry_point_mode() const
 {
   const symbolt &current_entry_point=
-    *symbol_table.lookup(goto_functionst::entry_point());
+    *goto_model.symbol_table.lookup(goto_functionst::entry_point());
   return current_entry_point.mode;
 }
 
 /// Eliminate the existing entry point function symbol and any symbols created
 /// in that scope from the symbol table.
-void rebuild_goto_start_functiont::remove_existing_entry_point()
+template<typename maybe_lazy_goto_modelt>
+void rebuild_goto_start_function_baset<maybe_lazy_goto_modelt>::
+remove_existing_entry_point()
 {
   // Remove the function itself
-  symbol_table.remove(goto_functionst::entry_point());
+  goto_model.symbol_table.remove(goto_functionst::entry_point());
 
   // And any symbols created in the scope of the entry point
   std::vector<irep_idt> entry_point_symbols;
-  for(const auto &symbol_entry : symbol_table.symbols)
+  for(const auto &symbol_entry : goto_model.symbol_table.symbols)
   {
     const bool is_entry_point_symbol=
       has_prefix(
@@ -107,6 +103,9 @@ void rebuild_goto_start_functiont::remove_existing_entry_point()
 
   for(const irep_idt &entry_point_symbol : entry_point_symbols)
   {
-    symbol_table.remove(entry_point_symbol);
+    goto_model.symbol_table.remove(entry_point_symbol);
   }
 }
+
+template class rebuild_goto_start_function_baset<goto_modelt>;
+template class rebuild_goto_start_function_baset<lazy_goto_modelt>;
diff --git a/src/goto-programs/rebuild_goto_start_function.h b/src/goto-programs/rebuild_goto_start_function.h
index 15516389fc4..8d5ad9f8fbe 100644
--- a/src/goto-programs/rebuild_goto_start_function.h
+++ b/src/goto-programs/rebuild_goto_start_function.h
@@ -12,6 +12,9 @@
 #include <util/message.h>
 class cmdlinet;
 
+#include "lazy_goto_model.h"
+
+
 class symbol_tablet;
 class goto_functionst;
 
@@ -21,14 +24,14 @@ class goto_functionst;
 #define HELP_FUNCTIONS \
   " --function name              set main function name\n"
 
-class rebuild_goto_start_functiont: public messaget
+template<typename maybe_lazy_goto_modelt>
+class rebuild_goto_start_function_baset: public messaget
 {
 public:
-  rebuild_goto_start_functiont(
-    message_handlert &_message_handler,
+  rebuild_goto_start_function_baset(
     const cmdlinet &cmdline,
-    symbol_tablet &symbol_table,
-    goto_functionst &goto_functions);
+    maybe_lazy_goto_modelt &goto_model,
+    message_handlert &message_handler);
 
   bool operator()();
 
@@ -38,8 +41,15 @@ class rebuild_goto_start_functiont: public messaget
   void remove_existing_entry_point();
 
   const cmdlinet &cmdline;
-  symbol_tablet &symbol_table;
-  goto_functionst &goto_functions;
+  maybe_lazy_goto_modelt &goto_model;
 };
 
+// NOLINTNEXTLINE(readability/namespace)  using required for templates
+using rebuild_goto_start_functiont =
+  rebuild_goto_start_function_baset<goto_modelt>;
+
+// NOLINTNEXTLINE(readability/namespace)  using required for templates
+using rebuild_lazy_goto_start_functiont =
+  rebuild_goto_start_function_baset<lazy_goto_modelt>;
+
 #endif // CPROVER_GOTO_PROGRAMS_REBUILD_GOTO_START_FUNCTION_H
diff --git a/src/goto-programs/remove_asm.cpp b/src/goto-programs/remove_asm.cpp
index 29958434d48..98af6d6867c 100644
--- a/src/goto-programs/remove_asm.cpp
+++ b/src/goto-programs/remove_asm.cpp
@@ -25,27 +25,20 @@ Date:   December 2014
 class remove_asmt
 {
 public:
-  inline remove_asmt(
-    symbol_tablet &_symbol_table,
-    goto_functionst &_goto_functions):
-    symbol_table(_symbol_table),
-    goto_functions(_goto_functions)
+  explicit remove_asmt(symbol_tablet &_symbol_table)
+    : symbol_table(_symbol_table)
   {
   }
 
-  void operator()();
+  void process_function(goto_functionst::goto_functiont &);
 
 protected:
   symbol_tablet &symbol_table;
-  goto_functionst &goto_functions;
 
   void process_instruction(
     goto_programt::instructiont &instruction,
     goto_programt &dest);
 
-  void process_function(
-    goto_functionst::goto_functiont &);
-
   void gcc_asm_function_call(
     const irep_idt &function_base_name,
     const codet &code,
@@ -305,24 +298,24 @@ void remove_asmt::process_function(
 }
 
 /// removes assembler
-void remove_asmt::operator()()
+void remove_asm(
+  goto_functionst::goto_functiont &goto_function,
+  symbol_tablet &symbol_table)
 {
-  Forall_goto_functions(it, goto_functions)
-  {
-    process_function(it->second);
-  }
+  remove_asmt rem(symbol_table);
+  rem.process_function(goto_function);
 }
 
 /// removes assembler
-void remove_asm(
-  symbol_tablet &symbol_table,
-  goto_functionst &goto_functions)
+void remove_asm(goto_functionst &goto_functions, symbol_tablet &symbol_table)
 {
-  remove_asmt(symbol_table, goto_functions)();
+  remove_asmt rem(symbol_table);
+  for(auto &f : goto_functions.function_map)
+    rem.process_function(f.second);
 }
 
 /// removes assembler
 void remove_asm(goto_modelt &goto_model)
 {
-  remove_asmt(goto_model.symbol_table, goto_model.goto_functions)();
+  remove_asm(goto_model.goto_functions, goto_model.symbol_table);
 }
diff --git a/src/goto-programs/remove_asm.h b/src/goto-programs/remove_asm.h
index 7717ba59ca0..913fe85c336 100644
--- a/src/goto-programs/remove_asm.h
+++ b/src/goto-programs/remove_asm.h
@@ -17,8 +17,12 @@ Date:   December 2014
 
 #include <goto-programs/goto_model.h>
 
-void remove_asm(symbol_tablet &, goto_functionst &);
+void remove_asm(
+  goto_functionst::goto_functiont &goto_function,
+  symbol_tablet &symbol_table);
 
-void remove_asm(goto_modelt &);
+void remove_asm(goto_functionst &goto_functions, symbol_tablet &symbol_table);
+
+void remove_asm(goto_modelt &goto_model);
 
 #endif // CPROVER_GOTO_PROGRAMS_REMOVE_ASM_H
diff --git a/src/goto-programs/remove_instanceof.cpp b/src/goto-programs/remove_instanceof.cpp
index 69db2a8859e..6d8a8de329b 100644
--- a/src/goto-programs/remove_instanceof.cpp
+++ b/src/goto-programs/remove_instanceof.cpp
@@ -22,26 +22,19 @@ Author: Chris Smowton, chris.smowton@diffblue.com
 class remove_instanceoft
 {
 public:
-  remove_instanceoft(
-    symbol_tablet &_symbol_table,
-    goto_functionst &_goto_functions):
-    symbol_table(_symbol_table),
-    ns(_symbol_table),
-    goto_functions(_goto_functions)
+  explicit remove_instanceoft(symbol_tablet &symbol_table)
+  : symbol_table(symbol_table), ns(symbol_table)
   {
-    class_hierarchy(_symbol_table);
+    class_hierarchy(symbol_table);
   }
 
-  // Lower instanceof for all functions:
-  void lower_instanceof();
+  // Lower instanceof for a single functions
+  bool lower_instanceof(goto_programt &);
 
 protected:
   symbol_tablet &symbol_table;
   namespacet ns;
   class_hierarchyt class_hierarchy;
-  goto_functionst &goto_functions;
-
-  bool lower_instanceof(goto_programt &);
 
   bool lower_instanceof(goto_programt &, goto_programt::targett);
 
@@ -174,33 +167,38 @@ bool remove_instanceoft::lower_instanceof(goto_programt &goto_program)
   return true;
 }
 
-/// See function above
-/// \return Side-effects on this->goto_functions, replacing every instanceof in
-///   every function with an explicit test.
-void remove_instanceoft::lower_instanceof()
+
+/// Replace every instanceof in the passed function with an explicit
+/// class-identifier test.
+/// Extra auxiliary variables may be introduced into symbol_table.
+/// \param function: The function to work on.
+/// \param symbol_table: The symbol table to add symbols to.
+void remove_instanceof(
+  goto_functionst::goto_functiont &function,
+  symbol_tablet &symbol_table)
 {
-  bool changed=false;
-  for(auto &f : goto_functions.function_map)
-    changed=(lower_instanceof(f.second.body) || changed);
-  if(changed)
-    goto_functions.compute_location_numbers();
+  remove_instanceoft rem(symbol_table);
+  rem.lower_instanceof(function.body);
 }
 
-/// See function above
-/// \par parameters: `goto_functions`, a function map, and the corresponding
-/// `symbol_table`.
-/// \return Side-effects on goto_functions, replacing every instanceof in every
-///   function with an explicit test. Extra auxiliary variables may be
-///   introduced into `symbol_table`.
+/// Replace every instanceof in every function with an explicit
+/// class-identifier test.
+/// Extra auxiliary variables may be introduced into symbol_table.
+/// \param goto_functions: The functions to work on.
+/// \param symbol_table: The symbol table to add symbols to.
 void remove_instanceof(
-  symbol_tablet &symbol_table,
-  goto_functionst &goto_functions)
+  goto_functionst &goto_functions,
+  symbol_tablet &symbol_table)
 {
-  remove_instanceoft rem(symbol_table, goto_functions);
-  rem.lower_instanceof();
+  remove_instanceoft rem(symbol_table);
+  bool changed=false;
+  for(auto &f : goto_functions.function_map)
+    changed=rem.lower_instanceof(f.second.body) || changed;
+  if(changed)
+    goto_functions.compute_location_numbers();
 }
 
 void remove_instanceof(goto_modelt &goto_model)
 {
-  remove_instanceof(goto_model.symbol_table, goto_model.goto_functions);
+  remove_instanceof(goto_model.goto_functions, goto_model.symbol_table);
 }
diff --git a/src/goto-programs/remove_instanceof.h b/src/goto-programs/remove_instanceof.h
index 15a02bf35b2..509b0157282 100644
--- a/src/goto-programs/remove_instanceof.h
+++ b/src/goto-programs/remove_instanceof.h
@@ -17,8 +17,12 @@ Author: Chris Smowton, chris.smowton@diffblue.com
 #include "goto_model.h"
 
 void remove_instanceof(
-  symbol_tablet &symbol_table,
-  goto_functionst &goto_functions);
+  goto_functionst::goto_functiont &function,
+  symbol_tablet &symbol_table);
+
+void remove_instanceof(
+  goto_functionst &goto_functions,
+  symbol_tablet &symbol_table);
 
 void remove_instanceof(goto_modelt &model);
 
diff --git a/src/goto-programs/remove_java_new.cpp b/src/goto-programs/remove_java_new.cpp
new file mode 100644
index 00000000000..b7059bbadff
--- /dev/null
+++ b/src/goto-programs/remove_java_new.cpp
@@ -0,0 +1,105 @@
+// Copyright 2017 Diffblue Limited. All Rights Reserved.
+
+/// \file
+/// Function-level/module-level pass to remove java_new and replace with
+/// malloc & zero-initialize
+
+#include "remove_java_new.h"
+
+#include <util/message.h>
+#include <util/pointer_offset_size.h>
+#include <linking/zero_initializer.h>
+
+#include "class_identifier.h"
+
+static bool remove_java_new(
+  goto_programt &goto_program,
+  const namespacet &ns,
+  message_handlert &message_handler)
+{
+  messaget msg(message_handler);
+
+  bool changed=false;
+  for(goto_programt::targett target=goto_program.instructions.begin();
+    target!=goto_program.instructions.end();
+    ++target)
+  {
+    code_assignt *assign=expr_try_dynamic_cast<code_assignt>(target->code);
+    if(assign==nullptr)
+      continue;
+    side_effect_exprt *rhs=
+      expr_try_dynamic_cast<side_effect_exprt>(assign->rhs());
+    if(rhs==nullptr)
+      continue;
+    if(rhs->get_statement()!=ID_java_new)
+      continue;
+    INVARIANT(rhs->operands().empty(), "java_new does not have operands");
+    INVARIANT(rhs->type().id()==ID_pointer, "java_new returns pointer");
+
+    const exprt &lhs=assign->lhs();
+    INVARIANT(
+      !lhs.is_nil(), "remove_java_new without lhs is yet to be implemented");
+
+    typet object_type=rhs->type().subtype();
+
+    // build size expression
+    exprt object_size=size_of_expr(object_type, ns);
+    CHECK_RETURN(object_size.is_not_nil());
+
+    changed=true;
+
+    source_locationt location=rhs->source_location();
+
+    // We produce a malloc side-effect
+    side_effect_exprt malloc_expr(ID_allocate);
+    malloc_expr.copy_to_operands(object_size);
+    // could use true and get rid of the code below
+    malloc_expr.copy_to_operands(false_exprt());
+    malloc_expr.type()=rhs->type();
+    *rhs=std::move(malloc_expr);
+
+    // zero-initialize the object
+    dereference_exprt deref(lhs, object_type);
+    exprt zero_object=
+      zero_initializer(object_type, location, ns, message_handler);
+    set_class_identifier(
+      expr_dynamic_cast<struct_exprt>(zero_object),
+      ns,
+      to_symbol_type(object_type));
+    goto_programt::targett zi_assign=goto_program.insert_after(target);
+    zi_assign->make_assignment();
+    zi_assign->code=code_assignt(deref, zero_object);
+    zi_assign->source_location=location;
+  }
+  if(!changed)
+    return false;
+  goto_program.update();
+  return true;
+}
+
+bool remove_java_new(
+  goto_functionst::goto_functiont &goto_function,
+  const namespacet &ns,
+  message_handlert &message_handler)
+{
+  return remove_java_new(goto_function.body, ns, message_handler);
+}
+
+void remove_java_new(
+  goto_functionst &goto_functions,
+  const namespacet &ns,
+  message_handlert &message_handler)
+{
+  for(auto &named_fn : goto_functions.function_map)
+    remove_java_new(named_fn.second, ns, message_handler);
+}
+
+void remove_java_new(
+  goto_modelt &goto_model,
+  message_handlert &message_handler)
+{
+  remove_java_new(
+    goto_model.goto_functions,
+    namespacet(goto_model.symbol_table),
+    message_handler);
+}
diff --git a/src/goto-programs/remove_java_new.h b/src/goto-programs/remove_java_new.h
new file mode 100644
index 00000000000..99263203a0f
--- /dev/null
+++ b/src/goto-programs/remove_java_new.h
@@ -0,0 +1,29 @@
+// Copyright 2017 Diffblue Limited. All Rights Reserved.
+
+/// \file
+/// Function-level/module-level pass to remove java_new and replace with
+/// malloc & zero-initialize
+
+#ifndef CPROVER_GOTO_PROGRAMS_REMOVE_JAVA_NEW_H
+#define CPROVER_GOTO_PROGRAMS_REMOVE_JAVA_NEW_H
+
+#include "goto_model.h"
+
+class message_handlert;
+
+
+bool remove_java_new(
+  goto_functionst::goto_functiont &goto_function,
+  const namespacet &ns,
+  message_handlert &message_handler);
+
+void remove_java_new(
+  goto_functionst &goto_functions,
+  const namespacet &ns,
+  message_handlert &message_handler);
+
+void remove_java_new(
+  goto_modelt &goto_model,
+  message_handlert &message_handler);
+
+#endif // CPROVER_GOTO_PROGRAMS_REMOVE_JAVA_NEW_H
diff --git a/src/goto-symex/adjust_float_expressions.cpp b/src/goto-symex/adjust_float_expressions.cpp
index f2b09db09ec..89abaf65757 100644
--- a/src/goto-symex/adjust_float_expressions.cpp
+++ b/src/goto-symex/adjust_float_expressions.cpp
@@ -179,7 +179,7 @@ void adjust_float_expressions(
   }
 }
 
-static void adjust_float_expressions(
+void adjust_float_expressions(
   goto_functionst::goto_functiont &goto_function,
   const namespacet &ns)
 {
diff --git a/src/goto-symex/adjust_float_expressions.h b/src/goto-symex/adjust_float_expressions.h
index 5cfd01d740f..bd011641d54 100644
--- a/src/goto-symex/adjust_float_expressions.h
+++ b/src/goto-symex/adjust_float_expressions.h
@@ -12,15 +12,20 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_GOTO_SYMEX_ADJUST_FLOAT_EXPRESSIONS_H
 #define CPROVER_GOTO_SYMEX_ADJUST_FLOAT_EXPRESSIONS_H
 
+#include <goto-programs/goto_functions.h>
+
 class exprt;
 class namespacet;
-class goto_functionst;
 class goto_modelt;
 
 void adjust_float_expressions(
   exprt &expr,
   const namespacet &ns);
 
+void adjust_float_expressions(
+  goto_functionst::goto_functiont &goto_function,
+  const namespacet &ns);
+
 void adjust_float_expressions(
   goto_functionst &goto_functions,
   const namespacet &ns);
diff --git a/src/goto-symex/rewrite_union.cpp b/src/goto-symex/rewrite_union.cpp
index e033188da4b..61cd69ee49b 100644
--- a/src/goto-symex/rewrite_union.cpp
+++ b/src/goto-symex/rewrite_union.cpp
@@ -107,7 +107,7 @@ void rewrite_union(
   }
 }
 
-static void rewrite_union(
+void rewrite_union(
   goto_functionst::goto_functiont &goto_function,
   const namespacet &ns)
 {
diff --git a/src/goto-symex/rewrite_union.h b/src/goto-symex/rewrite_union.h
index d2c9b1772b4..379e47c6b4d 100644
--- a/src/goto-symex/rewrite_union.h
+++ b/src/goto-symex/rewrite_union.h
@@ -23,6 +23,10 @@ void rewrite_union(
   exprt &expr,
   const namespacet &ns);
 
+void rewrite_union(
+  goto_functionst::goto_functiont &goto_function,
+  const namespacet &ns);
+
 void rewrite_union(
   goto_functionst &goto_functions,
   const namespacet &ns);
diff --git a/src/java_bytecode/ci_lazy_methods.cpp b/src/java_bytecode/ci_lazy_methods.cpp
index 4c108ba51b0..dd434acb372 100644
--- a/src/java_bytecode/ci_lazy_methods.cpp
+++ b/src/java_bytecode/ci_lazy_methods.cpp
@@ -73,7 +73,7 @@ bool ci_lazy_methodst::operator()(
   std::vector<irep_idt> method_worklist2;
 
   main_function_resultt main_function =
-    get_main_symbol(symbol_table, main_class, get_message_handler(), true);
+    get_main_symbol(symbol_table, main_class, get_message_handler());
   if(!main_function.is_success())
   {
     // Failed, mark all functions in the given main class(es)
diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp
index ac6bceab861..fb9b18bd871 100644
--- a/src/java_bytecode/java_bytecode_convert_method.cpp
+++ b/src/java_bytecode/java_bytecode_convert_method.cpp
@@ -382,11 +382,11 @@ void java_bytecode_convert_methodt::convert(
     id2string(class_symbol.name)+"."+id2string(m.name)+":"+m.descriptor;
   method_id=method_identifier;
 
-  const symbolt &old_sym=*symbol_table.lookup(method_identifier);
+  symbolt &method_symbol=*symbol_table.get_writeable(method_identifier);
 
   // Obtain a std::vector of code_typet::parametert objects from the
   // (function) type of the symbol
-  typet member_type=old_sym.type;
+  typet member_type=method_symbol.type;
   code_typet &code_type=to_code_type(member_type);
   method_return_type=code_type.return_type();
   code_typet::parameterst &parameters=code_type.parameters();
@@ -527,10 +527,17 @@ void java_bytecode_convert_methodt::convert(
   if(is_constructor(method))
     method.set(ID_constructor, true);
 
-  // we add the symbol for the method
-  symbolt method_symbol;
-  method_symbol.name=method.get_name();
-  method_symbol.base_name=method.get_base_name();
+  // Check the fields that can't change are valid
+  INVARIANT(
+    method_symbol.name==method.get_name(),
+    "Name of method symbol shouldn't change");
+  INVARIANT(
+    method_symbol.base_name==method.get_base_name(),
+    "Base name of method symbol shouldn't change");
+  INVARIANT(
+    method_symbol.module.empty(),
+    "Method symbol shouldn't have module");
+  // Update the symbol for the method
   method_symbol.mode=ID_java;
   method_symbol.location=m.source_location;
   method_symbol.location.set_function(method_identifier);
@@ -554,16 +561,6 @@ void java_bytecode_convert_methodt::convert(
   method_has_this=code_type.has_this();
   if((!m.is_abstract) && (!m.is_native))
     method_symbol.value=convert_instructions(m, code_type, method_symbol.name);
-
-  // Replace the existing stub symbol with the real deal:
-  const auto s_it=symbol_table.symbols.find(method.get_name());
-  INVARIANT(
-    s_it!=symbol_table.symbols.end(),
-    "the symbol was there earlier on this function; it must be there now");
-  symbol_table.erase(s_it);
-
-  // Insert the method symbol in the symbol table
-  symbol_table.add(method_symbol);
 }
 
 const bytecode_infot &java_bytecode_convert_methodt::get_bytecode_info(
diff --git a/src/java_bytecode/java_bytecode_instrument.cpp b/src/java_bytecode/java_bytecode_instrument.cpp
index a5981a913c5..b0bb08ef14b 100644
--- a/src/java_bytecode/java_bytecode_instrument.cpp
+++ b/src/java_bytecode/java_bytecode_instrument.cpp
@@ -598,7 +598,9 @@ void java_bytecode_instrument_symbol(
     message_handler);
   INVARIANT(
     symbol.value.id()==ID_code,
-    "java_bytecode_instrument expects a code-typed symbol");
+    "java_bytecode_instrument expects a code-typed symbol but was called with"
+      " " + id2string(symbol.name) + " which has a value with an id of " +
+      id2string(symbol.value.id()));
   instrument(symbol.value);
 }
 
diff --git a/src/java_bytecode/java_bytecode_language.cpp b/src/java_bytecode/java_bytecode_language.cpp
index 630bfaae078..73c23711f03 100644
--- a/src/java_bytecode/java_bytecode_language.cpp
+++ b/src/java_bytecode/java_bytecode_language.cpp
@@ -295,6 +295,10 @@ bool java_bytecode_languaget::generate_support_functions(
   if(!res.is_success())
     return res.is_error();
 
+  // Load the main function into the symbol table to get access to its
+  // parameter names
+  convert_lazy_method(res.main_function.name, symbol_table);
+
   // generate the test harness in __CPROVER__start and a call the entry point
   return
     java_entry_point(
@@ -372,12 +376,33 @@ void java_bytecode_languaget::methods_provided(id_sett &methods) const
 /// to have a value representing the method body identical to that produced
 /// using eager method conversion.
 /// \param function_id: method ID to convert
-/// \param symbol_table: global symbol table
+/// \param symtab: global symbol table
 void java_bytecode_languaget::convert_lazy_method(
   const irep_idt &function_id,
-  symbol_tablet &symbol_table)
+  symbol_tablet &symtab)
 {
+  const symbolt &symbol = symtab.lookup_ref(function_id);
+  if(symbol.value.is_not_nil())
+    return;
+
+  journalling_symbol_tablet symbol_table=
+    journalling_symbol_tablet::wrap(symtab);
+
   convert_single_method(function_id, symbol_table);
+
+  // Instrument runtime exceptions (unless symbol is a stub)
+  if(symbol.value.is_not_nil())
+  {
+    java_bytecode_instrument_symbol(
+      symbol_table,
+      symbol_table.get_writeable_ref(function_id),
+      throw_runtime_exceptions,
+      get_message_handler());
+  }
+
+  // now typecheck this function
+  java_bytecode_typecheck_updated_symbols(
+    symbol_table, get_message_handler(), string_refinement_enabled);
 }
 
 /// \brief Convert a method (one whose type is known but whose body hasn't
@@ -466,7 +491,13 @@ bool java_bytecode_languaget::final(symbol_table_baset &symbol_table)
 {
   PRECONDITION(language_options_initialized);
 
-  return false;
+  return recreate_initialize(
+    symbol_table,
+    main_class,
+    get_message_handler(),
+    assume_inputs_non_null,
+    object_factory_parameters,
+    get_pointer_type_selector());
 }
 
 void java_bytecode_languaget::show_parse(std::ostream &out)
diff --git a/src/java_bytecode/java_bytecode_typecheck.cpp b/src/java_bytecode/java_bytecode_typecheck.cpp
index e7f096c8333..36d9e170068 100644
--- a/src/java_bytecode/java_bytecode_typecheck.cpp
+++ b/src/java_bytecode/java_bytecode_typecheck.cpp
@@ -38,34 +38,35 @@ void java_bytecode_typecheckt::typecheck()
 {
   // The hash table iterators are not stable,
   // and we might add new symbols.
-
-  std::vector<irep_idt> identifiers;
+  journalling_symbol_tablet::changesett identifiers;
   identifiers.reserve(symbol_table.symbols.size());
   forall_symbols(s_it, symbol_table.symbols)
-    identifiers.push_back(s_it->first);
+    identifiers.insert(s_it->first);
+  typecheck(identifiers);
+}
 
+void java_bytecode_typecheckt::typecheck(
+  const journalling_symbol_tablet::changesett &identifiers)
+{
   // We first check all type symbols,
   // recursively doing base classes first.
   for(const irep_idt &id : identifiers)
   {
     symbolt &symbol=*symbol_table.get_writeable(id);
-    if(!symbol.is_type)
-      continue;
-    typecheck_type_symbol(symbol);
+    if(symbol.is_type)
+      typecheck_type_symbol(symbol);
   }
-
   // We now check all non-type symbols
   for(const irep_idt &id : identifiers)
   {
     symbolt &symbol=*symbol_table.get_writeable(id);
-    if(symbol.is_type)
-      continue;
-    typecheck_non_type_symbol(symbol);
+    if(!symbol.is_type)
+      typecheck_non_type_symbol(symbol);
   }
 }
 
 bool java_bytecode_typecheck(
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   message_handlert &message_handler,
   bool string_refinement_enabled)
 {
@@ -74,6 +75,16 @@ bool java_bytecode_typecheck(
   return java_bytecode_typecheck.typecheck_main();
 }
 
+void java_bytecode_typecheck_updated_symbols(
+  journalling_symbol_tablet &symbol_table,
+  message_handlert &message_handler,
+  bool string_refinement_enabled)
+{
+  java_bytecode_typecheckt java_bytecode_typecheck(
+    symbol_table, message_handler, string_refinement_enabled);
+  return java_bytecode_typecheck.typecheck(symbol_table.get_updated());
+}
+
 bool java_bytecode_typecheck(
   exprt &expr,
   message_handlert &message_handler,
diff --git a/src/java_bytecode/java_bytecode_typecheck.h b/src/java_bytecode/java_bytecode_typecheck.h
index fa35ba5eda9..29175fe875c 100644
--- a/src/java_bytecode/java_bytecode_typecheck.h
+++ b/src/java_bytecode/java_bytecode_typecheck.h
@@ -15,7 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <set>
 #include <map>
 
-#include <util/symbol_table.h>
+#include <util/journalling_symbol_table.h>
 #include <util/typecheck.h>
 #include <util/namespace.h>
 #include <util/std_code.h>
@@ -23,7 +23,12 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/std_types.h>
 
 bool java_bytecode_typecheck(
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
+  message_handlert &message_handler,
+  bool string_refinement_enabled);
+
+void java_bytecode_typecheck_updated_symbols(
+  journalling_symbol_tablet &symbol_table,
   message_handlert &message_handler,
   bool string_refinement_enabled);
 
@@ -36,7 +41,7 @@ class java_bytecode_typecheckt:public typecheckt
 {
 public:
   java_bytecode_typecheckt(
-    symbol_tablet &_symbol_table,
+    symbol_table_baset &_symbol_table,
     message_handlert &_message_handler,
     bool _string_refinement_enabled):
     typecheckt(_message_handler),
@@ -49,10 +54,11 @@ class java_bytecode_typecheckt:public typecheckt
   virtual ~java_bytecode_typecheckt() { }
 
   virtual void typecheck();
+  void typecheck(const journalling_symbol_tablet::changesett &identifiers);
   virtual void typecheck_expr(exprt &expr);
 
 protected:
-  symbol_tablet &symbol_table;
+  symbol_table_baset &symbol_table;
   const namespacet ns;
   bool string_refinement_enabled;
 
diff --git a/src/java_bytecode/java_entry_point.cpp b/src/java_bytecode/java_entry_point.cpp
index 1a2b83911f1..eab1a397286 100644
--- a/src/java_bytecode/java_entry_point.cpp
+++ b/src/java_bytecode/java_entry_point.cpp
@@ -321,8 +321,7 @@ void java_record_outputs(
 main_function_resultt get_main_symbol(
   const symbol_table_baset &symbol_table,
   const irep_idt &main_class,
-  message_handlert &message_handler,
-  bool allow_no_body)
+  message_handlert &message_handler)
 {
   messaget message(message_handler);
 
@@ -348,14 +347,6 @@ main_function_resultt get_main_symbol(
       symbol != nullptr,
       "resolve_friendly_method_name should return a symbol-table identifier");
 
-    // check if it has a body
-    if(symbol->value.is_nil() && !allow_no_body)
-    {
-      message.error()
-        << "main method `" << main_class << "' has no body" << messaget::eom;
-      return main_function_resultt::Error;
-    }
-
     return *symbol; // Return found function
   }
   else
@@ -395,18 +386,7 @@ main_function_resultt get_main_symbol(
       return main_function_resultt::Error;  // give up with error, no main
     }
 
-    // function symbol
-    const symbolt &symbol = **matches.begin();
-
-    // check if it has a body
-    if(symbol.value.is_nil() && !allow_no_body)
-    {
-      message.error()
-        << "main method `" << main_class << "' has no body" << messaget::eom;
-      return main_function_resultt::Error;  // give up with error
-    }
-
-    return symbol; // Return found function
+    return **matches.begin(); // Return found function
   }
 }
 
@@ -464,7 +444,6 @@ bool java_entry_point(
     return true;
   symbolt symbol=res.main_function;
 
-  assert(!symbol.value.is_nil());
   assert(symbol.type.id()==ID_code);
 
   create_initialize(symbol_table);
@@ -485,6 +464,48 @@ bool java_entry_point(
     pointer_type_selector);
 }
 
+/// Creates the initialize methods again taking account of symbols added to the
+/// symbol table during instantiation of lazy methods since they were first
+/// created,
+/// \param symbol_table: global symbol table containing symbols to initialize
+/// \param main_class: the class containing the "main" entry point
+/// \param message_handler: message_handlert for logging
+/// \param assume_init_pointers_not_null: specifies behaviour for
+/// java_static_lifetime_init
+/// \param object_factory_parameters: specifies behaviour for
+/// java_static_lifetime_init
+/// \param pointer_type_selector: specifies behaviour for
+/// java_static_lifetime_init
+bool recreate_initialize(
+  symbol_table_baset &symbol_table,
+  const irep_idt &main_class,
+  message_handlert &message_handler,
+  bool assume_init_pointers_not_null,
+  const object_factory_parameterst &object_factory_parameters,
+  const select_pointer_typet &pointer_type_selector)
+{
+  messaget message(message_handler);
+  main_function_resultt res=
+    get_main_symbol(symbol_table, main_class, message_handler);
+  if(res.status!=main_function_resultt::Success)
+  {
+    // No initialization was originally created (yikes!) so we can't recreate
+    // it now
+    return res.status==main_function_resultt::Error;
+  }
+
+  create_initialize(symbol_table);
+
+  java_static_lifetime_init(
+    symbol_table,
+    res.main_function.location,
+    assume_init_pointers_not_null,
+    object_factory_parameters,
+    pointer_type_selector);
+
+  return false;
+}
+
 /// Generate a _start function for a specific function. See
 /// java_entry_point for more details.
 /// \param symbol: The symbol representing the function to call
diff --git a/src/java_bytecode/java_entry_point.h b/src/java_bytecode/java_entry_point.h
index 8a21df6d389..98495c72a5a 100644
--- a/src/java_bytecode/java_entry_point.h
+++ b/src/java_bytecode/java_entry_point.h
@@ -63,8 +63,7 @@ struct main_function_resultt
 main_function_resultt get_main_symbol(
   const symbol_table_baset &symbol_table,
   const irep_idt &main_class,
-  message_handlert &,
-  bool allow_no_body = false);
+  message_handlert &);
 
 bool generate_java_start_function(
   const symbolt &symbol,
@@ -74,4 +73,12 @@ bool generate_java_start_function(
   const object_factory_parameterst& object_factory_parameters,
   const select_pointer_typet &pointer_type_selector);
 
+bool recreate_initialize(
+  symbol_table_baset &symbol_table,
+  const irep_idt &main_class,
+  message_handlert &message_handler,
+  bool assume_init_pointers_not_null,
+  const object_factory_parameterst &object_factory_parameters,
+  const select_pointer_typet &pointer_type_selector);
+
 #endif // CPROVER_JAVA_BYTECODE_JAVA_ENTRY_POINT_H
diff --git a/src/java_bytecode/java_pointer_casts.cpp b/src/java_bytecode/java_pointer_casts.cpp
index 26b42e0bd31..702211faeb1 100644
--- a/src/java_bytecode/java_pointer_casts.cpp
+++ b/src/java_bytecode/java_pointer_casts.cpp
@@ -45,16 +45,20 @@ bool find_superclass_with_type(
     if(base_struct.components().empty())
       return false;
 
-    const typet &first_field_type=
-        ns.follow(base_struct.components()[0].type());
+    const typet &first_field_type=base_struct.components()[0].type();
     ptr=clean_deref(ptr);
+    // Careful not to use the followed type here, as stub types may be
+    // extended by later method conversion adding fields (e.g. an access
+    // against x->y might add a new field `y` to the type of `*x`)
     ptr=member_exprt(
       ptr,
       base_struct.components()[0].get_name(),
       first_field_type);
     ptr=address_of_exprt(ptr);
 
-    if(first_field_type==target_type)
+    // Compare the real (underlying) type, as target_type is already a non-
+    // symbolic type.
+    if(ns.follow(first_field_type)==target_type)
       return true;
   }
 }
diff --git a/src/jbmc/jbmc_parse_options.cpp b/src/jbmc/jbmc_parse_options.cpp
index 7d3da461fd5..387064b40e8 100644
--- a/src/jbmc/jbmc_parse_options.cpp
+++ b/src/jbmc/jbmc_parse_options.cpp
@@ -26,7 +26,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <ansi-c/ansi_c_language.h>
 
 #include <goto-programs/convert_nondet.h>
-#include <goto-programs/initialize_goto_model.h>
+#include <goto-programs/lazy_goto_model.h>
 #include <goto-programs/instrument_preconditions.h>
 #include <goto-programs/goto_convert_functions.h>
 #include <goto-programs/goto_inline.h>
@@ -50,6 +50,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <goto-programs/show_properties.h>
 #include <goto-programs/string_abstraction.h>
 #include <goto-programs/string_instrumentation.h>
+#include <goto-programs/remove_java_new.h>
 
 #include <goto-symex/rewrite_union.h>
 #include <goto-symex/adjust_float_expressions.h>
@@ -480,18 +481,20 @@ int jbmc_parse_optionst::doit()
     return 0;
   }
 
-  int get_goto_program_ret=get_goto_program(options);
-
+  std::unique_ptr<goto_modelt> goto_model_ptr;
+  int get_goto_program_ret=get_goto_program(goto_model_ptr, options);
   if(get_goto_program_ret!=-1)
     return get_goto_program_ret;
 
+  goto_modelt &goto_model = *goto_model_ptr;
+
   if(cmdline.isset("show-properties"))
   {
     show_properties(goto_model, ui_message_handler.get_ui());
     return 0; // should contemplate EX_OK from sysexits.h
   }
 
-  if(set_properties())
+  if(set_properties(goto_model))
     return 7; // should contemplate EX_USAGE from sysexits.h
 
   // unwinds <clinit> loops to number of enum elements
@@ -529,10 +532,10 @@ int jbmc_parse_optionst::doit()
     prop_conv);
 
   // do actual BMC
-  return do_bmc(bmc);
+  return do_bmc(bmc, goto_model);
 }
 
-bool jbmc_parse_optionst::set_properties()
+bool jbmc_parse_optionst::set_properties(goto_modelt &goto_model)
 {
   try
   {
@@ -561,6 +564,7 @@ bool jbmc_parse_optionst::set_properties()
 }
 
 int jbmc_parse_optionst::get_goto_program(
+  std::unique_ptr<goto_modelt> &goto_model,
   const optionst &options)
 {
   if(cmdline.args.empty())
@@ -571,28 +575,40 @@ int jbmc_parse_optionst::get_goto_program(
 
   try
   {
-    goto_model=initialize_goto_model(cmdline, get_message_handler());
+    lazy_goto_modelt lazy_goto_model=lazy_goto_modelt::from_handler_object(
+      *this, options, get_message_handler());
+    lazy_goto_model.initialize(cmdline);
 
+    status() << "Generating GOTO Program" << messaget::eom;
+    lazy_goto_model.load_all_functions();
+
+    // Show the symbol table before process_goto_functions mangles return
+    // values, etc
     if(cmdline.isset("show-symbol-table"))
     {
-      show_symbol_table(goto_model, ui_message_handler.get_ui());
+      show_symbol_table(
+        lazy_goto_model.symbol_table, ui_message_handler.get_ui());
       return 0;
     }
 
-    if(process_goto_program(options))
+    // Move the model out of the local lazy_goto_model
+    // and into the caller's goto_model
+    goto_model=lazy_goto_modelt::process_whole_model_and_freeze(
+      std::move(lazy_goto_model));
+    if(goto_model == nullptr)
       return 6;
 
     // show it?
     if(cmdline.isset("show-loops"))
     {
-      show_loop_ids(ui_message_handler.get_ui(), goto_model);
+      show_loop_ids(ui_message_handler.get_ui(), *goto_model);
       return 0;
     }
 
     // show it?
     if(cmdline.isset("show-goto-functions"))
     {
-      show_goto_functions(goto_model, ui_message_handler.get_ui());
+      show_goto_functions(*goto_model, ui_message_handler.get_ui());
       return 0;
     }
 
@@ -625,14 +641,42 @@ int jbmc_parse_optionst::get_goto_program(
   return -1; // no error, continue
 }
 
-bool jbmc_parse_optionst::process_goto_program(
-  const optionst &options)
+void jbmc_parse_optionst::process_goto_function(
+  goto_functionst::goto_functiont &function, symbol_tablet &symbol_table)
 {
   try
   {
     // Remove inline assembler; this needs to happen before
     // adding the library.
-    remove_asm(goto_model);
+    remove_asm(function, symbol_table);
+  }
+
+  catch(const char *e)
+  {
+    error() << e << eom;
+    throw;
+  }
+
+  catch(const std::string &e)
+  {
+    error() << e << eom;
+    throw;
+  }
+
+  catch(const std::bad_alloc &)
+  {
+    error() << "Out of memory" << eom;
+    throw;
+  }
+}
+
+bool jbmc_parse_optionst::process_goto_functions(
+  goto_modelt &goto_model,
+  const optionst &options)
+{
+  try
+  {
+    remove_java_new(goto_model, get_message_handler());
 
     // add the library
     link_to_library(goto_model, get_message_handler());
@@ -717,9 +761,6 @@ bool jbmc_parse_optionst::process_goto_program(
     // recalculate numbers, etc.
     goto_model.goto_functions.update();
 
-    // add loop ids
-    goto_model.goto_functions.compute_loop_numbers();
-
     if(cmdline.isset("drop-unused-functions"))
     {
       // Entry point will have been set before and function pointers removed
@@ -790,7 +831,7 @@ bool jbmc_parse_optionst::process_goto_program(
 }
 
 /// invoke main modules
-int jbmc_parse_optionst::do_bmc(bmct &bmc)
+int jbmc_parse_optionst::do_bmc(bmct &bmc, goto_modelt &goto_model)
 {
   bmc.set_ui(ui_message_handler.get_ui());
 
diff --git a/src/jbmc/jbmc_parse_options.h b/src/jbmc/jbmc_parse_options.h
index 06916c296a9..5c722e0821a 100644
--- a/src/jbmc/jbmc_parse_options.h
+++ b/src/jbmc/jbmc_parse_options.h
@@ -78,16 +78,20 @@ class jbmc_parse_optionst:
     const char **argv,
     const std::string &extra_options);
 
+  void process_goto_function(
+    goto_functionst::goto_functiont &function, symbol_tablet &symbol_table);
+  bool process_goto_functions(goto_modelt &goto_model, const optionst &options);
+
 protected:
-  goto_modelt goto_model;
   ui_message_handlert ui_message_handler;
 
   void eval_verbosity();
   void get_command_line_options(optionst &);
-  int get_goto_program(const optionst &);
-  bool process_goto_program(const optionst &);
-  bool set_properties();
-  int do_bmc(bmct &);
+  int get_goto_program(
+    std::unique_ptr<goto_modelt> &goto_model, const optionst &);
+
+  bool set_properties(goto_modelt &goto_model);
+  int do_bmc(bmct &, goto_modelt &goto_model);
 };
 
 #endif // CPROVER_JBMC_JBMC_PARSE_OPTIONS_H
diff --git a/src/langapi/language_ui.cpp b/src/langapi/language_ui.cpp
index 0d515d81afb..560fd43bb89 100644
--- a/src/langapi/language_ui.cpp
+++ b/src/langapi/language_ui.cpp
@@ -58,13 +58,7 @@ bool language_uit::parse(const std::string &filename)
     return true;
   }
 
-  std::pair<language_filest::file_mapt::iterator, bool>
-    result=language_files.file_map.insert(
-      std::pair<std::string, language_filet>(filename, language_filet()));
-
-  language_filet &lf=result.first->second;
-
-  lf.filename=filename;
+  language_filet &lf=language_files.add_file(filename);
   lf.language=get_language_from_filename(filename);
 
   if(lf.language==nullptr)
diff --git a/src/util/language_file.cpp b/src/util/language_file.cpp
index f42e7f88159..559648182aa 100644
--- a/src/util/language_file.cpp
+++ b/src/util/language_file.cpp
@@ -25,7 +25,10 @@ language_filet::language_filet(const language_filet &rhs):
 /// destructor in the source file, where the full definition is availible.
 language_filet::~language_filet()=default;
 
-language_filet::language_filet()=default;
+language_filet::language_filet(const std::string &filename)
+  : filename(filename)
+{
+}
 
 void language_filet::get_modules()
 {
diff --git a/src/util/language_file.h b/src/util/language_file.h
index 19f644b8d44..6c32c68496a 100644
--- a/src/util/language_file.h
+++ b/src/util/language_file.h
@@ -17,11 +17,10 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <memory> // unique_ptr
 
 #include "message.h"
+#include "symbol_table.h"
+#include "language.h"
 
-class symbol_tablet;
-class symbol_table_baset;
 class language_filet;
-class languaget;
 
 class language_modulet final
 {
@@ -52,7 +51,7 @@ class language_filet final
     const irep_idt &id,
     symbol_tablet &symbol_table);
 
-  language_filet();
+  explicit language_filet(const std::string &filename);
   language_filet(const language_filet &rhs);
 
   ~language_filet();
@@ -60,21 +59,44 @@ class language_filet final
 
 class language_filest:public messaget
 {
-public:
+private:
   typedef std::map<std::string, language_filet> file_mapt;
   file_mapt file_map;
 
-  // Contains pointers into file_mapt!
   typedef std::map<std::string, language_modulet> module_mapt;
   module_mapt module_map;
 
-  // Contains pointers into filemapt!
+  // Contains pointers into file_map!
   // This is safe-ish as long as this is std::map.
   typedef std::map<irep_idt, language_filet *> lazy_method_mapt;
   lazy_method_mapt lazy_method_map;
 
+public:
+  language_filet &add_file(const std::string &filename)
+  {
+    language_filet language_file(filename);
+    return file_map.emplace(filename, std::move(language_file)).first->second;
+  }
+
+  void remove_file(const std::string &filename)
+  {
+    // Clear relevant entries from lazy_method_map
+    language_filet *language_file = &file_map.at(filename);
+    id_sett files_methods;
+    for(const std::pair<irep_idt, language_filet *> &method : lazy_method_map)
+    {
+      if(method.second == language_file)
+        files_methods.insert(method.first);
+    }
+    for(const irep_idt &method_name : files_methods)
+      lazy_method_map.erase(method_name);
+
+    file_map.erase(filename);
+  }
+
   void clear_files()
   {
+    lazy_method_map.clear();
     file_map.clear();
   }
 
@@ -92,11 +114,6 @@ class language_filest:public messaget
 
   bool interfaces(symbol_tablet &symbol_table);
 
-  bool has_lazy_method(const irep_idt &id)
-  {
-    return lazy_method_map.count(id)!=0;
-  }
-
   // The method must have been added to the symbol table and registered
   // in lazy_method_map (currently always in language_filest::typecheck)
   // for this to be legal.
@@ -104,7 +121,10 @@ class language_filest:public messaget
     const irep_idt &id,
     symbol_tablet &symbol_table)
   {
-    return lazy_method_map.at(id)->convert_lazy_method(id, symbol_table);
+    PRECONDITION(symbol_table.has_symbol(id));
+    lazy_method_mapt::iterator it=lazy_method_map.find(id);
+    if(it!=lazy_method_map.end())
+      it->second->convert_lazy_method(id, symbol_table);
   }
 
   void clear()
diff --git a/src/util/symbol.h b/src/util/symbol.h
index 7edae3146c0..06945fc6c1f 100644
--- a/src/util/symbol.h
+++ b/src/util/symbol.h
@@ -109,6 +109,11 @@ class symbolt
   {
     return !is_static_lifetime;
   }
+
+  bool is_function() const
+  {
+    return !is_type && !is_macro && type.id()==ID_code;
+  }
 };
 
 std::ostream &operator<<(std::ostream &out, const symbolt &symbol);
diff --git a/unit/java_bytecode/java_string_library_preprocess/convert_exprt_to_string_exprt.cpp b/unit/java_bytecode/java_string_library_preprocess/convert_exprt_to_string_exprt.cpp
index 78c85045929..7970c2af11f 100644
--- a/unit/java_bytecode/java_string_library_preprocess/convert_exprt_to_string_exprt.cpp
+++ b/unit/java_bytecode/java_string_library_preprocess/convert_exprt_to_string_exprt.cpp
@@ -9,7 +9,7 @@
 
 #include <testing-utils/catch.hpp>
 #include <util/c_types.h>
-#include <util/expr.h>
+#include <util/fresh_symbol.h>
 #include <util/std_code.h>
 #include <java_bytecode/java_string_library_preprocess.h>
 #include <langapi/language_util.h>
@@ -32,6 +32,8 @@ TEST_CASE("Convert exprt to string exprt")
 {
   GIVEN("A location, a string expression, and a symbol table")
   {
+    reset_temporary_counter();
+
     source_locationt loc;
     symbol_tablet symbol_table;
     namespacet ns(symbol_table);
diff --git a/unit/pointer-analysis/custom_value_set_analysis.cpp b/unit/pointer-analysis/custom_value_set_analysis.cpp
index b3f64a14476..db657133a51 100644
--- a/unit/pointer-analysis/custom_value_set_analysis.cpp
+++ b/unit/pointer-analysis/custom_value_set_analysis.cpp
@@ -12,6 +12,7 @@ Author: Chris Smowton, chris@smowton.net
 #include <langapi/mode.h>
 #include <goto-programs/initialize_goto_model.h>
 #include <goto-programs/goto_inline.h>
+#include <goto-programs/remove_java_new.h>
 #include <java_bytecode/java_bytecode_language.h>
 #include <java_bytecode/java_types.h>
 #include <pointer-analysis/value_set_analysis.h>
@@ -183,6 +184,9 @@ SCENARIO("test_value_set_analysis",
 
     namespacet ns(goto_model.symbol_table);
 
+    // VSA doesn't currently support java_new as an allocator
+    remove_java_new(goto_model, null_output);
+
     // Fully inline the test program, to avoid VSA conflating
     // constructor callsites confusing the results we're trying to check:
     goto_function_inline(goto_model, TEST_FUNCTION_NAME, null_output);
diff --git a/unit/testing-utils/load_java_class.cpp b/unit/testing-utils/load_java_class.cpp
index f79e14f7c9b..737dae1a162 100644
--- a/unit/testing-utils/load_java_class.cpp
+++ b/unit/testing-utils/load_java_class.cpp
@@ -12,8 +12,11 @@
 
 #include <util/config.h>
 #include <util/language.h>
+#include <util/options.h>
 #include <util/suffix.h>
 
+#include <goto-programs/lazy_goto_model.h>
+
 #include <java_bytecode/java_bytecode_language.h>
 
 /// Go through the process of loading, typechecking and finalising loading a
@@ -34,11 +37,21 @@ symbol_tablet load_java_class(
 symbol_tablet load_java_class(
   const std::string &java_class_name,
   const std::string &class_path,
-  std::unique_ptr<languaget> java_lang)
+  std::unique_ptr<languaget> &&java_lang)
 {
-  // We don't expect the .class suffix to allow us to check the name of the
-  // class
+  // We expect the name of the class without the .class suffix to allow us to
+  // check it
   PRECONDITION(!has_suffix(java_class_name, ".class"));
+  std::string filename=java_class_name + ".class";
+
+  // Construct a lazy_goto_modelt
+  null_message_handlert message_handler;
+  lazy_goto_modelt lazy_goto_model(
+    [] (goto_functionst::goto_functiont &function, symbol_tablet &symbol_table)
+    { },
+    [] (goto_modelt &goto_model)
+    { return false; },
+    message_handler);
 
   // Configure the path loading
   cmdlinet command_line;
@@ -46,22 +59,33 @@ symbol_tablet load_java_class(
   config.java.classpath.clear();
   config.java.classpath.push_back(class_path);
 
-  symbol_tablet new_symbol_table;
+  // Add the language to the model
+  language_filet &lf=lazy_goto_model.add_language_file(filename);
+  lf.language=std::move(java_lang);
+  languaget &language=*lf.language;
 
   std::istringstream java_code_stream("ignored");
-  null_message_handlert message_handler;
 
   // Configure the language, load the class files
-  java_lang->get_language_options(command_line);
-  java_lang->set_message_handler(message_handler);
-  java_lang->parse(java_code_stream, java_class_name + ".class");
-  java_lang->typecheck(new_symbol_table, "");
-  java_lang->final(new_symbol_table);
+  language.set_message_handler(message_handler);
+  language.get_language_options(command_line);
+  language.parse(java_code_stream, filename);
+  language.typecheck(lazy_goto_model.symbol_table, "");
+  language.generate_support_functions(lazy_goto_model.symbol_table);
+  language.final(lazy_goto_model.symbol_table);
+
+  lazy_goto_model.load_all_functions();
+
+  std::unique_ptr<goto_modelt> maybe_goto_model=
+    lazy_goto_modelt::process_whole_model_and_freeze(
+      std::move(lazy_goto_model));
+  INVARIANT(maybe_goto_model, "Freezing lazy_goto_model failed");
 
   // Verify that the class was loaded
   const std::string class_symbol_name="java::"+java_class_name;
-  REQUIRE(new_symbol_table.has_symbol(class_symbol_name));
-  const symbolt &class_symbol=*new_symbol_table.lookup(class_symbol_name);
+  REQUIRE(maybe_goto_model->symbol_table.has_symbol(class_symbol_name));
+  const symbolt &class_symbol=
+    *maybe_goto_model->symbol_table.lookup(class_symbol_name);
   REQUIRE(class_symbol.is_type);
   const typet &class_type=class_symbol.type;
   REQUIRE(class_type.id()==ID_struct);
@@ -70,5 +94,5 @@ symbol_tablet load_java_class(
   // Check your working directory and the class path is correctly configured
   // as this often indicates that one of these is wrong.
   REQUIRE_FALSE(class_type.get_bool(ID_incomplete_class));
-  return new_symbol_table;
+  return std::move(maybe_goto_model->symbol_table);
 }
diff --git a/unit/testing-utils/load_java_class.h b/unit/testing-utils/load_java_class.h
index c1c8ecd65cf..7460ca6d693 100644
--- a/unit/testing-utils/load_java_class.h
+++ b/unit/testing-utils/load_java_class.h
@@ -24,6 +24,6 @@ symbol_tablet load_java_class(
 symbol_tablet load_java_class(
   const std::string &java_class_name,
   const std::string &class_path,
-  std::unique_ptr<languaget> java_lang);
+  std::unique_ptr<languaget> &&java_lang);
 
 #endif // CPROVER_TESTING_UTILS_LOAD_JAVA_CLASS_H