Add regression test

In the original implementation, D.toString would be resolved to
java.lang.Object.toString().

Author: Matthias Güdemann

regression/cbmc-java/virtual10/A.class

@@ -0,0 +1,6 @@
+CORE
+E.class
+--show-goto-functions
+IF.*"java::D"
+IF.*"java::O"
+IF.*"java::C"

regression/cbmc-java/virtual10/B.class

@@ -0,0 +1,35 @@
+interface A {
+  public int f();
+}
+interface B {
+  public int g();
+}
+
+class O {
+  public String toString() {
+    return "O";
+  }
+}
+
+class D extends O implements A, B {
+  public int f() {
+    return 0;
+  }
+  public int g() {
+    return 1;
+  }
+}
+
+class C extends D {
+  public String toString() {
+    return "C";
+  }
+}
+
+class E {
+  C c;
+  D d;
+  String f(Object o) {
+    return o.toString();
+  }
+}