diff --git a/regression/cbmc-java/remove_virtual_function_typecast/VirtualFunctions$A.class b/regression/cbmc-java/remove_virtual_function_typecast/VirtualFunctions$A.class
new file mode 100644
index 00000000000..ad6430af4c8
Binary files /dev/null and b/regression/cbmc-java/remove_virtual_function_typecast/VirtualFunctions$A.class differ
diff --git a/regression/cbmc-java/remove_virtual_function_typecast/VirtualFunctions$B.class b/regression/cbmc-java/remove_virtual_function_typecast/VirtualFunctions$B.class
new file mode 100644
index 00000000000..62a2eaef1ce
Binary files /dev/null and b/regression/cbmc-java/remove_virtual_function_typecast/VirtualFunctions$B.class differ
diff --git a/regression/cbmc-java/remove_virtual_function_typecast/VirtualFunctions$C.class b/regression/cbmc-java/remove_virtual_function_typecast/VirtualFunctions$C.class
new file mode 100644
index 00000000000..60b7019fc93
Binary files /dev/null and b/regression/cbmc-java/remove_virtual_function_typecast/VirtualFunctions$C.class differ
diff --git a/regression/cbmc-java/remove_virtual_function_typecast/VirtualFunctions.class b/regression/cbmc-java/remove_virtual_function_typecast/VirtualFunctions.class
new file mode 100644
index 00000000000..6f11e3ca7fa
Binary files /dev/null and b/regression/cbmc-java/remove_virtual_function_typecast/VirtualFunctions.class differ
diff --git a/regression/cbmc-java/remove_virtual_function_typecast/VirtualFunctions.java b/regression/cbmc-java/remove_virtual_function_typecast/VirtualFunctions.java
new file mode 100644
index 00000000000..772a49a7e20
--- /dev/null
+++ b/regression/cbmc-java/remove_virtual_function_typecast/VirtualFunctions.java
@@ -0,0 +1,27 @@
+public class VirtualFunctions {
+  Object static_object;
+
+  public static class A {
+    public void f() {
+    }
+  }
+
+  public static class B extends A{
+    public void f() {
+    }
+  }
+
+  public static class C extends B {
+  }
+
+  public static void check(A a, B b, C c) {
+    // multiple possibilities, one needs a cast
+    a.f();
+
+    // single possibility, does not need a cast
+    b.f();
+
+    // single possibility, needs cast
+    c.f();
+  }
+}
diff --git a/regression/cbmc-java/remove_virtual_function_typecast/test.desc b/regression/cbmc-java/remove_virtual_function_typecast/test.desc
new file mode 100644
index 00000000000..32be1c0c99a
--- /dev/null
+++ b/regression/cbmc-java/remove_virtual_function_typecast/test.desc
@@ -0,0 +1,8 @@
+CORE
+VirtualFunctions.class
+--lazy-methods --java-max-vla-length 48 --unwind 8 --java-unwind-enum-static --trace --cover location --function VirtualFunctions.check --show-goto-functions
+ \(struct VirtualFunctions\$B \*\)a \. VirtualFunctions\$B\.f:\(\)V\(\);$
+ a \. VirtualFunctions\$A\.f:\(\)V\(\);$
+ b \. VirtualFunctions\$B\.f:\(\)V\(\);$
+ \(struct VirtualFunctions\$B \*\)c \. VirtualFunctions\$B\.f:\(\)V\(\);$
+--
diff --git a/src/goto-programs/remove_virtual_functions.cpp b/src/goto-programs/remove_virtual_functions.cpp
index 7028d0550ce..7c19e2d2071 100644
--- a/src/goto-programs/remove_virtual_functions.cpp
+++ b/src/goto-programs/remove_virtual_functions.cpp
@@ -96,6 +96,28 @@ void remove_virtual_functionst::remove_virtual_function(
     virtual_dispatch_fallback_actiont::CALL_LAST_FUNCTION);
 }
 
+/// Create a concrete function call to replace a virtual one
+/// \param call [in/out]: the function call to update
+/// \param function_symbol: the function to be called
+/// \param ns: namespace
+static void create_static_function_call(
+  code_function_callt &call,
+  const symbol_exprt &function_symbol,
+  const namespacet &ns)
+{
+  call.function() = function_symbol;
+  // Cast the `this` pointer to the correct type for the new callee:
+  const auto &callee_type =
+    to_code_type(ns.lookup(function_symbol.get_identifier()).type);
+  const code_typet::parametert *this_param = callee_type.get_this();
+  INVARIANT(
+    this_param != nullptr,
+    "Virtual function callees must have a `this` argument");
+  typet need_type = this_param->type();
+  if(!type_eq(call.arguments()[0].type(), need_type, ns))
+    call.arguments()[0].make_typecast(need_type);
+}
+
 void remove_virtual_functionst::remove_virtual_function(
   goto_programt &goto_program,
   goto_programt::targett target,
@@ -121,8 +143,10 @@ void remove_virtual_functionst::remove_virtual_function(
     if(functions.begin()->symbol_expr==symbol_exprt())
       target->make_skip();
     else
-      to_code_function_call(target->code).function()=
-        functions.begin()->symbol_expr;
+    {
+      create_static_function_call(
+        to_code_function_call(target->code), functions.front().symbol_expr, ns);
+    }
     return;
   }
 
@@ -187,18 +211,8 @@ void remove_virtual_functionst::remove_virtual_function(
       {
       // call function
         t1->make_function_call(code);
-        auto &newcall=to_code_function_call(t1->code);
-        newcall.function()=fun.symbol_expr;
-        // Cast the `this` pointer to the correct type for the new callee:
-        const auto &callee_type=
-          to_code_type(ns.lookup(fun.symbol_expr.get_identifier()).type);
-        const code_typet::parametert *this_param = callee_type.get_this();
-        INVARIANT(
-          this_param != nullptr,
-          "Virtual function callees must have a `this` argument");
-        typet need_type=this_param->type();
-        if(!type_eq(newcall.arguments()[0].type(), need_type, ns))
-          newcall.arguments()[0].make_typecast(need_type);
+        create_static_function_call(
+          to_code_function_call(t1->code), fun.symbol_expr, ns);
       }
       else
       {