diff --git a/regression/cbmc-java/instanceof1/instanceof1.class b/regression/cbmc-java/instanceof1/instanceof1.class
index 8d68b98063b..31bd4c733f4 100644
Binary files a/regression/cbmc-java/instanceof1/instanceof1.class and b/regression/cbmc-java/instanceof1/instanceof1.class differ
diff --git a/regression/cbmc-java/instanceof1/instanceof1.java b/regression/cbmc-java/instanceof1/instanceof1.java
index c21806a7389..600b8da230e 100644
--- a/regression/cbmc-java/instanceof1/instanceof1.java
+++ b/regression/cbmc-java/instanceof1/instanceof1.java
@@ -2,18 +2,6 @@ class instanceof1
 {
   public static void main(String[] args)
   {
-    // absolutely everything is an Object
     assert args instanceof Object;
-    assert int.class instanceof Object;
-    
-    // args is an array
-    assert args instanceof Object[];
-    
-    // string literals are strings
-    assert "" instanceof String;
-
-    // need a negative example, too
-    Object o=new Object();
-    assert ! (o instanceof String);
   }
 };
diff --git a/regression/cbmc-java/instanceof2/instanceof2.class b/regression/cbmc-java/instanceof2/instanceof2.class
new file mode 100644
index 00000000000..c56c25e1934
Binary files /dev/null and b/regression/cbmc-java/instanceof2/instanceof2.class differ
diff --git a/regression/cbmc-java/instanceof2/instanceof2.java b/regression/cbmc-java/instanceof2/instanceof2.java
new file mode 100644
index 00000000000..dfda558a120
--- /dev/null
+++ b/regression/cbmc-java/instanceof2/instanceof2.java
@@ -0,0 +1,7 @@
+class instanceof2
+{
+  public static void main(String[] args)
+  {
+    assert int.class instanceof Object;
+  }
+};
diff --git a/regression/cbmc-java/instanceof2/test.desc b/regression/cbmc-java/instanceof2/test.desc
new file mode 100644
index 00000000000..5e10735840b
--- /dev/null
+++ b/regression/cbmc-java/instanceof2/test.desc
@@ -0,0 +1,8 @@
+KNOWNBUG
+instanceof2.class
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc-java/instanceof3/instanceof3.class b/regression/cbmc-java/instanceof3/instanceof3.class
new file mode 100644
index 00000000000..b89a0754f28
Binary files /dev/null and b/regression/cbmc-java/instanceof3/instanceof3.class differ
diff --git a/regression/cbmc-java/instanceof3/instanceof3.java b/regression/cbmc-java/instanceof3/instanceof3.java
new file mode 100644
index 00000000000..2f2f4e64a58
--- /dev/null
+++ b/regression/cbmc-java/instanceof3/instanceof3.java
@@ -0,0 +1,7 @@
+class instanceof3
+{
+  public static void main(String[] args)
+  {
+    assert args instanceof Object[];
+  }
+};
diff --git a/regression/cbmc-java/instanceof3/test.desc b/regression/cbmc-java/instanceof3/test.desc
new file mode 100644
index 00000000000..f04f943dc4d
--- /dev/null
+++ b/regression/cbmc-java/instanceof3/test.desc
@@ -0,0 +1,8 @@
+KNOWNBUG
+instanceof3.class
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc-java/instanceof4/instanceof4.class b/regression/cbmc-java/instanceof4/instanceof4.class
new file mode 100644
index 00000000000..98ea9b30545
Binary files /dev/null and b/regression/cbmc-java/instanceof4/instanceof4.class differ
diff --git a/regression/cbmc-java/instanceof4/instanceof4.java b/regression/cbmc-java/instanceof4/instanceof4.java
new file mode 100644
index 00000000000..d743c8e1054
--- /dev/null
+++ b/regression/cbmc-java/instanceof4/instanceof4.java
@@ -0,0 +1,7 @@
+class instanceof4
+{
+  public static void main(String[] args)
+  {
+    assert "" instanceof String;
+  }
+};
diff --git a/regression/cbmc-java/instanceof4/test.desc b/regression/cbmc-java/instanceof4/test.desc
new file mode 100644
index 00000000000..f4eefaaa537
--- /dev/null
+++ b/regression/cbmc-java/instanceof4/test.desc
@@ -0,0 +1,8 @@
+CORE
+instanceof4.class
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc-java/instanceof5/instanceof5.class b/regression/cbmc-java/instanceof5/instanceof5.class
new file mode 100644
index 00000000000..a0aa9a35c34
Binary files /dev/null and b/regression/cbmc-java/instanceof5/instanceof5.class differ
diff --git a/regression/cbmc-java/instanceof5/instanceof5.java b/regression/cbmc-java/instanceof5/instanceof5.java
new file mode 100644
index 00000000000..9024f606fc6
--- /dev/null
+++ b/regression/cbmc-java/instanceof5/instanceof5.java
@@ -0,0 +1,8 @@
+class instanceof5
+{
+  public static void main(String[] args)
+  {
+    Object o=new Object();
+    assert ! (o instanceof String);
+  }
+};
diff --git a/regression/cbmc-java/instanceof5/test.desc b/regression/cbmc-java/instanceof5/test.desc
new file mode 100644
index 00000000000..dd357c9f50b
--- /dev/null
+++ b/regression/cbmc-java/instanceof5/test.desc
@@ -0,0 +1,8 @@
+CORE
+instanceof5.class
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc-java/instanceof6/A.class b/regression/cbmc-java/instanceof6/A.class
new file mode 100644
index 00000000000..acdf27cdda7
Binary files /dev/null and b/regression/cbmc-java/instanceof6/A.class differ
diff --git a/regression/cbmc-java/instanceof6/B.class b/regression/cbmc-java/instanceof6/B.class
new file mode 100644
index 00000000000..aabe9227640
Binary files /dev/null and b/regression/cbmc-java/instanceof6/B.class differ
diff --git a/regression/cbmc-java/instanceof6/instanceof6.class b/regression/cbmc-java/instanceof6/instanceof6.class
new file mode 100644
index 00000000000..4c1ddb09f5c
Binary files /dev/null and b/regression/cbmc-java/instanceof6/instanceof6.class differ
diff --git a/regression/cbmc-java/instanceof6/instanceof6.java b/regression/cbmc-java/instanceof6/instanceof6.java
new file mode 100644
index 00000000000..da056ae41d0
--- /dev/null
+++ b/regression/cbmc-java/instanceof6/instanceof6.java
@@ -0,0 +1,15 @@
+class instanceof6
+{
+  public static void main(String[] args)
+  {
+    A[] as = { new A(), new B() };
+    assert(as[0] instanceof A);
+    assert(as[1] instanceof A);
+  }
+};
+
+class A {
+}
+
+class B extends A {
+}
diff --git a/regression/cbmc-java/instanceof6/test.desc b/regression/cbmc-java/instanceof6/test.desc
new file mode 100644
index 00000000000..668b11700cc
--- /dev/null
+++ b/regression/cbmc-java/instanceof6/test.desc
@@ -0,0 +1,8 @@
+CORE
+instanceof6.class
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc-java/instanceof7/A.class b/regression/cbmc-java/instanceof7/A.class
new file mode 100644
index 00000000000..9ad3a64c0b4
Binary files /dev/null and b/regression/cbmc-java/instanceof7/A.class differ
diff --git a/regression/cbmc-java/instanceof7/B.class b/regression/cbmc-java/instanceof7/B.class
new file mode 100644
index 00000000000..6ac7c46e5f8
Binary files /dev/null and b/regression/cbmc-java/instanceof7/B.class differ
diff --git a/regression/cbmc-java/instanceof7/instanceof7.class b/regression/cbmc-java/instanceof7/instanceof7.class
new file mode 100644
index 00000000000..b4c454655ec
Binary files /dev/null and b/regression/cbmc-java/instanceof7/instanceof7.class differ
diff --git a/regression/cbmc-java/instanceof7/instanceof7.java b/regression/cbmc-java/instanceof7/instanceof7.java
new file mode 100644
index 00000000000..16419ae2e48
--- /dev/null
+++ b/regression/cbmc-java/instanceof7/instanceof7.java
@@ -0,0 +1,15 @@
+class instanceof7
+{
+  public static void main(String[] args)
+  {
+    A[] as = { new A(), new B() };
+    assert(!(as[0] instanceof B));
+    assert(as[1] instanceof B);
+  }
+};
+
+class A {
+}
+
+class B extends A {
+}
diff --git a/regression/cbmc-java/instanceof7/test.desc b/regression/cbmc-java/instanceof7/test.desc
new file mode 100644
index 00000000000..d9b11281fe5
--- /dev/null
+++ b/regression/cbmc-java/instanceof7/test.desc
@@ -0,0 +1,8 @@
+CORE
+instanceof7.class
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
index 87a9c969981..d09b544c678 100644
--- a/src/cbmc/cbmc_parse_options.cpp
+++ b/src/cbmc/cbmc_parse_options.cpp
@@ -22,6 +22,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <goto-programs/goto_convert_functions.h>
 #include <goto-programs/remove_function_pointers.h>
 #include <goto-programs/remove_virtual_functions.h>
+#include <goto-programs/remove_instanceof.h>
 #include <goto-programs/remove_returns.h>
 #include <goto-programs/remove_vector.h>
 #include <goto-programs/remove_complex.h>
@@ -884,7 +885,10 @@ bool cbmc_parse_optionst::process_goto_program(
       symbol_table,
       goto_functions,
       cmdline.isset("pointer-check"));
+    // Java virtual functions -> explicit dispatch tables:
     remove_virtual_functions(symbol_table, goto_functions);
+    // Java instanceof -> clsid comparison:
+    remove_instanceof(symbol_table, goto_functions);
 
     // full slice?
     if(cmdline.isset("full-slice"))
diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp
index 8b36f6e71a4..9e9c4a180bb 100644
--- a/src/goto-analyzer/goto_analyzer_parse_options.cpp
+++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp
@@ -19,6 +19,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <goto-programs/set_properties.h>
 #include <goto-programs/remove_function_pointers.h>
 #include <goto-programs/remove_virtual_functions.h>
+#include <goto-programs/remove_instanceof.h>
 #include <goto-programs/remove_returns.h>
 #include <goto-programs/remove_vector.h>
 #include <goto-programs/remove_complex.h>
@@ -380,7 +381,10 @@ bool goto_analyzer_parse_optionst::process_goto_program(
     // remove function pointers
     status() << "Removing function pointers and virtual functions" << eom;
     remove_function_pointers(goto_model, cmdline.isset("pointer-check"));
+    // Java virtual functions -> explicit dispatch tables:
     remove_virtual_functions(goto_model);
+    // Java instanceof -> clsid comparison:
+    remove_instanceof(goto_model);
 
     // do partial inlining
     status() << "Partial Inlining" << eom;
diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp
index 52c65c3ce37..b69d286a467 100644
--- a/src/goto-instrument/goto_instrument_parse_options.cpp
+++ b/src/goto-instrument/goto_instrument_parse_options.cpp
@@ -17,6 +17,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <goto-programs/goto_convert_functions.h>
 #include <goto-programs/remove_function_pointers.h>
+#include <goto-programs/remove_virtual_functions.h>
+#include <goto-programs/remove_instanceof.h>
 #include <goto-programs/remove_skip.h>
 #include <goto-programs/goto_inline.h>
 #include <goto-programs/show_properties.h>
@@ -246,7 +248,7 @@ int goto_instrument_parse_optionst::doit()
 
     if(cmdline.isset("show-value-sets"))
     {
-      do_function_pointer_removal();
+      do_indirect_call_and_rtti_removal();
       do_partial_inlining();
 
       // recalculate numbers, etc.
@@ -263,7 +265,7 @@ int goto_instrument_parse_optionst::doit()
 
     if(cmdline.isset("show-global-may-alias"))
     {
-      do_function_pointer_removal();
+      do_indirect_call_and_rtti_removal();
       do_partial_inlining();
       do_remove_returns();
       parameter_assignments(symbol_table, goto_functions);
@@ -281,7 +283,7 @@ int goto_instrument_parse_optionst::doit()
 
     if(cmdline.isset("show-local-bitvector-analysis"))
     {
-      do_function_pointer_removal();
+      do_indirect_call_and_rtti_removal();
       do_partial_inlining();
       parameter_assignments(symbol_table, goto_functions);
 
@@ -305,7 +307,7 @@ int goto_instrument_parse_optionst::doit()
 
     if(cmdline.isset("show-custom-bitvector-analysis"))
     {
-      do_function_pointer_removal();
+      do_indirect_call_and_rtti_removal();
       do_partial_inlining();
       do_remove_returns();
       parameter_assignments(symbol_table, goto_functions);
@@ -331,7 +333,7 @@ int goto_instrument_parse_optionst::doit()
 
     if(cmdline.isset("show-escape-analysis"))
     {
-      do_function_pointer_removal();
+      do_indirect_call_and_rtti_removal();
       do_partial_inlining();
       do_remove_returns();
       parameter_assignments(symbol_table, goto_functions);
@@ -351,7 +353,7 @@ int goto_instrument_parse_optionst::doit()
 
     if(cmdline.isset("custom-bitvector-analysis"))
     {
-      do_function_pointer_removal();
+      do_indirect_call_and_rtti_removal();
       do_partial_inlining();
       do_remove_returns();
       parameter_assignments(symbol_table, goto_functions);
@@ -382,7 +384,7 @@ int goto_instrument_parse_optionst::doit()
 
     if(cmdline.isset("show-points-to"))
     {
-      do_function_pointer_removal();
+      do_indirect_call_and_rtti_removal();
       do_partial_inlining();
 
       // recalculate numbers, etc.
@@ -399,7 +401,7 @@ int goto_instrument_parse_optionst::doit()
 
     if(cmdline.isset("show-intervals"))
     {
-      do_function_pointer_removal();
+      do_indirect_call_and_rtti_removal();
       do_partial_inlining();
 
       // recalculate numbers, etc.
@@ -433,7 +435,7 @@ int goto_instrument_parse_optionst::doit()
 
       if(!cmdline.isset("inline"))
       {
-        do_function_pointer_removal();
+        do_indirect_call_and_rtti_removal();
         do_partial_inlining();
 
         // recalculate numbers, etc.
@@ -460,7 +462,7 @@ int goto_instrument_parse_optionst::doit()
 
     if(cmdline.isset("show-reaching-definitions"))
     {
-      do_function_pointer_removal();
+      do_indirect_call_and_rtti_removal();
 
       const namespacet ns(symbol_table);
       reaching_definitions_analysist rd_analysis(ns);
@@ -483,7 +485,7 @@ int goto_instrument_parse_optionst::doit()
 
     if(cmdline.isset("show-dependence-graph"))
     {
-      do_function_pointer_removal();
+      do_indirect_call_and_rtti_removal();
 
       const namespacet ns(symbol_table);
       dependence_grapht dependence_graph(ns);
@@ -674,7 +676,7 @@ int goto_instrument_parse_optionst::doit()
 
     if(cmdline.isset("accelerate"))
     {
-      do_function_pointer_removal();
+      do_indirect_call_and_rtti_removal();
 
       namespacet ns(symbol_table);
 
@@ -757,7 +759,7 @@ int goto_instrument_parse_optionst::doit()
 
 /*******************************************************************\
 
-Function: goto_instrument_parse_optionst::do_function_pointer_removal
+Function: goto_instrument_parse_optionst::do_indirect_call_and_rtti_removal
 
   Inputs:
 
@@ -767,9 +769,10 @@ Function: goto_instrument_parse_optionst::do_function_pointer_removal
 
 \*******************************************************************/
 
-void goto_instrument_parse_optionst::do_function_pointer_removal()
+void goto_instrument_parse_optionst::do_indirect_call_and_rtti_removal(
+  bool force)
 {
-  if(function_pointer_removal_done)
+  if(function_pointer_removal_done && !force)
     return;
 
   function_pointer_removal_done=true;
@@ -779,6 +782,10 @@ void goto_instrument_parse_optionst::do_function_pointer_removal()
     symbol_table,
     goto_functions,
     cmdline.isset("pointer-check"));
+  status() << "Virtual function removal" << eom;
+  remove_virtual_functions(symbol_table, goto_functions);
+  status() << "Java instanceof removal" << eom;
+  remove_instanceof(symbol_table, goto_functions);
 }
 
 /*******************************************************************\
@@ -954,7 +961,7 @@ void goto_instrument_parse_optionst::instrument_goto_program()
   // now do full inlining, if requested
   if(cmdline.isset("inline"))
   {
-    do_function_pointer_removal();
+    do_indirect_call_and_rtti_removal();
 
     if(cmdline.isset("show-custom-bitvector-analysis") ||
        cmdline.isset("custom-bitvector-analysis"))
@@ -980,7 +987,7 @@ void goto_instrument_parse_optionst::instrument_goto_program()
 
   if(cmdline.isset("escape-analysis"))
   {
-    do_function_pointer_removal();
+    do_indirect_call_and_rtti_removal();
     do_partial_inlining();
     do_remove_returns();
     parameter_assignments(symbol_table, goto_functions);
@@ -1009,14 +1016,14 @@ void goto_instrument_parse_optionst::instrument_goto_program()
 
   // replace function pointers, if explicitly requested
   if(cmdline.isset("remove-function-pointers"))
-    do_function_pointer_removal();
+    do_indirect_call_and_rtti_removal();
 
   if(cmdline.isset("function-inline"))
   {
     std::string function=cmdline.get_value("function-inline");
     assert(!function.empty());
 
-    do_function_pointer_removal();
+    do_indirect_call_and_rtti_removal();
 
     status() << "Inlining calls of function `" << function << "'" << eom;
 
@@ -1067,7 +1074,7 @@ void goto_instrument_parse_optionst::instrument_goto_program()
 
   if(cmdline.isset("partial-inline"))
   {
-    do_function_pointer_removal();
+    do_indirect_call_and_rtti_removal();
 
     status() << "Partial inlining" << eom;
     goto_partial_inline(goto_functions, ns, ui_message_handler, true);
@@ -1079,11 +1086,7 @@ void goto_instrument_parse_optionst::instrument_goto_program()
   // now do full inlining, if requested
   if(cmdline.isset("inline"))
   {
-    status() << "Function Pointer Removal" << eom;
-    remove_function_pointers(
-      symbol_table,
-      goto_functions,
-      cmdline.isset("pointer-check"));
+    do_indirect_call_and_rtti_removal(/*force=*/true);
 
     if(cmdline.isset("show-custom-bitvector-analysis") ||
        cmdline.isset("custom-bitvector-analysis"))
@@ -1099,7 +1102,7 @@ void goto_instrument_parse_optionst::instrument_goto_program()
 
   if(cmdline.isset("constant-propagator"))
   {
-    do_function_pointer_removal();
+    do_indirect_call_and_rtti_removal();
 
     status() << "Propagating Constants" << eom;
 
@@ -1161,7 +1164,7 @@ void goto_instrument_parse_optionst::instrument_goto_program()
      cmdline.isset("isr") ||
      cmdline.isset("concurrency"))
   {
-    do_function_pointer_removal();
+    do_indirect_call_and_rtti_removal();
     do_partial_inlining();
 
     status() << "Pointer Analysis" << eom;
@@ -1400,7 +1403,7 @@ void goto_instrument_parse_optionst::instrument_goto_program()
   // full slice?
   if(cmdline.isset("full-slice"))
   {
-    do_function_pointer_removal();
+    do_indirect_call_and_rtti_removal();
 
     status() << "Performing a full slice" << eom;
     if(cmdline.isset("property"))
diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h
index c8c992f23e7..1d74bd94dbf 100644
--- a/src/goto-instrument/goto_instrument_parse_options.h
+++ b/src/goto-instrument/goto_instrument_parse_options.h
@@ -96,7 +96,7 @@ class goto_instrument_parse_optionst:
 
   void eval_verbosity();
 
-  void do_function_pointer_removal();
+  void do_indirect_call_and_rtti_removal(bool force=false);
   void do_partial_inlining();
   void do_remove_returns();
 
diff --git a/src/goto-programs/remove_instanceof.cpp b/src/goto-programs/remove_instanceof.cpp
index 7930a67f4c2..ee7f5979332 100644
--- a/src/goto-programs/remove_instanceof.cpp
+++ b/src/goto-programs/remove_instanceof.cpp
@@ -276,3 +276,9 @@ void remove_instanceof(
   remove_instanceoft rem(symbol_table, goto_functions);
   rem.lower_instanceof();
 }
+
+void remove_instanceof(goto_modelt &goto_model)
+{
+  remove_instanceof(
+    goto_model.symbol_table, goto_model.goto_functions);
+}
diff --git a/src/goto-programs/remove_instanceof.h b/src/goto-programs/remove_instanceof.h
index 6adf67b3dd8..7b4682ba9bf 100644
--- a/src/goto-programs/remove_instanceof.h
+++ b/src/goto-programs/remove_instanceof.h
@@ -11,10 +11,12 @@ Author: Chris Smowton, chris.smowton@diffblue.com
 
 #include <util/symbol_table.h>
 #include "goto_functions.h"
+#include "goto_model.h"
 
 void remove_instanceof(
   symbol_tablet &symbol_table,
   goto_functionst &goto_functions);
 
+void remove_instanceof(goto_modelt &model);
 
 #endif
diff --git a/src/symex/symex_parse_options.cpp b/src/symex/symex_parse_options.cpp
index 9930d9cf43a..148f5b646d1 100644
--- a/src/symex/symex_parse_options.cpp
+++ b/src/symex/symex_parse_options.cpp
@@ -32,6 +32,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <goto-programs/remove_complex.h>
 #include <goto-programs/remove_vector.h>
 #include <goto-programs/remove_virtual_functions.h>
+#include <goto-programs/remove_instanceof.h>
 
 #include <goto-symex/rewrite_union.h>
 #include <goto-symex/adjust_float_expressions.h>
@@ -361,7 +362,10 @@ bool symex_parse_optionst::process_goto_program(const optionst &options)
     // remove stuff
     remove_complex(goto_model);
     remove_vector(goto_model);
+    // Java virtual functions -> explicit dispatch tables:
     remove_virtual_functions(goto_model);
+    // Java instanceof -> clsid comparison:
+    remove_instanceof(goto_model);
     rewrite_union(goto_model);
     adjust_float_expressions(goto_model);