Tests for simplifying ID_string equalities

regression/cbmc-java/virtual8/Test.java

@@ -0,0 +1,29 @@
+public class Test {
+  public static void runF(A x) {
+    x.f();
+  }
+
+  public static void main() {
+    A y = new D();
+    runF(y);
+  }
+}
+
+class A {
+  void f() { }
+}
+
+
+class B extends A {
+  void f() { }
+}
+
+class C extends A {
+  void f() { }
+}
+
+class D extends C {
+}
+
+class E extends B {
+}

regression/cbmc-java/virtual8/test.desc

@@ -0,0 +1,11 @@
+CORE
+Test.class
+--program-only
+^EXIT=0$
+^SIGNAL=0$
+C\.f
+--
+A\.f
+B\.f
+D\.f
+E\.f

regression/cbmc-java/virtual9/Test.java

@@ -0,0 +1,33 @@
+public class Test {
+  public static void runF(A x) {
+    x.f();
+  }
+
+  public static void main(String[] args) {
+    A y = null;
+    if(args.length==3)
+      y = new C();
+    else
+      y = new E();
+    runF(y);
+  }
+}
+
+class A {
+  void f() { }
+}
+
+
+class B extends A {
+  void f() { }
+}
+
+class C extends A {
+  void f() { }
+}
+
+class D extends C {
+}
+
+class E extends B {
+}

regression/cbmc-java/virtual9/test.desc

@@ -0,0 +1,13 @@
+KNOWNBUG
+Test.class
+--program-only
+^EXIT=0$
+^SIGNAL=0$
+B\.f
+C\.f
+--
+A\.f
+D\.f
+E\.f
+--
+could be pruned by a value set analysis