diff --git a/regression/goto-diff/java-instanceof/new.jar b/regression/goto-diff/java-instanceof/new.jar
new file mode 100644
index 00000000000..bc067de9a6a
Binary files /dev/null and b/regression/goto-diff/java-instanceof/new.jar differ
diff --git a/regression/goto-diff/java-instanceof/new/Test.java b/regression/goto-diff/java-instanceof/new/Test.java
new file mode 100644
index 00000000000..0bd39087a0b
--- /dev/null
+++ b/regression/goto-diff/java-instanceof/new/Test.java
@@ -0,0 +1,16 @@
+class A {
+}
+
+class B extends A {
+}
+
+public class Test {
+
+  public boolean foo(A x) {
+    if (x instanceof A) {
+      return true;
+    } else {
+      return false;
+    }
+  }
+}
diff --git a/regression/goto-diff/java-instanceof/old.jar b/regression/goto-diff/java-instanceof/old.jar
new file mode 100644
index 00000000000..25aba503dd7
Binary files /dev/null and b/regression/goto-diff/java-instanceof/old.jar differ
diff --git a/regression/goto-diff/java-instanceof/old/Test.java b/regression/goto-diff/java-instanceof/old/Test.java
new file mode 100644
index 00000000000..6ec791ae253
--- /dev/null
+++ b/regression/goto-diff/java-instanceof/old/Test.java
@@ -0,0 +1,22 @@
+/* 
+old.jar needs to be created by first adding B.class and Test.class and then
+updated to add A.class. This makes the class loader load the classes A and B
+in reverse order.
+*/
+
+class A {
+}
+
+class B extends A {
+}
+
+public class Test {
+
+  public boolean foo(A x) {
+    if (x instanceof A) {
+      return true;
+    } else {
+      return false;
+    }
+  }
+}
diff --git a/regression/goto-diff/java-instanceof/test.desc b/regression/goto-diff/java-instanceof/test.desc
new file mode 100644
index 00000000000..9e5863b5a5e
--- /dev/null
+++ b/regression/goto-diff/java-instanceof/test.desc
@@ -0,0 +1,10 @@
+CORE
+new.jar
+old.jar
+// Enable multi-line checking
+activate-multi-line-match
+EXIT=0
+SIGNAL=0
+new functions:\nmodified functions:\ndeleted functions:
+--
+^warning: ignoring
diff --git a/regression/goto-diff/java-virtual-methods/new.jar b/regression/goto-diff/java-virtual-methods/new.jar
new file mode 100644
index 00000000000..5c9c5990a03
Binary files /dev/null and b/regression/goto-diff/java-virtual-methods/new.jar differ
diff --git a/regression/goto-diff/java-virtual-methods/new/Test.java b/regression/goto-diff/java-virtual-methods/new/Test.java
new file mode 100644
index 00000000000..a048bc7cf61
--- /dev/null
+++ b/regression/goto-diff/java-virtual-methods/new/Test.java
@@ -0,0 +1,18 @@
+class A {
+  boolean bar() {
+    return true;
+  }
+}
+
+class B extends A {
+  boolean bar() {
+    return false;
+  }
+}
+
+public class Test {
+
+  public boolean foo(A x) {
+    return x.bar();
+  }
+}
diff --git a/regression/goto-diff/java-virtual-methods/old.jar b/regression/goto-diff/java-virtual-methods/old.jar
new file mode 100644
index 00000000000..fdea5e45df8
Binary files /dev/null and b/regression/goto-diff/java-virtual-methods/old.jar differ
diff --git a/regression/goto-diff/java-virtual-methods/old/Test.java b/regression/goto-diff/java-virtual-methods/old/Test.java
new file mode 100644
index 00000000000..41b3d813c18
--- /dev/null
+++ b/regression/goto-diff/java-virtual-methods/old/Test.java
@@ -0,0 +1,24 @@
+/* 
+old.jar needs to be created by first adding B.class and Test.class and then
+updated to add A.class. This makes the class loader load the classes A and B
+in reverse order.
+*/
+
+class A {
+  boolean bar() {
+    return true;
+  }
+}
+
+class B extends A {
+  boolean bar() {
+    return false;
+  }
+}
+
+public class Test {
+
+  public boolean foo(A x) {
+    return x.bar();
+  }
+}
diff --git a/regression/goto-diff/java-virtual-methods/test.desc b/regression/goto-diff/java-virtual-methods/test.desc
new file mode 100644
index 00000000000..9e5863b5a5e
--- /dev/null
+++ b/regression/goto-diff/java-virtual-methods/test.desc
@@ -0,0 +1,10 @@
+CORE
+new.jar
+old.jar
+// Enable multi-line checking
+activate-multi-line-match
+EXIT=0
+SIGNAL=0
+new functions:\nmodified functions:\ndeleted functions:
+--
+^warning: ignoring
diff --git a/src/goto-programs/remove_instanceof.cpp b/src/goto-programs/remove_instanceof.cpp
index 50166e33d03..e859c8d9384 100644
--- a/src/goto-programs/remove_instanceof.cpp
+++ b/src/goto-programs/remove_instanceof.cpp
@@ -87,6 +87,14 @@ std::size_t remove_instanceoft::lower_instanceof(
   std::vector<irep_idt> children=
     class_hierarchy.get_children_trans(target_name);
   children.push_back(target_name);
+  // Sort alphabetically to make order of generated disjuncts
+  // independent of class loading order
+  std::sort(
+    children.begin(),
+    children.end(),
+    [](const irep_idt &a, const irep_idt &b) { // NOLINT
+      return a.compare(b) < 0;
+    });
 
   // Insert an instruction before the new check that assigns the clsid we're
   // checking for to a temporary, as GOTO program if-expressions should
diff --git a/src/goto-programs/remove_virtual_functions.cpp b/src/goto-programs/remove_virtual_functions.cpp
index fad271b0d27..f3b53c57a9b 100644
--- a/src/goto-programs/remove_virtual_functions.cpp
+++ b/src/goto-programs/remove_virtual_functions.cpp
@@ -445,6 +445,8 @@ void remove_virtual_functionst::get_functions(
         has_prefix(
           id2string(b.symbol_expr.get_identifier()), "java::java.lang.Object"))
         return true;
+      else if(a.symbol_expr.get_identifier() == b.symbol_expr.get_identifier())
+        return a.class_id < b.class_id;
       else
         return a.symbol_expr.get_identifier() < b.symbol_expr.get_identifier();
     });