diff --git a/jbmc/regression/jbmc/generic_function_parameter/Test.class b/jbmc/regression/jbmc/generic_function_parameter/Test.class
new file mode 100644
index 00000000000..ae8d55d61b6
Binary files /dev/null and b/jbmc/regression/jbmc/generic_function_parameter/Test.class differ
diff --git a/jbmc/regression/jbmc/generic_function_parameter/Test.java b/jbmc/regression/jbmc/generic_function_parameter/Test.java
new file mode 100644
index 00000000000..e1a3907526a
--- /dev/null
+++ b/jbmc/regression/jbmc/generic_function_parameter/Test.java
@@ -0,0 +1,28 @@
+
+public class Test<T> {
+
+  public void main(Test<String> param) {
+
+    callee(param);
+
+  }
+
+  public void callee(Test<String> param) {
+
+    assert false;
+
+  }
+
+  public void main2(Test<String> param) {
+
+    callee2((Test<T>)param);
+
+  }
+
+  public void callee2(Test<T> param) {
+
+    assert false;
+
+  }
+
+}
diff --git a/jbmc/regression/jbmc/generic_function_parameter/callee2_with_cast.desc b/jbmc/regression/jbmc/generic_function_parameter/callee2_with_cast.desc
new file mode 100644
index 00000000000..adcb0f01924
--- /dev/null
+++ b/jbmc/regression/jbmc/generic_function_parameter/callee2_with_cast.desc
@@ -0,0 +1,9 @@
+CORE
+Test.class
+--function Test.main2 --show-goto-functions
+^EXIT=0$
+^SIGNAL=0$
+this \. Test.callee2:\(LTest;\)V\(\(struct Test \*\)param\);
+--
+--
+Test and callee2 have differing parameter types, so there should be a cast at the callsite.
diff --git a/jbmc/regression/jbmc/generic_function_parameter/callee_without_cast.desc b/jbmc/regression/jbmc/generic_function_parameter/callee_without_cast.desc
new file mode 100644
index 00000000000..2f711614d97
--- /dev/null
+++ b/jbmc/regression/jbmc/generic_function_parameter/callee_without_cast.desc
@@ -0,0 +1,9 @@
+CORE
+Test.class
+--function Test.main --show-goto-functions
+^EXIT=0$
+^SIGNAL=0$
+this \. Test.callee:\(LTest;\)V\(param\);
+--
+--
+Test and callee have matching parameter types, so there should be no cast at the callsite.
diff --git a/jbmc/regression/jbmc/generic_function_parameter/ensure_runs.desc b/jbmc/regression/jbmc/generic_function_parameter/ensure_runs.desc
new file mode 100644
index 00000000000..871055f5801
--- /dev/null
+++ b/jbmc/regression/jbmc/generic_function_parameter/ensure_runs.desc
@@ -0,0 +1,9 @@
+CORE
+Test.class
+--function Test.main
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+^\[java::Test.callee:\(LTest;\)V\.assertion\.1\] line 12 assertion at file Test\.java line 12 function java::Test\.callee:\(LTest;\)V bytecode-index 5: FAILURE$
+--
+^warning: ignoring
diff --git a/jbmc/regression/jbmc/generic_function_parameter/ensure_runs2.desc b/jbmc/regression/jbmc/generic_function_parameter/ensure_runs2.desc
new file mode 100644
index 00000000000..30d2be9f4a5
--- /dev/null
+++ b/jbmc/regression/jbmc/generic_function_parameter/ensure_runs2.desc
@@ -0,0 +1,9 @@
+CORE
+Test.class
+--function Test.main2
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+^\[java::Test.callee2:\(LTest;\)V\.assertion\.1\] line 24 assertion at file Test\.java line 24 function java::Test\.callee2:\(LTest;\)V bytecode-index 5: FAILURE$
+--
+^warning: ignoring