diff --git a/regression/cbmc-java/virtual1/A.class b/regression/cbmc-java/virtual1/A.class
index a6cf73ebf2c..c0f32f4d5cb 100644
Binary files a/regression/cbmc-java/virtual1/A.class and b/regression/cbmc-java/virtual1/A.class differ
diff --git a/regression/cbmc-java/virtual1/B.class b/regression/cbmc-java/virtual1/B.class
index 7ec682f6a65..504fd1ed233 100644
Binary files a/regression/cbmc-java/virtual1/B.class and b/regression/cbmc-java/virtual1/B.class differ
diff --git a/regression/cbmc-java/virtual1/virtual1.class b/regression/cbmc-java/virtual1/virtual1.class
index 9bc4c3e9aa4..c237ac54264 100644
Binary files a/regression/cbmc-java/virtual1/virtual1.class and b/regression/cbmc-java/virtual1/virtual1.class differ
diff --git a/regression/cbmc-java/virtual1/virtual1.java b/regression/cbmc-java/virtual1/virtual1.java
index d3655a2a030..286b6cebb99 100644
--- a/regression/cbmc-java/virtual1/virtual1.java
+++ b/regression/cbmc-java/virtual1/virtual1.java
@@ -16,6 +16,7 @@ class virtual1
   public static void main(String[] args)
   {
     A a=new A();
+    B b=new B();
     a.f();
   }
 }
diff --git a/regression/cbmc-java/virtual2/virtual2.class b/regression/cbmc-java/virtual2/virtual2.class
index 7c6498be6d7..9d0a8b325bb 100644
Binary files a/regression/cbmc-java/virtual2/virtual2.class and b/regression/cbmc-java/virtual2/virtual2.class differ
diff --git a/regression/cbmc-java/virtual2/virtual2.java b/regression/cbmc-java/virtual2/virtual2.java
index 27f8d0a2d9f..5de1a8f8b2b 100644
--- a/regression/cbmc-java/virtual2/virtual2.java
+++ b/regression/cbmc-java/virtual2/virtual2.java
@@ -15,8 +15,9 @@ class virtual2
 {
   public static void main(String[] args)
   {
-    A a=new B();
-    a.f();
+    A a=new A();
+    A b=new B();
+    b.f();
   }
 }
 
diff --git a/regression/cbmc-java/virtual3/virtual3.class b/regression/cbmc-java/virtual3/virtual3.class
index be0a5491bbb..0fd3a06b7fc 100644
Binary files a/regression/cbmc-java/virtual3/virtual3.class and b/regression/cbmc-java/virtual3/virtual3.class differ
diff --git a/regression/cbmc-java/virtual3/virtual3.java b/regression/cbmc-java/virtual3/virtual3.java
index bb0c5890857..2f294a87a5c 100644
--- a/regression/cbmc-java/virtual3/virtual3.java
+++ b/regression/cbmc-java/virtual3/virtual3.java
@@ -1,7 +1,7 @@
 interface A
 {
   public void f();
-};
+}
 
 class B implements A
 {
@@ -9,14 +9,20 @@ public void f()
   {
     assert false;
   }
-};
+}
+
+class C implements A
+{
+  public void f(){}
+}
 
 class virtual3
 {
   public static void main(String[] args)
   {
-    A a = new B();
-    a.f();
+    A b = new B();
+    A c = new C();
+    b.f();
   }
 }
 
diff --git a/regression/cbmc-java/virtual4/virtual4.class b/regression/cbmc-java/virtual4/virtual4.class
index f64437d4b6d..3f3bdc8044f 100644
Binary files a/regression/cbmc-java/virtual4/virtual4.class and b/regression/cbmc-java/virtual4/virtual4.class differ
diff --git a/regression/cbmc-java/virtual4/virtual4.java b/regression/cbmc-java/virtual4/virtual4.java
index 146bf3119cd..5d3812708c0 100644
--- a/regression/cbmc-java/virtual4/virtual4.java
+++ b/regression/cbmc-java/virtual4/virtual4.java
@@ -20,8 +20,9 @@ class virtual4
 {
   public static void main(String[] args)
   {
-    A a = new C();
-    a.f();
+    A b = new B();
+    A c = new C();
+    c.f();
   }
 }
 
diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp
index 399caa50846..d6c776d3d6b 100644
--- a/src/goto-programs/builtin_functions.cpp
+++ b/src/goto-programs/builtin_functions.cpp
@@ -23,6 +23,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/pointer_predicates.h>
 #include <util/pointer_offset_size.h>
 #include <util/vtable.h>
+#include <util/namespace_utils.h>
 
 #include <linking/zero_initializer.h>
 
@@ -545,61 +546,33 @@ symbol_exprt get_vt(const irep_idt &class_name) {
   return symbol_exprt(vt_name, vttype);
 }
 
-const dereference_exprt cast_if_necessary(const exprt &lhs,
-    const irep_idt &ptr_class, const irep_idt &vt_class) {
-  const symbol_typet class_type(vt_class);
-  if (ptr_class == vt_class) return dereference_exprt(lhs, class_type);
-  const symbol_typet target_type(ptr_class);
-  const typecast_exprt cast(lhs, pointer_typet(target_type));
-  return dereference_exprt(cast, target_type);
-}
-
-void assign_vtpointer(goto_programt &dest, const namespacet &ns,
-    const exprt &lhs, const irep_idt &ptr_class, const irep_idt &vt_class,
-    const source_locationt &location) {
-  const symbol_exprt ptr_vt(get_vt(ptr_class));
-  const symbol_exprt vt(get_vt(vt_class));
-  const dereference_exprt lhs_ref(cast_if_necessary(lhs, ptr_class, vt_class));
-  const std::string memb_name(vtnamest::get_pointer(id2string(ptr_class)));
-  const pointer_typet ptr_vt_type(ptr_vt.type());
-  const member_exprt vtmember(lhs_ref, memb_name, ptr_vt_type);
-  const address_of_exprt vtable_ptr(vt);
-  const goto_programt::targett instr(dest.add_instruction(ASSIGN));
-  instr->source_location = location;
-  if (ptr_class == vt_class) {
-    instr->code = code_assignt(vtmember, vtable_ptr);
-  } else {
-    const typecast_exprt cast(vtable_ptr, ptr_vt_type);
-    instr->code = code_assignt(vtmember, cast);
-  }
-}
-
 bool is_type_missing(const namespacet &ns, const symbol_typet &type)
 {
   return !ns.get_symbol_table().has_symbol(type.get_identifier());
 }
 
-void assign_vtpointers(goto_programt &dest, const namespacet &ns,
-    const exprt &lhs, const symbol_typet &class_type,
-    const source_locationt &location)
+exprt &get_vt_pointer_member(struct_exprt &expr)
+{
+  // We assume the first member is vt_pointer or super class object.
+  assert(expr.has_operands());
+  exprt &op0=expr.op0();
+  if (ID_struct != op0.id()) return op0;
+  return get_vt_pointer_member(to_struct_expr(op0));
+}
+
+void set_vt_pointer(struct_exprt &expr, const namespacet &ns,
+    const symbol_typet &class_type)
 {
   if (is_type_missing(ns, class_type)) return;
   const irep_idt &class_name(class_type.get_identifier());
-  const irep_idt vtname(vtnamest::get_table(id2string(class_name)));
-  if (ns.get_symbol_table().has_symbol(vtname)) {
-    const class_typet &full_class_type(to_class_type(ns.follow(class_type)));
-    const irept::subt &bases(full_class_type.bases());
-    for (irept::subt::const_iterator it=bases.begin(); it != bases.end(); ++it) {
-      const typet &type(static_cast<const typet &>(it->find(ID_type)));
-      const symbol_typet &parent_type(to_symbol_type(type));
-      if (is_type_missing(ns, parent_type)) continue;
-      const irep_idt &parent_name(parent_type.get_identifier());
-      const irep_idt parent_vtname(vtnamest::get_table(id2string(parent_name)));
-      if(!ns.get_symbol_table().has_symbol(parent_vtname)) continue;
-      assign_vtpointer(dest, ns, lhs, parent_name, class_name, location);
-    }
-    assign_vtpointer(dest, ns, lhs, class_name, class_name, location);
-  }
+  const symbol_exprt vt(get_vt(class_name));
+  exprt &vt_pointer_member=get_vt_pointer_member(expr);
+  const typet &member_type=vt_pointer_member.type();
+  const address_of_exprt vt_pointer(vt);
+  if (type_eq(member_type, vt_pointer.type(), ns))
+    vt_pointer_member=vt_pointer;
+  else
+    vt_pointer_member=typecast_exprt(vt_pointer, member_type);
 }
 }
 
@@ -647,11 +620,10 @@ void goto_convertt::do_java_new(
   // zero-initialize the object
   dereference_exprt deref(lhs, object_type);
   exprt zero_object=zero_initializer(object_type, location, ns, get_message_handler());
+  set_vt_pointer(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;
-
-  assign_vtpointers(dest, ns, lhs, to_symbol_type(object_type), location);
 }
 
 /*******************************************************************\
diff --git a/src/java_bytecode/java_bytecode_convert.cpp b/src/java_bytecode/java_bytecode_convert.cpp
index 4db35cf72bf..5078e12b091 100644
--- a/src/java_bytecode/java_bytecode_convert.cpp
+++ b/src/java_bytecode/java_bytecode_convert.cpp
@@ -747,12 +747,8 @@ codet java_bytecode_convertt::convert_instructions(
 
       if(is_virtual)
       {
-#if 0
         const exprt &this_arg=call.arguments().front();
         call.function() = make_vtable_function(arg0, this_arg);
-#else
-        call.function() = arg0;
-#endif
       }
       else
         call.function() = arg0;
diff --git a/src/java_bytecode/java_bytecode_language.cpp b/src/java_bytecode/java_bytecode_language.cpp
index 296beac835f..cefda783ac2 100644
--- a/src/java_bytecode/java_bytecode_language.cpp
+++ b/src/java_bytecode/java_bytecode_language.cpp
@@ -160,6 +160,10 @@ bool java_bytecode_languaget::typecheck(
       return true;
   }
 
+  // Construct vtable symbols before typecheck
+  if (java_bytecode_vtable(symbol_table, module))
+    return true;
+
   // now typecheck all
   if(java_bytecode_typecheck(
        symbol_table, get_message_handler()))
diff --git a/src/java_bytecode/java_bytecode_parser.cpp b/src/java_bytecode/java_bytecode_parser.cpp
index ad5ff235673..768e5c3f06d 100644
--- a/src/java_bytecode/java_bytecode_parser.cpp
+++ b/src/java_bytecode/java_bytecode_parser.cpp
@@ -591,7 +591,7 @@ void java_bytecode_parsert::rinterfaces(classt &parsed_class)
   u2 interfaces_count=read_u2();
 
   for(unsigned i=0; i<interfaces_count; i++)
-    parsed_class.implements.push_back(pool_entry(read_u2()).s);
+    parsed_class.implements.push_back(constant(read_u2()).type().get(ID_C_base_name));
 }
 
 /*******************************************************************\
diff --git a/src/java_bytecode/java_bytecode_vtable.cpp b/src/java_bytecode/java_bytecode_vtable.cpp
index 696d42e2a36..2c025e4cd0c 100644
--- a/src/java_bytecode/java_bytecode_vtable.cpp
+++ b/src/java_bytecode/java_bytecode_vtable.cpp
@@ -16,31 +16,38 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/vtable.h>
 
 namespace {
-bool is_virtual(const class_typet::methodt &method) {
+bool is_virtual(const class_typet::methodt &method)
+{
   return method.get_bool(ID_is_virtual)
      && !method.get_bool(ID_constructor);
 }
 
-const char ID_virtual_name[] = "virtual_name";
+const char ID_virtual_name[]="virtual_name";
 
-class is_virtual_name_equalt {
+class is_virtual_name_equalt
+{
   const irep_idt &virtual_name;
 public:
   is_virtual_name_equalt(const class_typet::methodt &method) :
-      virtual_name(method.get(ID_virtual_name)) {
+      virtual_name(method.get(ID_virtual_name))
+  {
   }
-  bool operator()(const class_typet::methodt &method) const {
+  bool operator()(const class_typet::methodt &method) const
+  {
     return virtual_name == method.get(ID_virtual_name);
   }
 };
 
-class is_name_equalt {
+class is_name_equalt
+{
   const irep_idt &name;
 public:
   is_name_equalt(const irep_idt &name) :
-      name(name) {
+      name(name)
+  {
   }
-  bool operator()(const class_typet::componentt &component) const {
+  bool operator()(const class_typet::componentt &component) const
+  {
     return name == component.get_name();
   }
 };
@@ -72,16 +79,16 @@ class java_bytecode_vtable_factoryt
     const std::string &class_name=id2string(class_type.get(ID_name));
     const std::string &base_class_name=id2string(class_type.get(ID_base_name));
     const symbolt &type_symbol(get_vt_type_symbol(class_type));
-    result.name = vtnamest::get_table(class_name);
-    result.base_name = vtnamest::get_table_base(base_class_name);
-    result.pretty_name = result.base_name;
-    result.mode = type_symbol.mode;
-    result.module = module;
-    result.location = type_symbol.location;
-    result.type = symbol_typet(type_symbol.name);
-    result.is_lvalue = true;
-    result.is_state_var = true;
-    result.is_static_lifetime = true;
+    result.name=vtnamest::get_table(class_name);
+    result.base_name=vtnamest::get_table_base(base_class_name);
+    result.pretty_name=result.base_name;
+    result.mode=type_symbol.mode;
+    result.module=module;
+    result.location=type_symbol.location;
+    result.type=symbol_typet(type_symbol.name);
+    result.is_lvalue=true;
+    result.is_state_var=true;
+    result.is_static_lifetime=true;
   }
 
   bool has_component(const class_typet &vtable_type, const irep_idt &ifc_name)
@@ -108,7 +115,7 @@ class java_bytecode_vtable_factoryt
     struct_typet::componentt entry_component;
     entry_component.set_name(ifc_name);
     entry_component.set_base_name(ifc_method->get_base_name());
-    entry_component.type() = pointer_typet(implementation.type());
+    entry_component.type()=pointer_typet(implementation.type());
     vtable_type.components().push_back(entry_component);
 
     const irep_idt &impl_name(implementation.get_name());
@@ -145,8 +152,8 @@ class java_bytecode_vtable_factoryt
     const irept::subt &types,
     const class_typet::methodt &method)
   {
-    for(irept::subt::const_iterator it=types.begin();
-        it != types.end(); ++it)
+    for (irept::subt::const_iterator it=types.begin();
+         it != types.end(); ++it)
     {
       if (!has_method(*it, method)) continue;
       result.push_back(get_class_type(*it));
@@ -162,7 +169,7 @@ class java_bytecode_vtable_factoryt
     std::vector<class_typet> bases;
     extract_types(bases, class_type.bases(), method);
     //extract_types(bases, class_type.find(ID_interfaces).get_sub(), method);
-    for(std::vector<class_typet>::const_iterator b=bases.begin(); b != bases.end(); ++b)
+    for (std::vector<class_typet>::const_iterator b=bases.begin(); b != bases.end(); ++b)
       add_vtable_entry(vtable_value, *b, class_type, method);
   }
 
@@ -174,11 +181,12 @@ class java_bytecode_vtable_factoryt
   }
 
   void set_vtable_value(symbolt &vtable_symbol, const class_typet &class_type,
-      struct_exprt &vtable_value) {
+      struct_exprt &vtable_value)
+  {
     const std::string &class_name(id2string(class_type.get(ID_name)));
     const irep_idt vttype(vtnamest::get_type(class_name));
-    vtable_value.type() = symbol_typet(vttype);
-    vtable_symbol.value = vtable_value;
+    vtable_value.type()=symbol_typet(vttype);
+    vtable_symbol.value=vtable_value;
   }
 
   bool is_class_with_vt(const symbolt &symbol)
@@ -189,21 +197,21 @@ class java_bytecode_vtable_factoryt
     return symbol_table.has_symbol(vtnamest::get_type(class_name));
   }
 
-  void operator()(const std::pair<const irep_idt, symbolt> &named_symbol)
+  void operator()(const irep_idt &symbol_name)
   {
-    const symbolt &symbol(named_symbol.second);
+    const symbolt &symbol=symbol_table.lookup(symbol_name);
     if (!is_class_with_vt(symbol)) return;
     const class_typet &class_type(to_class_type(symbol.type));
-    const std::string &class_name(id2string(named_symbol.first));
+    const std::string &class_name(id2string(symbol_name));
     if (symbol_table.has_symbol(vtnamest::get_table(class_name))) return;
     symbolt vtable_symbol;
     create_vtable_symbol(vtable_symbol, class_type);
     const class_typet::methodst &methods(class_type.methods());
     struct_exprt vtable_value;
-    for (class_typet::methodst::const_iterator m=methods.begin(); m != methods.end(); ++m)
-      create_base_vtable_entries(vtable_value, class_type, *m);
-    for (class_typet::methodst::const_iterator m=methods.begin(); m != methods.end(); ++m)
-      create_vtable_entry(vtable_value, class_type, *m);
+    for (const class_typet::methodst::value_type &m : methods)
+      create_base_vtable_entries(vtable_value, class_type, m);
+    for (const class_typet::methodst::value_type &m : methods)
+      create_vtable_entry(vtable_value, class_type, m);
     set_vtable_value(vtable_symbol, class_type, vtable_value);
     assert(!symbol_table.add(vtable_symbol));
   }
@@ -228,41 +236,47 @@ bool java_bytecode_vtable(
   const std::string &module)
 {
   const symbol_tablet::symbolst &symbols(symbol_table.symbols);
+  std::vector<irep_idt> names;
+  names.reserve(symbols.size());
+  std::transform(symbols.begin(), symbols.end(), std::back_inserter(names),
+      [](const std::pair<irep_idt, symbolt> &entry)
+      { return entry.first;});
   java_bytecode_vtable_factoryt factory(symbol_table, module);
-  std::for_each(symbols.begin(), symbols.end(), factory);
+  std::for_each(names.begin(), names.end(), factory);
   return factory.has_error;
 }
 
-namespace {
+namespace
+{
 
 void create_vtable_type(const irep_idt &vt_name, symbol_tablet &symbol_table,
-    const symbolt &class_symbol) {
+    const symbolt &class_symbol)
+{
   symbolt vt_symb_type;
-  vt_symb_type.name = vt_name;
-  vt_symb_type.base_name = vtnamest::get_type_base(
+  vt_symb_type.name=vt_name;
+  vt_symb_type.base_name=vtnamest::get_type_base(
       id2string(class_symbol.base_name));
-  vt_symb_type.pretty_name = vt_symb_type.base_name;
-  vt_symb_type.mode = class_symbol.mode;
-  vt_symb_type.module = class_symbol.module;
-  vt_symb_type.location = class_symbol.location;
-  vt_symb_type.type = struct_typet();
+  vt_symb_type.pretty_name=vt_symb_type.base_name;
+  vt_symb_type.mode=class_symbol.mode;
+  vt_symb_type.module=class_symbol.module;
+  vt_symb_type.location=class_symbol.location;
+  vt_symb_type.type=struct_typet();
   vt_symb_type.type.set(ID_name, vt_symb_type.name);
-  vt_symb_type.is_type = true;
+  vt_symb_type.is_type=true;
   assert(!symbol_table.add(vt_symb_type));
 }
 
-const char ID_isvtptr[] = "is_vtptr";
+const char ID_isvtptr[]="is_vtptr";
+const char ID_vtable_pointer[]="@vtable_pointer";
 
-void add_vtable_pointer_member(
-  const irep_idt &vt_name,
-  symbolt &class_symbol)
+void add_vtable_pointer_member(const irep_idt &vt_name, symbolt &class_symbol)
 {
   struct_typet::componentt comp;
 
   comp.type()=pointer_typet(symbol_typet(vt_name));
-  comp.set_name("@vtable_pointer");
-  comp.set_base_name("@vtable_pointer");
-  comp.set_pretty_name("@vtable_pointer");
+  comp.set_name(ID_vtable_pointer);
+  comp.set_base_name(ID_vtable_pointer);
+  comp.set_pretty_name(ID_vtable_pointer);
   comp.set(ID_isvtptr, true);
 
   struct_typet &class_type=to_struct_type(class_symbol.type);
@@ -287,10 +301,9 @@ void create_vtable_symbol(
   symbol_tablet &symbol_table,
   const symbolt &class_symbol)
 {
-  const irep_idt vttype=
-    vtnamest::get_type(id2string(class_symbol.name));
-  
-  if(!symbol_table.has_symbol(vttype))
+  const irep_idt vttype=vtnamest::get_type(id2string(class_symbol.name));
+
+  if (!symbol_table.has_symbol(vttype))
     create_vtable_type(vttype, symbol_table, class_symbol);
 }
 
@@ -308,14 +321,14 @@ void create_vtable_symbol(
 
 void create_vtable_pointer(symbolt &class_symbol)
 {
-  const irep_idt vttype=
-    vtnamest::get_type(id2string(class_symbol.name));
-  
+  const irep_idt vttype=vtnamest::get_type(id2string(class_symbol.name));
+
   add_vtable_pointer_member(vttype, class_symbol);
 }
 
-namespace {
-const char NAME_SEP = '.';
+namespace
+{
+const char NAME_SEP='.';
 }
 
 /*******************************************************************
@@ -338,27 +351,27 @@ void set_virtual_name(class_typet::methodt &method)
   method.set(ID_virtual_name, virtual_name);
 }
 
-namespace {
+namespace
+{
 
-exprt get_ref(
-  const exprt &this_obj,
-  const symbol_typet &target_type)
+exprt get_ref(const exprt &this_obj, const symbol_typet &target_type)
 {
   const typet &type(this_obj.type());
   const irep_idt &type_id(type.id());
-  if(ID_symbol == type_id)
+  if (ID_symbol == type_id)
     return get_ref(address_of_exprt(this_obj), target_type);
   assert(ID_pointer == type_id);
   const typecast_exprt cast(this_obj, pointer_typet(target_type));
   return dereference_exprt(cast, target_type);
 }
 
-const char JAVA_NS[] = "java::";
+const char JAVA_NS[]="java::";
 const size_t JAVA_NS_LENGTH(6);
 const char CLS_MTD_SEP(':');
 const char NSEP('.');
 
-std::string get_full_class_name(const std::string &name) {
+std::string get_full_class_name(const std::string &name)
+{
   const bool has_prefix(name.find(JAVA_NS) != std::string::npos);
   const std::string::size_type offset(has_prefix ? JAVA_NS_LENGTH : 0);
   const std::string::size_type end(name.find_first_of(CLS_MTD_SEP, offset));
@@ -379,24 +392,28 @@ std::string get_full_class_name(const std::string &name) {
 
 \*******************************************************************/
 
-exprt make_vtable_function(
-  const exprt &func,
-  const exprt &this_obj)
+exprt make_vtable_function(const exprt &func, const exprt &this_obj)
 {
   const irep_idt &func_name(func.get(ID_identifier));
   const std::string class_id(get_full_class_name(id2string(func_name)));
 
-  //if (class_id.find("java.lang.") != std::string::npos) {
+  if (class_id.find("java.lang.") != std::string::npos)
+  {
     // TODO: Handle unavailable models!
-    //return func;
-  //}
+    // When translating a single java_bytecode_parse_treet, we don't know
+    // which classes will eventually be available yet. If we could provide
+    // access to the class loader here, we know which classes have been
+    // loaded successfully. For classes which have not been loaded, returning
+    // "func" is equivalent to an unimplemented function.
+    return func;
+  }
 
   const symbol_typet vtable_type(vtnamest::get_type(class_id));
-  const pointer_typet vtable_pointer_type(vtable_type);
+  const pointer_typet vt_ptr_type(vtable_type);
   const symbol_typet target_type(class_id);
   const exprt this_ref(get_ref(this_obj, target_type));
   const typet ref_type(this_ref.type());
-  const member_exprt vtable_member(this_ref, "@vtable_pointer", vtable_pointer_type);
+  const member_exprt vtable_member(this_ref, ID_vtable_pointer, vt_ptr_type);
   const dereference_exprt vtable(vtable_member, vtable_type); // TODO: cast?
   const pointer_typet func_ptr_type(func.type());
   const member_exprt func_ptr(vtable, func_name, func_ptr_type);
diff --git a/src/java_bytecode/java_bytecode_vtable.h b/src/java_bytecode/java_bytecode_vtable.h
index 4482c263972..157428702d1 100644
--- a/src/java_bytecode/java_bytecode_vtable.h
+++ b/src/java_bytecode/java_bytecode_vtable.h
@@ -18,10 +18,6 @@ void create_vtable_symbol(
   symbol_tablet &symbol_table,
   const class symbolt &class_symbol);
 
-code_assignt make_vtable_assignment(
-  const symbol_tablet &symbol_table,
-  const exprt &func);
-
 exprt make_vtable_function(
   const exprt &function,
   const exprt &this_obj);
@@ -29,4 +25,8 @@ exprt make_vtable_function(
 void set_virtual_name(
   class_typet::methodt &method);
 
+bool java_bytecode_vtable(
+  symbol_tablet &symbol_table,
+  const std::string &module);
+
 #endif /* CPROVER_JAVA_BYTECODE_VTABLE_H */