diffblue · peterschrammel · Aug 23, 2017 · Aug 14, 2017 · thk123 · Aug 15, 2017
diff --git a/regression/cbmc-java/virtual_function_unwinding/Inner.class b/regression/cbmc-java/virtual_function_unwinding/Inner.class
diff --git a/regression/cbmc-java/virtual_function_unwinding/Interface.class b/regression/cbmc-java/virtual_function_unwinding/Interface.class
diff --git a/regression/cbmc-java/virtual_function_unwinding/Outer.class b/regression/cbmc-java/virtual_function_unwinding/Outer.class
diff --git a/regression/cbmc-java/virtual_function_unwinding/Virtual.class b/regression/cbmc-java/virtual_function_unwinding/Virtual.class
diff --git a/regression/cbmc-java/virtual_function_unwinding/Virtual.java b/regression/cbmc-java/virtual_function_unwinding/Virtual.java
@@ -0,0 +1,19 @@
+interface Interface {
+  boolean b();
+}
+
+class Inner implements Interface {
+  public boolean b() { return false; }
+}
+
+class Outer implements Interface {
+  private Interface inner;
+  public Outer(Interface inner) { this.inner = inner; }
+  public boolean b() { return !inner.b(); }
+}
+
+public class Virtual {
+  public static void main(String[] args) {
+    assert new Outer(new Inner()).b();
+  }
+}
diff --git a/regression/cbmc-java/virtual_function_unwinding/test.desc b/regression/cbmc-java/virtual_function_unwinding/test.desc
@@ -0,0 +1,8 @@
+KNOWNBUG
+Virtual.class
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+See diffblue/test-gen#845 for details