diff --git a/regression/cbmc-java/lazyloading1/A.class b/regression/cbmc-java/lazyloading1/A.class
new file mode 100644
index 00000000000..d6a62ca1ce4
Binary files /dev/null and b/regression/cbmc-java/lazyloading1/A.class differ
diff --git a/regression/cbmc-java/lazyloading1/B.class b/regression/cbmc-java/lazyloading1/B.class
new file mode 100644
index 00000000000..2d693bf7383
Binary files /dev/null and b/regression/cbmc-java/lazyloading1/B.class differ
diff --git a/regression/cbmc-java/lazyloading1/test.class b/regression/cbmc-java/lazyloading1/test.class
new file mode 100644
index 00000000000..25d52a223f4
Binary files /dev/null and b/regression/cbmc-java/lazyloading1/test.class differ
diff --git a/regression/cbmc-java/lazyloading1/test.desc b/regression/cbmc-java/lazyloading1/test.desc
new file mode 100644
index 00000000000..c0011248128
--- /dev/null
+++ b/regression/cbmc-java/lazyloading1/test.desc
@@ -0,0 +1,8 @@
+CORE
+test.class
+--lazy-methods --verbosity 10 --function test.main
+^EXIT=0$
+^SIGNAL=0$
+elaborate java::A\.f:\(\)V
+--
+elaborate java::B\.g:\(\)V
diff --git a/regression/cbmc-java/lazyloading1/test.java b/regression/cbmc-java/lazyloading1/test.java
new file mode 100644
index 00000000000..e0686d8c4d0
--- /dev/null
+++ b/regression/cbmc-java/lazyloading1/test.java
@@ -0,0 +1,21 @@
+// The most basic lazy loading test: A::f is directly called, B::g should be unreachable
+
+public class test
+{
+  A a;
+  B b;
+  public static void main()
+  {
+    A.f();
+  }
+}
+
+class A
+{
+  public static void f() {}
+}
+
+class B
+{
+  public static void g() {}
+}
diff --git a/regression/cbmc-java/lazyloading2/A.class b/regression/cbmc-java/lazyloading2/A.class
new file mode 100644
index 00000000000..6d789cdb6ec
Binary files /dev/null and b/regression/cbmc-java/lazyloading2/A.class differ
diff --git a/regression/cbmc-java/lazyloading2/B.class b/regression/cbmc-java/lazyloading2/B.class
new file mode 100644
index 00000000000..d9cf49c418f
Binary files /dev/null and b/regression/cbmc-java/lazyloading2/B.class differ
diff --git a/regression/cbmc-java/lazyloading2/test.class b/regression/cbmc-java/lazyloading2/test.class
new file mode 100644
index 00000000000..054809ef0f6
Binary files /dev/null and b/regression/cbmc-java/lazyloading2/test.class differ
diff --git a/regression/cbmc-java/lazyloading2/test.desc b/regression/cbmc-java/lazyloading2/test.desc
new file mode 100644
index 00000000000..c0011248128
--- /dev/null
+++ b/regression/cbmc-java/lazyloading2/test.desc
@@ -0,0 +1,8 @@
+CORE
+test.class
+--lazy-methods --verbosity 10 --function test.main
+^EXIT=0$
+^SIGNAL=0$
+elaborate java::A\.f:\(\)V
+--
+elaborate java::B\.g:\(\)V
diff --git a/regression/cbmc-java/lazyloading2/test.java b/regression/cbmc-java/lazyloading2/test.java
new file mode 100644
index 00000000000..b53bae71fa4
--- /dev/null
+++ b/regression/cbmc-java/lazyloading2/test.java
@@ -0,0 +1,23 @@
+// This test checks that because A is instantiated in main and B is not,
+// A::f is reachable and B::g is not
+
+public class test
+{
+  A a;
+  B b;
+  public static void main()
+  {
+    A a = new A();
+    a.f();
+  }
+}
+
+class A
+{
+  public void f() {}
+}
+
+class B
+{
+  public void g() {}
+}
diff --git a/regression/cbmc-java/lazyloading3/A.class b/regression/cbmc-java/lazyloading3/A.class
new file mode 100644
index 00000000000..affb565d625
Binary files /dev/null and b/regression/cbmc-java/lazyloading3/A.class differ
diff --git a/regression/cbmc-java/lazyloading3/B.class b/regression/cbmc-java/lazyloading3/B.class
new file mode 100644
index 00000000000..9a4ab54d369
Binary files /dev/null and b/regression/cbmc-java/lazyloading3/B.class differ
diff --git a/regression/cbmc-java/lazyloading3/C.class b/regression/cbmc-java/lazyloading3/C.class
new file mode 100644
index 00000000000..c249e24ace4
Binary files /dev/null and b/regression/cbmc-java/lazyloading3/C.class differ
diff --git a/regression/cbmc-java/lazyloading3/D.class b/regression/cbmc-java/lazyloading3/D.class
new file mode 100644
index 00000000000..7e16bd6527d
Binary files /dev/null and b/regression/cbmc-java/lazyloading3/D.class differ
diff --git a/regression/cbmc-java/lazyloading3/test.class b/regression/cbmc-java/lazyloading3/test.class
new file mode 100644
index 00000000000..8e470f64650
Binary files /dev/null and b/regression/cbmc-java/lazyloading3/test.class differ
diff --git a/regression/cbmc-java/lazyloading3/test.desc b/regression/cbmc-java/lazyloading3/test.desc
new file mode 100644
index 00000000000..c0011248128
--- /dev/null
+++ b/regression/cbmc-java/lazyloading3/test.desc
@@ -0,0 +1,8 @@
+CORE
+test.class
+--lazy-methods --verbosity 10 --function test.main
+^EXIT=0$
+^SIGNAL=0$
+elaborate java::A\.f:\(\)V
+--
+elaborate java::B\.g:\(\)V
diff --git a/regression/cbmc-java/lazyloading3/test.java b/regression/cbmc-java/lazyloading3/test.java
new file mode 100644
index 00000000000..6d3129d1261
--- /dev/null
+++ b/regression/cbmc-java/lazyloading3/test.java
@@ -0,0 +1,30 @@
+// This test checks that because `main` has a parameter of type C, which has a field of type A,
+// A::f is considered reachable, but B::g is not.
+
+public class test
+{
+  public static void main(C c)
+  {
+    c.a.f();
+  }
+}
+
+class A
+{
+  public void f() {}
+}
+
+class B
+{
+  public void g() {}
+}
+
+class C
+{
+  A a;
+}
+
+class D
+{
+  B b;
+}
diff --git a/regression/failed-tests-printer.pl b/regression/failed-tests-printer.pl
index 832ba2d2c64..40767185d5c 100755
--- a/regression/failed-tests-printer.pl
+++ b/regression/failed-tests-printer.pl
@@ -4,23 +4,25 @@
 
 open LOG,"<tests.log" or die "Failed to open tests.log\n";
 
-my $ignore = 1;
+my $printed_this_test = 1;
 my $current_test = "";
 
 while (<LOG>) {
   chomp;
   if (/^Test '(.+)'/) {
     $current_test = $1;
-    $ignore = 0;
-  } elsif (1 == $ignore) {
-    next;
+    $printed_this_test = 0;
   } elsif (/\[FAILED\]\s*$/) {
-    $ignore = 1;
-    print "Failed test: $current_test\n";
-    my $outf = `sed -n '2p' $current_test/test.desc`;
-    $outf =~ s/\..*$/.out/;
-    system("cat $current_test/$outf");
-    print "\n\n";
+    if(0 == $printed_this_test) {
+      $printed_this_test = 1;
+      print "\n\n";
+      print "Failed test: $current_test\n";
+      my $outf = `sed -n '2p' $current_test/test.desc`;
+      $outf =~ s/\..*$/.out/;
+      system("cat $current_test/$outf");
+      print "\n\nFailed test.desc lines:\n";
+    }
+    print "$_\n";
   }
 }
 
diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h
index 87e9beb45d2..adc6e2ee517 100644
--- a/src/cbmc/cbmc_parse_options.h
+++ b/src/cbmc/cbmc_parse_options.h
@@ -56,6 +56,7 @@ class optionst;
   "(graphml-witness):" \
   "(java-max-vla-length):(java-unwind-enum-static)" \
   "(localize-faults)(localize-faults-method):" \
+  "(lazy-methods)" \
   "(fixedbv)(floatbv)(all-claims)(all-properties)" // legacy, and will eventually disappear // NOLINT(whitespace/line_length)
 
 class cbmc_parse_optionst:
diff --git a/src/goto-cc/compile.cpp b/src/goto-cc/compile.cpp
index 7ab9c5eae3d..3027bc5bf0b 100644
--- a/src/goto-cc/compile.cpp
+++ b/src/goto-cc/compile.cpp
@@ -540,8 +540,8 @@ bool compilet::parse(const std::string &file_name)
 
   language_filet language_file;
 
-  std::pair<language_filest::filemapt::iterator, bool>
-  res=language_files.filemap.insert(
+  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;
@@ -732,7 +732,7 @@ bool compilet::parse_source(const std::string &file_name)
     return true;
 
   // so we remove it from the list afterwards
-  language_files.filemap.erase(file_name);
+  language_files.file_map.erase(file_name);
   return false;
 }
 
diff --git a/src/goto-programs/get_goto_model.cpp b/src/goto-programs/get_goto_model.cpp
index 5afef435596..02aae876030 100644
--- a/src/goto-programs/get_goto_model.cpp
+++ b/src/goto-programs/get_goto_model.cpp
@@ -75,8 +75,8 @@ bool get_goto_modelt::operator()(const std::vector<std::string> &files)
           return true;
         }
 
-        std::pair<language_filest::filemapt::iterator, bool>
-          result=language_files.filemap.insert(
+        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;
diff --git a/src/goto-programs/remove_virtual_functions.cpp b/src/goto-programs/remove_virtual_functions.cpp
index da9cce5039f..b24621fe668 100644
--- a/src/goto-programs/remove_virtual_functions.cpp
+++ b/src/goto-programs/remove_virtual_functions.cpp
@@ -339,7 +339,8 @@ void remove_virtual_functionst::get_functions(
     component_name,
     functions);
 
-  functions.push_back(root_function);
+  if(root_function.symbol_expr!=symbol_exprt())
+    functions.push_back(root_function);
 }
 
 /*******************************************************************\
diff --git a/src/java_bytecode/java_bytecode_convert_class.cpp b/src/java_bytecode/java_bytecode_convert_class.cpp
index 8d42611bfe0..440b0ce32cf 100644
--- a/src/java_bytecode/java_bytecode_convert_class.cpp
+++ b/src/java_bytecode/java_bytecode_convert_class.cpp
@@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "java_root_class.h"
 #include "java_types.h"
 #include "java_bytecode_convert_method.h"
+#include "java_bytecode_language.h"
 
 #include <util/namespace.h>
 #include <util/std_expr.h>
@@ -27,11 +28,15 @@ class java_bytecode_convert_classt:public messaget
     symbol_tablet &_symbol_table,
     message_handlert &_message_handler,
     bool _disable_runtime_checks,
-    size_t _max_array_length):
+    size_t _max_array_length,
+    lazy_methodst& _lazy_methods,
+    lazy_methods_modet _lazy_methods_mode):
     messaget(_message_handler),
     symbol_table(_symbol_table),
     disable_runtime_checks(_disable_runtime_checks),
-    max_array_length(_max_array_length)
+    max_array_length(_max_array_length),
+    lazy_methods(_lazy_methods),
+    lazy_methods_mode(_lazy_methods_mode)
   {
   }
 
@@ -52,6 +57,8 @@ class java_bytecode_convert_classt:public messaget
   symbol_tablet &symbol_table;
   const bool disable_runtime_checks;
   const size_t max_array_length;
+  lazy_methodst &lazy_methods;
+  lazy_methods_modet lazy_methods_mode;
 
   // conversion
   void convert(const classt &c);
@@ -75,6 +82,13 @@ Function: java_bytecode_convert_classt::convert
 
 void java_bytecode_convert_classt::convert(const classt &c)
 {
+  std::string qualified_classname="java::"+id2string(c.name);
+  if(symbol_table.has_symbol(qualified_classname))
+  {
+    debug() << "Skip class " << c.name << " (already loaded)" << eom;
+    return;
+  }
+
   class_typet class_type;
 
   class_type.set_tag(c.name);
@@ -107,7 +121,7 @@ void java_bytecode_convert_classt::convert(const classt &c)
   symbolt new_symbol;
   new_symbol.base_name=c.name;
   new_symbol.pretty_name=c.name;
-  new_symbol.name="java::"+id2string(c.name);
+  new_symbol.name=qualified_classname;
   class_type.set(ID_name, new_symbol.name);
   new_symbol.type=class_type;
   new_symbol.mode=ID_java;
@@ -128,13 +142,35 @@ void java_bytecode_convert_classt::convert(const classt &c)
 
   // now do methods
   for(const auto &method : c.methods)
-    java_bytecode_convert_method(
+  {
+    const irep_idt method_identifier=
+      id2string(qualified_classname)+
+      "."+id2string(method.name)+
+      ":"+method.signature;
+    // Always run the lazy pre-stage, as it symbol-table
+    // registers the function.
+    java_bytecode_convert_method_lazy(
       *class_symbol,
+      method_identifier,
       method,
-      symbol_table,
-      get_message_handler(),
-      disable_runtime_checks,
-      max_array_length);
+      symbol_table);
+    if(lazy_methods_mode==LAZY_METHODS_MODE_EAGER)
+    {
+      // Upgrade to a fully-realized symbol now:
+      java_bytecode_convert_method(
+        *class_symbol,
+        method,
+        symbol_table,
+        get_message_handler(),
+        disable_runtime_checks,
+        max_array_length);
+    }
+    else
+    {
+      // Wait for our caller to decide what needs elaborating.
+      lazy_methods[method_identifier]=std::make_pair(class_symbol, &method);
+    }
+  }
 
   // is this a root class?
   if(c.extends.empty())
@@ -322,13 +358,17 @@ bool java_bytecode_convert_class(
   symbol_tablet &symbol_table,
   message_handlert &message_handler,
   bool disable_runtime_checks,
-  size_t max_array_length)
+  size_t max_array_length,
+  lazy_methodst &lazy_methods,
+  lazy_methods_modet lazy_methods_mode)
 {
   java_bytecode_convert_classt java_bytecode_convert_class(
     symbol_table,
     message_handler,
     disable_runtime_checks,
-    max_array_length);
+    max_array_length,
+    lazy_methods,
+    lazy_methods_mode);
 
   try
   {
diff --git a/src/java_bytecode/java_bytecode_convert_class.h b/src/java_bytecode/java_bytecode_convert_class.h
index ffaaf6e34da..5cc1526a125 100644
--- a/src/java_bytecode/java_bytecode_convert_class.h
+++ b/src/java_bytecode/java_bytecode_convert_class.h
@@ -13,12 +13,15 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/message.h>
 
 #include "java_bytecode_parse_tree.h"
+#include "java_bytecode_language.h"
 
 bool java_bytecode_convert_class(
   const java_bytecode_parse_treet &parse_tree,
   symbol_tablet &symbol_table,
   message_handlert &message_handler,
   bool disable_runtime_checks,
-  size_t max_array_length);
+  size_t max_array_length,
+  lazy_methodst &,
+  lazy_methods_modet);
 
 #endif // CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_CONVERT_CLASS_H
diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp
index f9cb121091b..5e85451398a 100644
--- a/src/java_bytecode/java_bytecode_convert_method.cpp
+++ b/src/java_bytecode/java_bytecode_convert_method.cpp
@@ -179,43 +179,93 @@ const exprt java_bytecode_convert_methodt::variable(
 
 /*******************************************************************\
 
-Function: java_bytecode_convert_methodt::convert
+Function: java_bytecode_convert_method_lazy
 
-  Inputs:
+  Inputs: `class_symbol`: class this method belongs to
+          `method_identifier`: fully qualified method name, including
+            type signature (e.g. "x.y.z.f:(I)")
+          `m`: parsed method object to convert
+          `symbol_table`: global symbol table (will be modified)
 
  Outputs:
 
- Purpose:
+ Purpose: This creates a method symbol in the symtab, but doesn't
+          actually perform method conversion just yet. The caller
+          should call java_bytecode_convert_method later to give the
+          symbol/method a body.
 
 \*******************************************************************/
 
-void java_bytecode_convert_methodt::convert(
+void java_bytecode_convert_method_lazy(
   const symbolt &class_symbol,
-  const methodt &m)
+  const irep_idt &method_identifier,
+  const java_bytecode_parse_treet::methodt &m,
+  symbol_tablet &symbol_table)
 {
+  symbolt method_symbol;
   typet member_type=java_type_from_string(m.signature);
 
-  assert(member_type.id()==ID_code);
-
-  const irep_idt method_identifier=
-    id2string(class_symbol.name)+"."+id2string(m.name)+":"+m.signature;
-  method_id=method_identifier;
+  method_symbol.name=method_identifier;
+  method_symbol.base_name=m.base_name;
+  method_symbol.mode=ID_java;
+  method_symbol.location=m.source_location;
+  method_symbol.location.set_function(method_identifier);
 
-  code_typet &code_type=to_code_type(member_type);
-  method_return_type=code_type.return_type();
-  code_typet::parameterst &parameters=code_type.parameters();
+  if(method_symbol.base_name=="<init>")
+  {
+    method_symbol.pretty_name=
+      id2string(class_symbol.pretty_name)+"."+
+      id2string(class_symbol.base_name)+"()";
+    member_type.set(ID_constructor, true);
+  }
+  else
+    method_symbol.pretty_name=
+      id2string(class_symbol.pretty_name)+"."+
+      id2string(m.base_name)+"()";
 
   // do we need to add 'this' as a parameter?
   if(!m.is_static)
   {
+    code_typet &code_type=to_code_type(member_type);
+    code_typet::parameterst &parameters=code_type.parameters();
     code_typet::parametert this_p;
-    const reference_typet object_ref_type(
-      symbol_typet(class_symbol.name));
+    const reference_typet object_ref_type(symbol_typet(class_symbol.name));
     this_p.type()=object_ref_type;
     this_p.set_this();
     parameters.insert(parameters.begin(), this_p);
   }
 
+  method_symbol.type=member_type;
+  symbol_table.add(method_symbol);
+}
+
+/*******************************************************************\
+
+Function: java_bytecode_convert_methodt::convert
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void java_bytecode_convert_methodt::convert(
+  const symbolt &class_symbol,
+  const methodt &m)
+{
+  const irep_idt method_identifier=
+    id2string(class_symbol.name)+"."+id2string(m.name)+":"+m.signature;
+  method_id=method_identifier;
+
+  const auto &old_sym=symbol_table.lookup(method_identifier);
+
+  typet member_type=old_sym.type;
+  code_typet &code_type=to_code_type(member_type);
+  method_return_type=code_type.return_type();
+  code_typet::parameterst &parameters=code_type.parameters();
+
   variables.clear();
 
   // find parameter names in the local variable table:
@@ -343,10 +393,10 @@ void java_bytecode_convert_methodt::convert(
   if((!m.is_abstract) && (!m.is_native))
     method_symbol.value=convert_instructions(m, code_type);
 
-  // do we have the method symbol already?
+  // Replace the existing stub symbol with the real deal:
   const auto s_it=symbol_table.symbols.find(method.get_name());
-  if(s_it!=symbol_table.symbols.end())
-    symbol_table.symbols.erase(s_it); // erase, we stubbed it
+  assert(s_it!=symbol_table.symbols.end());
+  symbol_table.symbols.erase(s_it);
 
   symbol_table.add(method_symbol);
 }
@@ -1033,7 +1083,11 @@ codet java_bytecode_convert_methodt::convert_instructions(
           {
             if(as_string(arg0.get(ID_identifier))
                .find("<init>")!=std::string::npos)
+            {
+              if(needed_classes)
+                needed_classes->insert(classname);
               code_type.set(ID_constructor, true);
+            }
             else
               code_type.set(ID_java_super_method_call, true);
           }
@@ -1115,11 +1169,15 @@ codet java_bytecode_convert_methodt::convert_instructions(
         assert(use_this);
         assert(!call.arguments().empty());
         call.function()=arg0;
+        // Populate needed methods later,
+        // once we know what object types can exist.
       }
       else
       {
         // static binding
         call.function()=symbol_exprt(arg0.get(ID_identifier), arg0.type());
+        if(needed_methods)
+          needed_methods->push_back(arg0.get(ID_identifier));
       }
 
       call.function().add_source_location()=loc;
@@ -1661,6 +1719,11 @@ codet java_bytecode_convert_methodt::convert_instructions(
       symbol_exprt symbol_expr(arg0.type());
       const auto &field_name=arg0.get_string(ID_component_name);
       symbol_expr.set_identifier(arg0.get_string(ID_class)+"."+field_name);
+      if(needed_classes && arg0.type().id()==ID_symbol)
+      {
+        needed_classes->insert(
+          to_symbol_type(arg0.type()).get_identifier());
+      }
       results[0]=java_bytecode_promotion(symbol_expr);
 
       // set $assertionDisabled to false
@@ -1678,6 +1741,11 @@ codet java_bytecode_convert_methodt::convert_instructions(
       symbol_exprt symbol_expr(arg0.type());
       const auto &field_name=arg0.get_string(ID_component_name);
       symbol_expr.set_identifier(arg0.get_string(ID_class)+"."+field_name);
+      if(needed_classes && arg0.type().id()==ID_symbol)
+      {
+        needed_classes->insert(
+          to_symbol_type(arg0.type()).get_identifier());
+      }
       c=code_assignt(symbol_expr, op[0]);
     }
     else if(statement==patternt("?2?")) // i2c etc.
@@ -2140,13 +2208,17 @@ void java_bytecode_convert_method(
   symbol_tablet &symbol_table,
   message_handlert &message_handler,
   bool disable_runtime_checks,
-  size_t max_array_length)
+  size_t max_array_length,
+  safe_pointer<std::vector<irep_idt> > needed_methods,
+  safe_pointer<std::set<irep_idt> > needed_classes)
 {
   java_bytecode_convert_methodt java_bytecode_convert_method(
     symbol_table,
     message_handler,
     disable_runtime_checks,
-    max_array_length);
+    max_array_length,
+    needed_methods,
+    needed_classes);
 
   java_bytecode_convert_method(class_symbol, method);
 }
diff --git a/src/java_bytecode/java_bytecode_convert_method.h b/src/java_bytecode/java_bytecode_convert_method.h
index 8945af95bd1..e81881f44e1 100644
--- a/src/java_bytecode/java_bytecode_convert_method.h
+++ b/src/java_bytecode/java_bytecode_convert_method.h
@@ -11,15 +11,46 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/symbol_table.h>
 #include <util/message.h>
+#include <util/safe_pointer.h>
 
 #include "java_bytecode_parse_tree.h"
 
+class class_hierarchyt;
+
 void java_bytecode_convert_method(
   const symbolt &class_symbol,
   const java_bytecode_parse_treet::methodt &,
   symbol_tablet &symbol_table,
   message_handlert &message_handler,
   bool disable_runtime_checks,
-  size_t max_array_length);
+  size_t max_array_length,
+  safe_pointer<std::vector<irep_idt> > needed_methods,
+  safe_pointer<std::set<irep_idt> > needed_classes);
+
+// Must provide both the optional parameters or neither.
+inline void java_bytecode_convert_method(
+  const symbolt &class_symbol,
+  const java_bytecode_parse_treet::methodt &method,
+  symbol_tablet &symbol_table,
+  message_handlert &message_handler,
+  bool disable_runtime_checks,
+  size_t max_array_length)
+{
+  java_bytecode_convert_method(
+    class_symbol,
+    method,
+    symbol_table,
+    message_handler,
+    disable_runtime_checks,
+    max_array_length,
+    safe_pointer<std::vector<irep_idt> >::create_null(),
+    safe_pointer<std::set<irep_idt> >::create_null());
+}
+
+void java_bytecode_convert_method_lazy(
+  const symbolt &class_symbol,
+  const irep_idt &method_identifier,
+  const java_bytecode_parse_treet::methodt &,
+  symbol_tablet &symbol_table);
 
 #endif // CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_CONVERT_METHOD_H
diff --git a/src/java_bytecode/java_bytecode_convert_method_class.h b/src/java_bytecode/java_bytecode_convert_method_class.h
index 43f51269aab..0d5476d12f7 100644
--- a/src/java_bytecode/java_bytecode_convert_method_class.h
+++ b/src/java_bytecode/java_bytecode_convert_method_class.h
@@ -13,8 +13,10 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/message.h>
 #include <util/std_types.h>
 #include <util/std_expr.h>
+#include <util/safe_pointer.h>
 #include <analyses/cfg_dominators.h>
 #include "java_bytecode_parse_tree.h"
+#include "java_bytecode_convert_class.h"
 
 #include <vector>
 #include <list>
@@ -29,11 +31,15 @@ class java_bytecode_convert_methodt:public messaget
     symbol_tablet &_symbol_table,
     message_handlert &_message_handler,
     bool _disable_runtime_checks,
-    size_t _max_array_length):
+    size_t _max_array_length,
+    safe_pointer<std::vector<irep_idt> > _needed_methods,
+    safe_pointer<std::set<irep_idt> > _needed_classes):
     messaget(_message_handler),
     symbol_table(_symbol_table),
     disable_runtime_checks(_disable_runtime_checks),
-    max_array_length(_max_array_length)
+    max_array_length(_max_array_length),
+    needed_methods(_needed_methods),
+    needed_classes(_needed_classes)
   {
   }
 
@@ -52,6 +58,8 @@ class java_bytecode_convert_methodt:public messaget
   symbol_tablet &symbol_table;
   const bool disable_runtime_checks;
   const size_t max_array_length;
+  safe_pointer<std::vector<irep_idt> > needed_methods;
+  safe_pointer<std::set<irep_idt> > needed_classes;
 
   irep_idt method_id;
   irep_idt current_method;
diff --git a/src/java_bytecode/java_bytecode_language.cpp b/src/java_bytecode/java_bytecode_language.cpp
index 1d9d9f57b41..e9d5a87186b 100644
--- a/src/java_bytecode/java_bytecode_language.cpp
+++ b/src/java_bytecode/java_bytecode_language.cpp
@@ -14,8 +14,11 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/cmdline.h>
 #include <util/string2int.h>
 
+#include <goto-programs/class_hierarchy.h>
+
 #include "java_bytecode_language.h"
 #include "java_bytecode_convert_class.h"
+#include "java_bytecode_convert_method.h"
 #include "java_bytecode_internal_additions.h"
 #include "java_bytecode_typecheck.h"
 #include "java_entry_point.h"
@@ -45,6 +48,12 @@ void java_bytecode_languaget::get_language_options(const cmdlinet &cmd)
       std::stoi(cmd.get_value("java-max-input-array-length"));
   if(cmd.isset("java-max-vla-length"))
     max_user_array_length=std::stoi(cmd.get_value("java-max-vla-length"));
+  if(cmd.isset("lazy-methods-context-sensitive"))
+    lazy_methods_mode=LAZY_METHODS_MODE_CONTEXT_SENSITIVE;
+  else if(cmd.isset("lazy-methods"))
+    lazy_methods_mode=LAZY_METHODS_MODE_CONTEXT_INSENSITIVE;
+  else
+    lazy_methods_mode=LAZY_METHODS_MODE_EAGER;
 }
 
 /*******************************************************************\
@@ -147,6 +156,8 @@ bool java_bytecode_languaget::parse(
     {
       status() << "JAR file without entry point: loading it all" << eom;
       java_class_loader.load_entire_jar(path);
+      for(const auto &kv : java_class_loader.jar_map.at(path).entries)
+        main_jar_classes.push_back(kv.first);
     }
     else
       java_class_loader.add_jar_file(path);
@@ -170,6 +181,287 @@ bool java_bytecode_languaget::parse(
 
 /*******************************************************************\
 
+Function: get_virtual_method_target
+
+  Inputs: `needed_classes`: set of classes that can be instantiated.
+            Any potential callee not in this set will be ignored.
+          `call_basename`: unqualified function name with type
+            signature (e.g. "f:(I)")
+          `classname`: class name that may define or override a
+            function named `call_basename`.
+          `symbol_table`: global symtab
+
+ Outputs: Returns the fully qualified name of `classname`'s definition
+          of `call_basename` if found and `classname` is present in
+          `needed_classes`, or irep_idt() otherwise.
+
+ Purpose: Find a virtual callee, if one is defined and the callee type
+          is known to exist.
+
+\*******************************************************************/
+
+static irep_idt get_virtual_method_target(
+  const std::set<irep_idt> &needed_classes,
+  const irep_idt &call_basename,
+  const irep_idt &classname,
+  const symbol_tablet &symbol_table)
+{
+  // Program-wide, is this class ever instantiated?
+  if(!needed_classes.count(classname))
+    return irep_idt();
+  auto methodid=id2string(classname)+"."+id2string(call_basename);
+  if(symbol_table.has_symbol(methodid))
+    return methodid;
+  else
+    return irep_idt();
+}
+
+/*******************************************************************\
+
+Function: get_virtual_method_target
+
+  Inputs: `c`: function call whose potential target functions should
+            be determined.
+          `needed_classes`: set of classes that can be instantiated.
+            Any potential callee not in this set will be ignored.
+          `symbol_table`: global symtab
+          `class_hierarchy`: global class hierarchy
+
+ Outputs: Populates `needed_methods` with all possible `c` callees,
+          taking `needed_classes` into account (virtual function
+          overrides defined on classes that are not 'needed' are
+          ignored)
+
+ Purpose: Find possible callees, excluding types that are not known
+          to be instantiated.
+
+\*******************************************************************/
+
+static void get_virtual_method_targets(
+  const code_function_callt &c,
+  const std::set<irep_idt> &needed_classes,
+  std::vector<irep_idt> &needed_methods,
+  symbol_tablet &symbol_table,
+  const class_hierarchyt &class_hierarchy)
+{
+  const auto &called_function=c.function();
+  assert(called_function.id()==ID_virtual_function);
+
+  const auto &call_class=called_function.get(ID_C_class);
+  assert(call_class!=irep_idt());
+  const auto &call_basename=called_function.get(ID_component_name);
+  assert(call_basename!=irep_idt());
+
+  auto old_size=needed_methods.size();
+
+  auto child_classes=class_hierarchy.get_children_trans(call_class);
+  for(const auto &child_class : child_classes)
+  {
+    auto child_method=
+      get_virtual_method_target(
+        needed_classes,
+        call_basename,
+        child_class,
+        symbol_table);
+    if(child_method!=irep_idt())
+      needed_methods.push_back(child_method);
+  }
+
+  irep_idt parent_class_id=call_class;
+  while(1)
+  {
+    auto parent_method=
+      get_virtual_method_target(
+        needed_classes,
+        call_basename,
+        parent_class_id,
+        symbol_table);
+    if(parent_method!=irep_idt())
+    {
+      needed_methods.push_back(parent_method);
+      break;
+    }
+    else
+    {
+      auto findit=class_hierarchy.class_map.find(parent_class_id);
+      if(findit==class_hierarchy.class_map.end())
+        break;
+      else
+      {
+        const auto &entry=findit->second;
+        if(entry.parents.empty())
+          break;
+        else
+          parent_class_id=entry.parents[0];
+      }
+    }
+  }
+
+  if(needed_methods.size()==old_size)
+  {
+    // Didn't find any candidate callee. Generate a stub.
+    std::string stubname=id2string(call_class)+"."+id2string(call_basename);
+    symbolt symbol;
+    symbol.name=stubname;
+    symbol.base_name=call_basename;
+    symbol.type=c.function().type();
+    symbol.value.make_nil();
+    symbol.mode=ID_java;
+    symbol_table.add(symbol);
+  }
+}
+
+/*******************************************************************\
+
+Function: gather_virtual_callsites
+
+  Inputs: `e`: expression tree to search
+
+ Outputs: Populates `result` with pointers to each function call
+            within e that calls a virtual function.
+
+ Purpose: See output
+
+\*******************************************************************/
+
+static void gather_virtual_callsites(
+  const exprt &e,
+  std::vector<const code_function_callt *> &result)
+{
+  if(e.id()!=ID_code)
+    return;
+  const codet &c=to_code(e);
+  if(c.get_statement()==ID_function_call &&
+     to_code_function_call(c).function().id()==ID_virtual_function)
+    result.push_back(&to_code_function_call(c));
+  else
+    forall_operands(it, e)
+      gather_virtual_callsites(*it, result);
+}
+
+/*******************************************************************\
+
+Function: gather_needed_globals
+
+  Inputs: `e`: expression tree to search
+          `symbol_table`: global symtab
+
+ Outputs: Populates `needed` with global variable symbols referenced
+          from `e` or its children.
+
+ Purpose: See output
+
+\*******************************************************************/
+
+static void gather_needed_globals(
+  const exprt &e,
+  const symbol_tablet &symbol_table,
+  symbol_tablet &needed)
+{
+  if(e.id()==ID_symbol)
+  {
+    const auto &sym=symbol_table.lookup(to_symbol_expr(e).get_identifier());
+    if(sym.is_static_lifetime)
+      needed.add(sym);
+  }
+  else
+    forall_operands(opit, e)
+      gather_needed_globals(*opit, symbol_table, needed);
+}
+
+/*******************************************************************\
+
+Function: gather_field_types
+
+  Inputs: `class_type`: root of class tree to search
+          `ns`: global namespace
+
+ Outputs: Populates `needed_classes` with all Java reference types
+            reachable starting at `class_type`. For example if
+            `class_type` is `symbol_typet("java::A")` and A has a B
+            field, then `B` (but not `A`) will be added to
+            `needed_classes`.
+
+ Purpose: See output
+
+\*******************************************************************/
+
+static void gather_field_types(
+  const typet &class_type,
+  const namespacet &ns,
+  std::set<irep_idt> &needed_classes)
+{
+  const auto &underlying_type=to_struct_type(ns.follow(class_type));
+  for(const auto &field : underlying_type.components())
+  {
+    if(field.type().id()==ID_struct || field.type().id()==ID_symbol)
+      gather_field_types(field.type(), ns, needed_classes);
+    else if(field.type().id()==ID_pointer)
+    {
+      // Skip array primitive pointers, for example:
+      if(field.type().subtype().id()!=ID_symbol)
+        continue;
+      const auto &field_classid=
+        to_symbol_type(field.type().subtype()).get_identifier();
+      if(needed_classes.insert(field_classid).second)
+        gather_field_types(field.type().subtype(), ns, needed_classes);
+    }
+  }
+}
+
+/*******************************************************************\
+
+Function: initialize_needed_classes
+
+  Inputs: `entry_points`: list of fully-qualified function names that
+            we should assume are reachable
+          `ns`: global namespace
+          `ch`: global class hierarchy
+
+ Outputs: Populates `needed_classes` with all Java reference types
+            whose references may be passed, directly or indirectly,
+            to any of the functions in `entry_points`.
+
+ Purpose: See output
+
+\*******************************************************************/
+
+static void initialize_needed_classes(
+  const std::vector<irep_idt> &entry_points,
+  const namespacet &ns,
+  const class_hierarchyt &ch,
+  std::set<irep_idt> &needed_classes)
+{
+  for(const auto &mname : entry_points)
+  {
+    const auto &symbol=ns.lookup(mname);
+    const auto &mtype=to_code_type(symbol.type);
+    for(const auto &param : mtype.parameters())
+    {
+      if(param.type().id()==ID_pointer)
+      {
+        const auto &param_classid=
+          to_symbol_type(param.type().subtype()).get_identifier();
+        std::vector<irep_idt> class_and_parents=
+          ch.get_parents_trans(param_classid);
+        class_and_parents.push_back(param_classid);
+        for(const auto &classid : class_and_parents)
+          needed_classes.insert(classid);
+        gather_field_types(param.type().subtype(), ns, needed_classes);
+      }
+    }
+  }
+
+  // Also add classes whose instances are magically
+  // created by the JVM and so won't be spotted by
+  // looking for constructors and calls as usual:
+  needed_classes.insert("java::java.lang.String");
+  needed_classes.insert("java::java.lang.Class");
+  needed_classes.insert("java::java.lang.Object");
+}
+
+/*******************************************************************\
+
 Function: java_bytecode_languaget::typecheck
 
   Inputs:
@@ -200,7 +492,18 @@ bool java_bytecode_languaget::typecheck(
          symbol_table,
          get_message_handler(),
          disable_runtime_checks,
-         max_user_array_length))
+         max_user_array_length,
+         lazy_methods,
+         lazy_methods_mode))
+      return true;
+  }
+
+  // Now incrementally elaborate methods
+  // that are reachable from this entry point.
+  if(lazy_methods_mode==LAZY_METHODS_MODE_CONTEXT_INSENSITIVE)
+  {
+    // ci: context-insensitive.
+    if(do_ci_lazy_method_conversion(symbol_table, lazy_methods))
       return true;
   }
 
@@ -214,6 +517,221 @@ bool java_bytecode_languaget::typecheck(
 
 /*******************************************************************\
 
+Function: java_bytecode_languaget::do_ci_lazy_method_conversion
+
+  Inputs: `symbol_table`: global symbol table
+          `lazy_methods`: map from method names to relevant symbol
+                          and parsed-method objects.
+
+ Outputs: Elaborates lazily-converted methods that may be reachable
+          starting from the main entry point (usually provided with
+          the --function command-line option) (side-effect on the
+          symbol_table). Returns false on success.
+
+ Purpose: Uses a simple context-insensitive ('ci') analysis to
+          determine which methods may be reachable from the main
+          entry point. In brief, static methods are reachable if we
+          find a callsite in another reachable site, while virtual
+          methods are reachable if we find a virtual callsite
+          targeting a compatible type *and* a constructor callsite
+          indicating an object of that type may be instantiated (or
+          evidence that an object of that type exists before the
+          main function is entered, such as being passed as a
+          parameter).
+
+\*******************************************************************/
+
+bool java_bytecode_languaget::do_ci_lazy_method_conversion(
+  symbol_tablet &symbol_table,
+  lazy_methodst &lazy_methods)
+{
+  class_hierarchyt ch;
+  ch(symbol_table);
+
+  std::vector<irep_idt> method_worklist1;
+  std::vector<irep_idt> method_worklist2;
+
+  auto main_function=
+    get_main_symbol(symbol_table, main_class, get_message_handler(), true);
+  if(main_function.stop_convert)
+  {
+    // Failed, mark all functions in the given main class(es) reachable.
+    std::vector<irep_idt> reachable_classes;
+    if(!main_class.empty())
+      reachable_classes.push_back(main_class);
+    else
+      reachable_classes=main_jar_classes;
+    for(const auto &classname : reachable_classes)
+    {
+      const auto &methods=
+        java_class_loader.class_map.at(classname).parsed_class.methods;
+      for(const auto &method : methods)
+      {
+        const irep_idt methodid="java::"+id2string(classname)+"."+
+          id2string(method.name)+":"+
+          id2string(method.signature);
+        method_worklist2.push_back(methodid);
+      }
+    }
+  }
+  else
+    method_worklist2.push_back(main_function.main_function.name);
+
+  std::set<irep_idt> needed_classes;
+  initialize_needed_classes(
+    method_worklist2,
+    namespacet(symbol_table),
+    ch,
+    needed_classes);
+
+  std::set<irep_idt> methods_already_populated;
+  std::vector<const code_function_callt *> virtual_callsites;
+
+  bool any_new_methods;
+  do
+  {
+    any_new_methods=false;
+    while(method_worklist2.size()!=0)
+    {
+      std::swap(method_worklist1, method_worklist2);
+      for(const auto &mname : method_worklist1)
+      {
+        if(!methods_already_populated.insert(mname).second)
+          continue;
+        auto findit=lazy_methods.find(mname);
+        if(findit==lazy_methods.end())
+        {
+          debug() << "Skip " << mname << eom;
+          continue;
+        }
+        debug() << "CI lazy methods: elaborate " << mname << eom;
+        const auto &parsed_method=findit->second;
+        java_bytecode_convert_method(
+          *parsed_method.first,
+          *parsed_method.second,
+          symbol_table,
+          get_message_handler(),
+          disable_runtime_checks,
+          max_user_array_length,
+          safe_pointer<std::vector<irep_idt> >::create_non_null(
+            &method_worklist2),
+          safe_pointer<std::set<irep_idt> >::create_non_null(
+            &needed_classes));
+        gather_virtual_callsites(
+          symbol_table.lookup(mname).value,
+          virtual_callsites);
+        any_new_methods=true;
+      }
+      method_worklist1.clear();
+    }
+
+    // Given the object types we now know may be created, populate more
+    // possible virtual function call targets:
+
+    debug() << "CI lazy methods: add virtual method targets ("
+            << virtual_callsites.size()
+            << " callsites)"
+            << eom;
+
+    for(const auto &callsite : virtual_callsites)
+    {
+      // This will also create a stub if a virtual callsite has no targets.
+      get_virtual_method_targets(
+        *callsite,
+        needed_classes,
+        method_worklist2,
+        symbol_table,
+        ch);
+    }
+  }
+  while(any_new_methods);
+
+  // Remove symbols for methods that were declared but never used:
+  symbol_tablet keep_symbols;
+
+  for(const auto &sym : symbol_table.symbols)
+  {
+    if(sym.second.is_static_lifetime)
+      continue;
+    if(lazy_methods.count(sym.first) &&
+       !methods_already_populated.count(sym.first))
+    {
+      continue;
+    }
+    if(sym.second.type.id()==ID_code)
+      gather_needed_globals(sym.second.value, symbol_table, keep_symbols);
+    keep_symbols.add(sym.second);
+  }
+
+  debug() << "CI lazy methods: removed "
+          << symbol_table.symbols.size() - keep_symbols.symbols.size()
+          << " unreachable methods and globals"
+          << eom;
+
+  symbol_table.swap(keep_symbols);
+
+  return false;
+}
+
+/*******************************************************************\
+
+Function: java_bytecode_languaget::lazy_methods_provided
+
+  Inputs: None
+
+ Outputs: Populates `methods` with the complete list of lazy methods
+          that are available to convert (those which are valid
+          parameters for `convert_lazy_method`)
+
+ Purpose: Provide feedback to `language_filest` so that when asked
+          for a lazy method, it can delegate to this instance of
+          java_bytecode_languaget.
+
+\*******************************************************************/
+
+void java_bytecode_languaget::lazy_methods_provided(
+  std::set<irep_idt> &methods) const
+{
+  for(const auto &kv : lazy_methods)
+    methods.insert(kv.first);
+}
+
+/*******************************************************************\
+
+Function: java_bytecode_languaget::convert_lazy_method
+
+  Inputs: `id`: method ID to convert
+          `symtab`: global symbol table
+
+ Outputs: Amends the symbol table entry for function `id`, which
+          should be a lazy method provided by this instance of
+          `java_bytecode_languaget`. It should initially have a nil
+          value. After this method completes, it will have a value
+          representing the method body, identical to that produced
+          using eager method conversion.
+
+ Purpose: Promote a lazy-converted method (one whose type is known
+          but whose body hasn't been converted) into a fully-
+          elaborated one.
+
+\*******************************************************************/
+
+void java_bytecode_languaget::convert_lazy_method(
+  const irep_idt &id,
+  symbol_tablet &symtab)
+{
+  const auto &lazy_method_entry=lazy_methods.at(id);
+  java_bytecode_convert_method(
+    *lazy_method_entry.first,
+    *lazy_method_entry.second,
+    symtab,
+    get_message_handler(),
+    disable_runtime_checks,
+    max_user_array_length);
+}
+
+/*******************************************************************\
+
 Function: java_bytecode_languaget::final
 
   Inputs:
diff --git a/src/java_bytecode/java_bytecode_language.h b/src/java_bytecode/java_bytecode_language.h
index 5937f6f4fd4..ea177e0226a 100644
--- a/src/java_bytecode/java_bytecode_language.h
+++ b/src/java_bytecode/java_bytecode_language.h
@@ -16,6 +16,20 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #define MAX_NONDET_ARRAY_LENGTH_DEFAULT 5
 
+enum lazy_methods_modet
+{
+  LAZY_METHODS_MODE_EAGER,
+  LAZY_METHODS_MODE_CONTEXT_INSENSITIVE,
+  LAZY_METHODS_MODE_CONTEXT_SENSITIVE
+};
+
+typedef std::pair<
+          const symbolt *,
+          const java_bytecode_parse_treet::methodt *>
+  lazy_method_valuet;
+typedef std::map<irep_idt, lazy_method_valuet>
+  lazy_methodst;
+
 class java_bytecode_languaget:public languaget
 {
 public:
@@ -69,9 +83,15 @@ class java_bytecode_languaget:public languaget
   std::set<std::string> extensions() const override;
 
   void modules_provided(std::set<std::string> &modules) override;
+  virtual void lazy_methods_provided(std::set<irep_idt> &) const override;
+  virtual void convert_lazy_method(
+    const irep_idt &id, symbol_tablet &) override;
 
 protected:
+  bool do_ci_lazy_method_conversion(symbol_tablet &, lazy_methodst &);
+
   irep_idt main_class;
+  std::vector<irep_idt> main_jar_classes;
   java_class_loadert java_class_loader;
   bool assume_inputs_non_null;      // assume inputs variables to be non-null
 
@@ -82,6 +102,8 @@ class java_bytecode_languaget:public languaget
                                     //  - array size for newarray
   size_t max_nondet_array_length;   // maximal length for non-det array creation
   size_t max_user_array_length;     // max size for user code created arrays
+  lazy_methodst lazy_methods;
+  lazy_methods_modet lazy_methods_mode;
 };
 
 languaget *new_java_bytecode_language();
diff --git a/src/java_bytecode/java_class_loader.h b/src/java_bytecode/java_class_loader.h
index d3fcdd62810..b96097c504d 100644
--- a/src/java_bytecode/java_class_loader.h
+++ b/src/java_bytecode/java_class_loader.h
@@ -37,7 +37,6 @@ class java_class_loadert:public messaget
 
   jar_poolt jar_pool;
 
-protected:
   class jar_map_entryt
   {
   public:
diff --git a/src/java_bytecode/java_entry_point.cpp b/src/java_bytecode/java_entry_point.cpp
index d4d40beff3b..3a687ad57f6 100644
--- a/src/java_bytecode/java_entry_point.cpp
+++ b/src/java_bytecode/java_entry_point.cpp
@@ -326,11 +326,11 @@ void java_record_outputs(
   }
 }
 
-
 main_function_resultt get_main_symbol(
   symbol_tablet &symbol_table,
   const irep_idt &main_class,
-  message_handlert &message_handler)
+  message_handlert &message_handler,
+  bool allow_no_body)
 {
   symbolt symbol;
   main_function_resultt res;
@@ -414,7 +414,7 @@ main_function_resultt get_main_symbol(
     }
 
     // check if it has a body
-    if(symbol.value.is_nil())
+    if(symbol.value.is_nil() && !allow_no_body)
     {
       message.error() << "main method `" << main_class
                       << "' has no body" << messaget::eom;
@@ -479,7 +479,7 @@ main_function_resultt get_main_symbol(
     symbol=symbol_table.symbols.find(*matches.begin())->second;
 
     // check if it has a body
-    if(symbol.value.is_nil())
+    if(symbol.value.is_nil() && !allow_no_body)
     {
       message.error() << "main method `" << main_class
                       << "' has no body" << messaget::eom;
diff --git a/src/java_bytecode/java_entry_point.h b/src/java_bytecode/java_entry_point.h
index 7fa562de89a..e6575734d80 100644
--- a/src/java_bytecode/java_entry_point.h
+++ b/src/java_bytecode/java_entry_point.h
@@ -28,6 +28,7 @@ typedef struct
 main_function_resultt get_main_symbol(
   symbol_tablet &symbol_table,
   const irep_idt &main_class,
-  message_handlert &);
+  message_handlert &,
+  bool allow_no_body=false);
 
 #endif // CPROVER_JAVA_BYTECODE_JAVA_ENTRY_POINT_H
diff --git a/src/langapi/language_ui.cpp b/src/langapi/language_ui.cpp
index 3775c3c6125..45198cbffd2 100644
--- a/src/langapi/language_ui.cpp
+++ b/src/langapi/language_ui.cpp
@@ -104,8 +104,8 @@ bool language_uit::parse(const std::string &filename)
     return true;
   }
 
-  std::pair<language_filest::filemapt::iterator, bool>
-    result=language_files.filemap.insert(
+  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;
diff --git a/src/util/language.h b/src/util/language.h
index edd83471cd5..b19615496ec 100644
--- a/src/util/language.h
+++ b/src/util/language.h
@@ -49,6 +49,15 @@ class languaget:public messaget
   virtual void modules_provided(std::set<std::string> &modules)
   { }
 
+  // add lazy functions provided to set
+
+  virtual void lazy_methods_provided(std::set<irep_idt> &methods) const
+  { }
+
+  // populate a lazy method
+  virtual void convert_lazy_method(const irep_idt &id, symbol_tablet &)
+  { }
+
   // final adjustments, e.g., initialization and call to main()
 
   virtual bool final(
diff --git a/src/util/language_file.cpp b/src/util/language_file.cpp
index f7a49991d63..efd7b8d53b6 100644
--- a/src/util/language_file.cpp
+++ b/src/util/language_file.cpp
@@ -64,6 +64,13 @@ void language_filet::get_modules()
   language->modules_provided(modules);
 }
 
+void language_filet::convert_lazy_method(
+  const irep_idt &id,
+  symbol_tablet &symbol_table)
+{
+  language->convert_lazy_method(id, symbol_table);
+}
+
 /*******************************************************************\
 
 Function: language_filest::show_parse
@@ -78,8 +85,8 @@ Function: language_filest::show_parse
 
 void language_filest::show_parse(std::ostream &out)
 {
-  for(filemapt::iterator it=filemap.begin();
-      it!=filemap.end(); it++)
+  for(file_mapt::iterator it=file_map.begin();
+      it!=file_map.end(); it++)
     it->second.language->show_parse(out);
 }
 
@@ -97,8 +104,8 @@ Function: language_filest::parse
 
 bool language_filest::parse()
 {
-  for(filemapt::iterator it=filemap.begin();
-      it!=filemap.end(); it++)
+  for(file_mapt::iterator it=file_map.begin();
+      it!=file_map.end(); it++)
   {
     // open file
 
@@ -144,8 +151,8 @@ bool language_filest::typecheck(symbol_tablet &symbol_table)
 {
   // typecheck interfaces
 
-  for(filemapt::iterator it=filemap.begin();
-      it!=filemap.end(); it++)
+  for(file_mapt::iterator it=file_map.begin();
+      it!=file_map.end(); it++)
   {
     if(it->second.language->interfaces(symbol_table))
       return true;
@@ -155,8 +162,8 @@ bool language_filest::typecheck(symbol_tablet &symbol_table)
 
   unsigned collision_counter=0;
 
-  for(filemapt::iterator fm_it=filemap.begin();
-      fm_it!=filemap.end(); fm_it++)
+  for(file_mapt::iterator fm_it=file_map.begin();
+      fm_it!=file_map.end(); fm_it++)
   {
     const language_filet::modulest &modules=
       fm_it->second.modules;
@@ -169,7 +176,7 @@ bool language_filest::typecheck(symbol_tablet &symbol_table)
       // these may collide, and then get renamed
       std::string module_name=*mo_it;
 
-      while(modulemap.find(module_name)!=modulemap.end())
+      while(module_map.find(module_name)!=module_map.end())
       {
         module_name=*mo_it+"#"+std::to_string(collision_counter);
         collision_counter++;
@@ -178,25 +185,34 @@ bool language_filest::typecheck(symbol_tablet &symbol_table)
       language_modulet module;
       module.file=&fm_it->second;
       module.name=module_name;
-      modulemap.insert(
+      module_map.insert(
         std::pair<std::string, language_modulet>(module.name, module));
     }
   }
 
   // typecheck files
 
-  for(filemapt::iterator it=filemap.begin();
-      it!=filemap.end(); it++)
+  for(file_mapt::iterator it=file_map.begin();
+      it!=file_map.end(); it++)
   {
     if(it->second.modules.empty())
+    {
       if(it->second.language->typecheck(symbol_table, ""))
         return true;
+      // register lazy methods.
+      // TODO: learn about modules and generalise this
+      // to module-providing languages if required.
+      std::set<irep_idt> lazy_method_ids;
+      it->second.language->lazy_methods_provided(lazy_method_ids);
+      for(const auto &id : lazy_method_ids)
+        lazy_method_map[id]=&it->second;
+    }
   }
 
   // typecheck modules
 
-  for(modulemapt::iterator it=modulemap.begin();
-      it!=modulemap.end(); it++)
+  for(module_mapt::iterator it=module_map.begin();
+      it!=module_map.end(); it++)
   {
     if(typecheck_module(symbol_table, it->second))
       return true;
@@ -222,8 +238,8 @@ bool language_filest::final(
 {
   std::set<std::string> languages;
 
-  for(filemapt::iterator it=filemap.begin();
-      it!=filemap.end(); it++)
+  for(file_mapt::iterator it=file_map.begin();
+      it!=file_map.end(); it++)
   {
     if(languages.insert(it->second.language->id()).second)
       if(it->second.language->final(symbol_table))
@@ -248,8 +264,8 @@ Function: language_filest::interfaces
 bool language_filest::interfaces(
   symbol_tablet &symbol_table)
 {
-  for(filemapt::iterator it=filemap.begin();
-      it!=filemap.end(); it++)
+  for(file_mapt::iterator it=file_map.begin();
+      it!=file_map.end(); it++)
   {
     if(it->second.language->interfaces(symbol_table))
       return true;
@@ -276,9 +292,9 @@ bool language_filest::typecheck_module(
 {
   // check module map
 
-  modulemapt::iterator it=modulemap.find(module);
+  module_mapt::iterator it=module_map.find(module);
 
-  if(it==modulemap.end())
+  if(it==module_map.end())
   {
     error() << "found no file that provides module " << module << eom;
     return true;
diff --git a/src/util/language_file.h b/src/util/language_file.h
index 533e8d5240e..d3184d48697 100644
--- a/src/util/language_file.h
+++ b/src/util/language_file.h
@@ -42,6 +42,10 @@ class language_filet
 
   void get_modules();
 
+  void convert_lazy_method(
+    const irep_idt &id,
+    symbol_tablet &symbol_table);
+
   language_filet(const language_filet &rhs);
 
   language_filet():language(NULL)
@@ -54,15 +58,21 @@ class language_filet
 class language_filest:public messaget
 {
 public:
-  typedef std::map<std::string, language_filet> filemapt;
-  filemapt filemap;
+  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;
 
-  typedef std::map<std::string, language_modulet> modulemapt;
-  modulemapt modulemap;
+  // Contains pointers into filemapt!
+  // 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;
 
   void clear_files()
   {
-    filemap.clear();
+    file_map.clear();
   }
 
   bool parse();
@@ -75,10 +85,26 @@ 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);
+  }
+
+  // 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.
+  void convert_lazy_method(
+    const irep_idt &id,
+    symbol_tablet &symbol_table)
+  {
+    return lazy_method_map.at(id)->convert_lazy_method(id, symbol_table);
+  }
+
   void clear()
   {
-    filemap.clear();
-    modulemap.clear();
+    file_map.clear();
+    module_map.clear();
+    lazy_method_map.clear();
   }
 
 protected:
diff --git a/src/util/safe_pointer.h b/src/util/safe_pointer.h
new file mode 100644
index 00000000000..47e52ac13fe
--- /dev/null
+++ b/src/util/safe_pointer.h
@@ -0,0 +1,64 @@
+/*******************************************************************\
+
+Module: Simple checked pointers
+
+Author: Chris Smowton, chris@smowton.net
+
+\*******************************************************************/
+
+#ifndef CPROVER_UTIL_SAFE_POINTER_H
+#define CPROVER_UTIL_SAFE_POINTER_H
+
+template<class T> class safe_pointer
+{
+ public:
+  operator bool() const
+  {
+    return !!ptr;
+  }
+
+  T *get() const
+  {
+    assert(ptr && "dereferenced a null safe pointer");
+    return ptr;
+  }
+
+  T &operator*() const
+  {
+    return *get();
+  }
+
+  T *operator->() const
+  {
+    return get();
+  }
+
+  static safe_pointer<T> create_null()
+  {
+    return safe_pointer();
+  }
+
+  static safe_pointer<T> create_non_null(
+    T *target)
+  {
+    assert(target && "initialized safe pointer with null");
+    return safe_pointer(target);
+  }
+
+  static safe_pointer<T> create_maybe_null(
+    T *target)
+  {
+    return safe_pointer(target);
+  }
+
+ protected:
+  T *ptr;
+
+  explicit safe_pointer(T *target) : ptr(target)
+  {}
+
+  safe_pointer() : ptr(nullptr)
+  {}
+};
+
+#endif