diff --git a/jbmc/regression/jbmc/virtual_equals_object_param/SimpleEquals.class b/jbmc/regression/jbmc/virtual_equals_object_param/SimpleEquals.class
new file mode 100644
index 00000000000..3adeca6f588
Binary files /dev/null and b/jbmc/regression/jbmc/virtual_equals_object_param/SimpleEquals.class differ
diff --git a/jbmc/regression/jbmc/virtual_equals_object_param/SimpleEquals.java b/jbmc/regression/jbmc/virtual_equals_object_param/SimpleEquals.java
new file mode 100644
index 00000000000..0bbcfdbcd6f
--- /dev/null
+++ b/jbmc/regression/jbmc/virtual_equals_object_param/SimpleEquals.java
@@ -0,0 +1,22 @@
+// Simpler test case demonstrating the virtual method resolution bug
+public class SimpleEquals {
+  public static void testDirect() {
+    // Direct call on String - this works
+    String s1 = "hello";
+    String s2 = "hello";
+    assert(s1.equals(s2));
+  }
+
+  public static void testThroughObject(Object o1, Object o2) {
+    // Call through Object parameter - this was failing before the fix
+    assert(o1.equals(o2));
+  }
+
+  public static void main(String[] args) {
+    testDirect();
+    
+    String s1 = "world";
+    String s2 = "world";
+    testThroughObject(s1, s2);
+  }
+}
diff --git a/jbmc/regression/jbmc/virtual_equals_object_param/equals_Pass.class b/jbmc/regression/jbmc/virtual_equals_object_param/equals_Pass.class
new file mode 100644
index 00000000000..5246bc17974
Binary files /dev/null and b/jbmc/regression/jbmc/virtual_equals_object_param/equals_Pass.class differ
diff --git a/jbmc/regression/jbmc/virtual_equals_object_param/equals_Pass.java b/jbmc/regression/jbmc/virtual_equals_object_param/equals_Pass.java
new file mode 100644
index 00000000000..e5a9f365b6c
--- /dev/null
+++ b/jbmc/regression/jbmc/virtual_equals_object_param/equals_Pass.java
@@ -0,0 +1,13 @@
+public class equals_Pass {
+  private static boolean myEquals(Object a, Object b) {
+      return (a == b) || (a != null && a.equals(b));
+  }
+
+  public static void main(String[] args) {
+    String a = new String("abc");
+    String b = new String("abc");
+    assert((a == b) || (a != null && a.equals(b)));  // This passes
+    boolean result = myEquals(a, b);
+    assert(result);  // This fails
+  }
+}
diff --git a/jbmc/regression/jbmc/virtual_equals_object_param/simple_test.desc b/jbmc/regression/jbmc/virtual_equals_object_param/simple_test.desc
new file mode 100644
index 00000000000..2e69d6649e8
--- /dev/null
+++ b/jbmc/regression/jbmc/virtual_equals_object_param/simple_test.desc
@@ -0,0 +1,9 @@
+CORE
+SimpleEquals.class
+--function SimpleEquals.main
+^EXIT=0$
+^SIGNAL=0$
+^\[SimpleEquals.testDirect.assertion.1\] line 6 .*: SUCCESS$
+^\[SimpleEquals.testThroughObject.assertion.1\] line 11 .*: SUCCESS$
+--
+^warning: ignoring
diff --git a/jbmc/regression/jbmc/virtual_equals_object_param/test.desc b/jbmc/regression/jbmc/virtual_equals_object_param/test.desc
new file mode 100644
index 00000000000..2abada22906
--- /dev/null
+++ b/jbmc/regression/jbmc/virtual_equals_object_param/test.desc
@@ -0,0 +1,9 @@
+CORE
+equals_Pass.class
+--function equals_Pass.main
+^EXIT=0$
+^SIGNAL=0$
+^\[equals_Pass.main.assertion.1\] line 9 .*: SUCCESS$
+^\[equals_Pass.main.assertion.2\] line 11 .*: SUCCESS$
+--
+^warning: ignoring
diff --git a/src/goto-programs/remove_virtual_functions.cpp b/src/goto-programs/remove_virtual_functions.cpp
index 21d96041a1e..9b3d502c0b7 100644
--- a/src/goto-programs/remove_virtual_functions.cpp
+++ b/src/goto-programs/remove_virtual_functions.cpp
@@ -518,13 +518,12 @@ void get_virtual_calleest::get_child_functions_rec(
   for(const auto &child : findit->second.children)
   {
     // Skip if we have already visited this and we found a function call that
-    // did not resolve to non java.lang.Object.
+    // resolved to a non-Object implementation (i.e., we don't need to revisit).
     auto it = entry_map.find(child);
     if(
-      it != entry_map.end() &&
-      (!it->second.symbol_expr.has_value() ||
-       !it->second.symbol_expr->get_identifier().starts_with(
-         "java::java.lang.Object")))
+      it != entry_map.end() && it->second.symbol_expr.has_value() &&
+      !it->second.symbol_expr->get_identifier().starts_with(
+        "java::java.lang.Object"))
     {
       continue;
     }