diff --git a/jbmc/regression/jbmc/generic_base_type/Base.class b/jbmc/regression/jbmc/generic_base_type/Base.class
new file mode 100644
index 00000000000..ed1fc4dfe8a
Binary files /dev/null and b/jbmc/regression/jbmc/generic_base_type/Base.class differ
diff --git a/jbmc/regression/jbmc/generic_base_type/Base.java b/jbmc/regression/jbmc/generic_base_type/Base.java
new file mode 100644
index 00000000000..ffc8e304c23
--- /dev/null
+++ b/jbmc/regression/jbmc/generic_base_type/Base.java
@@ -0,0 +1,21 @@
+
+public class Base<T> { }
+
+class Test<T> extends Base<T> {
+
+  public void main(boolean unknown) {
+
+    if(unknown)
+      callee(getSpecialisedTest());
+    else
+      callee2(getUnspecialisedTest());
+
+  }
+
+  public Test<String> getSpecialisedTest() { return new Test<String>(); }
+  public Test<T> getUnspecialisedTest() { return new Test<T>(); }
+
+  public void callee(Base<String> b) { assert false; }
+  public void callee2(Base<T> b) { assert false; }
+
+}
diff --git a/jbmc/regression/jbmc/generic_base_type/Test.class b/jbmc/regression/jbmc/generic_base_type/Test.class
new file mode 100644
index 00000000000..da50eff488b
Binary files /dev/null and b/jbmc/regression/jbmc/generic_base_type/Test.class differ
diff --git a/jbmc/regression/jbmc/generic_base_type/check_casts.desc b/jbmc/regression/jbmc/generic_base_type/check_casts.desc
new file mode 100644
index 00000000000..69536dff3b9
--- /dev/null
+++ b/jbmc/regression/jbmc/generic_base_type/check_casts.desc
@@ -0,0 +1,10 @@
+CORE
+Test.class
+--function Test.main --show-goto-functions
+^EXIT=0$
+^SIGNAL=0$
+this \. Test\.callee:\(LBase;\)V\(\(struct Base \*\)&return_tmp0->@Base\);
+this \. Test\.callee2:\(LBase;\)V\(&return_tmp1->@Base\);
+--
+callee has a qualified Base type, and so requires a cast.
+callee2 has the unqualified type that Test<T> naturally inherits, so no cast is required.
diff --git a/jbmc/regression/jbmc/generic_base_type/ensure_runs.desc b/jbmc/regression/jbmc/generic_base_type/ensure_runs.desc
new file mode 100644
index 00000000000..188d02849a9
--- /dev/null
+++ b/jbmc/regression/jbmc/generic_base_type/ensure_runs.desc
@@ -0,0 +1,10 @@
+CORE
+Test.class
+--function Test.main
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+\[java::Test\.callee:\(LBase;\)V\.assertion\.1\] line 18 assertion at file Base\.java line 18 function java::Test\.callee:\(LBase;\)V bytecode-index 5: FAILURE
+\[java::Test\.callee2:\(LBase;\)V\.assertion\.1\] line 19 assertion at file Base\.java line 19 function java::Test\.callee2:\(LBase;\)V bytecode-index 5: FAILURE
+--
+^warning: ignoring