diff --git a/regression/cbmc-java/NullPointer1/test.desc b/regression/cbmc-java/NullPointer1/test.desc
index d479356875a..b11a57a56fd 100644
--- a/regression/cbmc-java/NullPointer1/test.desc
+++ b/regression/cbmc-java/NullPointer1/test.desc
@@ -3,7 +3,7 @@ NullPointer1.class
 --pointer-check --stop-on-fail
 ^EXIT=10$
 ^SIGNAL=0$
-^  file NullPointer1.java line 16 function java::NullPointer1.main:\(\[Ljava/lang/String;\)V$
+^  file NullPointer1.java line 16 function java::NullPointer1.main:\(\[Ljava/lang/String;\)V bytecode_index 9$
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring
diff --git a/regression/cbmc-java/NullPointer4/test.desc b/regression/cbmc-java/NullPointer4/test.desc
index 2e1b728c1fc..28c9e6f47fd 100644
--- a/regression/cbmc-java/NullPointer4/test.desc
+++ b/regression/cbmc-java/NullPointer4/test.desc
@@ -3,7 +3,7 @@ NullPointer4.class
 --pointer-check --stop-on-fail
 ^EXIT=10$
 ^SIGNAL=0$
-^  file NullPointer4.java line 6 function java::NullPointer4.main:\(\[Ljava/lang/String;\)V$
+^  file NullPointer4.java line 6 function java::NullPointer4.main:\(\[Ljava/lang/String;\)V bytecode_index 4$
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring
diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp
index cc418d6aed9..a6871b94d23 100644
--- a/src/analyses/goto_check.cpp
+++ b/src/analyses/goto_check.cpp
@@ -1820,6 +1820,10 @@ void goto_checkt::goto_check(
 
         if(it->source_location.get_column()!=irep_idt())
           i_it->source_location.set_column(it->source_location.get_column());
+
+        if(it->source_location.get_java_bytecode_index()!=irep_idt())
+          i_it->source_location.set_java_bytecode_index(
+            it->source_location.get_java_bytecode_index());
       }
 
       if(i_it->function==irep_idt())