diff --git a/jbmc/regression/jbmc/parameter-annotation-not-null/test_array.desc b/jbmc/regression/jbmc/parameter-annotation-not-null/test_array.desc
index d69e34dc1f..6135bc74fe 100644
--- a/jbmc/regression/jbmc/parameter-annotation-not-null/test_array.desc
+++ b/jbmc/regression/jbmc/parameter-annotation-not-null/test_array.desc
@@ -4,7 +4,7 @@ Main.class
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
-\[not-null-annotation-check\.1\] line \d+ Not null annotation check: FAILURE
-\[not-null-annotation-check\.2\] line \d+ Not null annotation check: SUCCESS
+\[java::Main\.bar:\(Ljava/lang/Integer;ZLjava/lang/Object;\[Ljava/lang/String;\)Ljava/lang/Integer;\.not-null-annotation-check\.1\] line \d+ Not null annotation check: FAILURE
+\[java::Main\.bar:\(Ljava/lang/Integer;ZLjava/lang/Object;\[Ljava/lang/String;\)Ljava/lang/Integer;\.not-null-annotation-check\.2\] line \d+ Not null annotation check: SUCCESS
 --
 ^warning: ignoring
diff --git a/jbmc/regression/jbmc/parameter-annotation-not-null/test_object.desc b/jbmc/regression/jbmc/parameter-annotation-not-null/test_object.desc
index e546ffb874..21adb4efd6 100644
--- a/jbmc/regression/jbmc/parameter-annotation-not-null/test_object.desc
+++ b/jbmc/regression/jbmc/parameter-annotation-not-null/test_object.desc
@@ -4,7 +4,7 @@ Main.class
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
-\[not-null-annotation-check\.1\] line \d+ Not null annotation check: SUCCESS
-\[not-null-annotation-check\.2\] line \d+ Not null annotation check: FAILURE
+\[java::Main\.foo:\(Ljava/lang/Integer;ZLjava/lang/Object;\[Ljava/lang/String;\)Ljava/lang/Integer;\.not-null-annotation-check\.1\] line \d+ Not null annotation check: SUCCESS
+\[java::Main\.foo:\(Ljava/lang/Integer;ZLjava/lang/Object;\[Ljava/lang/String;\)Ljava/lang/Integer;\.not-null-annotation-check\.2\] line \d+ Not null annotation check: FAILURE
 --
 ^warning: ignoring
diff --git a/jbmc/regression/jbmc/parameter-annotation-not-null/test_success.desc b/jbmc/regression/jbmc/parameter-annotation-not-null/test_success.desc
index 1285af8cb8..d01c2f281e 100644
--- a/jbmc/regression/jbmc/parameter-annotation-not-null/test_success.desc
+++ b/jbmc/regression/jbmc/parameter-annotation-not-null/test_success.desc
@@ -4,7 +4,7 @@ Main.class
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
-\[not-null-annotation-check\.1\] line \d+ Not null annotation check: SUCCESS
-\[not-null-annotation-check\.2\] line \d+ Not null annotation check: SUCCESS
+\[java::Main\.foo:\(Ljava/lang/Integer;ZLjava/lang/Object;\[Ljava/lang/String;\)Ljava/lang/Integer;\.not-null-annotation-check\.1\] line \d+ Not null annotation check: SUCCESS
+\[java::Main\.foo:\(Ljava/lang/Integer;ZLjava/lang/Object;\[Ljava/lang/String;\)Ljava/lang/Integer;\.not-null-annotation-check\.2\] line \d+ Not null annotation check: SUCCESS
 --
 ^warning: ignoring