diff --git a/regression/cbmc-java/ArithmeticException6/test.desc b/regression/cbmc-java/ArithmeticException6/test.desc
index 8cab5f69869..8cd09de8d51 100644
--- a/regression/cbmc-java/ArithmeticException6/test.desc
+++ b/regression/cbmc-java/ArithmeticException6/test.desc
@@ -1,6 +1,6 @@
 CORE
 ArithmeticExceptionTest.class
---java-throw-runtime-exceptions
+--java-throw-runtime-exceptions --function ArithmeticExceptionTest.main
 ^EXIT=10$
 ^SIGNAL=0$
 ^.*assertion at file ArithmeticExceptionTest.java line 7 function.*: FAILURE$
diff --git a/regression/cbmc-java/LocalVarTable5/test.desc b/regression/cbmc-java/LocalVarTable5/test.desc
index 6f55a0d2bc6..82237a426e9 100644
--- a/regression/cbmc-java/LocalVarTable5/test.desc
+++ b/regression/cbmc-java/LocalVarTable5/test.desc
@@ -1,6 +1,6 @@
 CORE
 test.class
---show-goto-functions
+--show-goto-functions --function test.main
 dead anonlocal::1i
 dead anonlocal::2i
 dead anonlocal::3a
diff --git a/regression/cbmc-java/NondetInit2/test.desc b/regression/cbmc-java/NondetInit2/test.desc
index d75e7538e9b..4d752d2f54a 100644
--- a/regression/cbmc-java/NondetInit2/test.desc
+++ b/regression/cbmc-java/NondetInit2/test.desc
@@ -1,5 +1,4 @@
 CORE
 Test.class
-
+--function Test.main
 ^VERIFICATION SUCCESSFUL$
-
diff --git a/regression/cbmc-java/NondetInit3/Subclass.class b/regression/cbmc-java/NondetInit3/Subclass.class
index ff6f1ffb001..68201e11870 100644
Binary files a/regression/cbmc-java/NondetInit3/Subclass.class and b/regression/cbmc-java/NondetInit3/Subclass.class differ
diff --git a/regression/cbmc-java/NondetInit3/Test.class b/regression/cbmc-java/NondetInit3/Test.class
index d3b4a9378f8..0c032f41a9c 100644
Binary files a/regression/cbmc-java/NondetInit3/Test.class and b/regression/cbmc-java/NondetInit3/Test.class differ
diff --git a/regression/cbmc-java/NondetInit3/Test.java b/regression/cbmc-java/NondetInit3/Test.java
index edcea5419ca..3a5a6a01883 100644
--- a/regression/cbmc-java/NondetInit3/Test.java
+++ b/regression/cbmc-java/NondetInit3/Test.java
@@ -14,7 +14,8 @@ public static void main(Subclass nondetInput) {
         // The condition enforced by cproverNondetInitialize should hold
         // even though the parameter is a subtype of Test, not directly an
         // instance of Test itself.
-        assert nondetInput.arr.length == 1;
+        if(nondetInput != null)
+            assert nondetInput.arr.length == 1;
     }
 
 }
diff --git a/regression/cbmc-java/NondetInit3/test.desc b/regression/cbmc-java/NondetInit3/test.desc
index d75e7538e9b..4d752d2f54a 100644
--- a/regression/cbmc-java/NondetInit3/test.desc
+++ b/regression/cbmc-java/NondetInit3/test.desc
@@ -1,5 +1,4 @@
 CORE
 Test.class
-
+--function Test.main
 ^VERIFICATION SUCCESSFUL$
-
diff --git a/regression/cbmc-java/VarLengthArrayTrace1/test.desc b/regression/cbmc-java/VarLengthArrayTrace1/test.desc
index 77b1aeea6d8..d8d3ba023a0 100644
--- a/regression/cbmc-java/VarLengthArrayTrace1/test.desc
+++ b/regression/cbmc-java/VarLengthArrayTrace1/test.desc
@@ -1,6 +1,6 @@
 CORE
 VarLengthArrayTrace1.class
---trace
+--trace --function VarLengthArrayTrace1.main
 ^EXIT=10$
 ^SIGNAL=0$
 dynamic_3_array\[1.*\]=10
diff --git a/regression/cbmc-java/arrayread1/test.desc b/regression/cbmc-java/arrayread1/test.desc
index f0cbf9617d2..ed81d9c96da 100644
--- a/regression/cbmc-java/arrayread1/test.desc
+++ b/regression/cbmc-java/arrayread1/test.desc
@@ -1,6 +1,6 @@
 CORE
 arrayread1.class
---unwind 3 --no-propagation
+--unwind 3 --no-propagation --function arrayread1.main
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/cbmc-java/cast_null1/test.desc b/regression/cbmc-java/cast_null1/test.desc
index 86a52fc73e7..b4ae385c8a5 100644
--- a/regression/cbmc-java/cast_null1/test.desc
+++ b/regression/cbmc-java/cast_null1/test.desc
@@ -1,6 +1,6 @@
 CORE
 test.class
-
+--function test.main
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/cbmc-java/cast_null2/test.desc b/regression/cbmc-java/cast_null2/test.desc
index c621e5854e5..b71b059cd5a 100644
--- a/regression/cbmc-java/cast_null2/test.desc
+++ b/regression/cbmc-java/cast_null2/test.desc
@@ -1,6 +1,6 @@
 CORE
 test.class
---java-throw-runtime-exceptions
+--java-throw-runtime-exceptions --function test.main
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/cbmc-java/destructor1/test.desc b/regression/cbmc-java/destructor1/test.desc
index 32dea0b83f5..e8fdb97f062 100644
--- a/regression/cbmc-java/destructor1/test.desc
+++ b/regression/cbmc-java/destructor1/test.desc
@@ -1,6 +1,6 @@
 CORE
 Break.class
---show-goto-functions
+--show-goto-functions --function Break.main
 ^EXIT=0$
 ^SIGNAL=0$
 dead i;
diff --git a/regression/cbmc-java/exceptions22/test.desc b/regression/cbmc-java/exceptions22/test.desc
index a3eaa698597..89862c09829 100644
--- a/regression/cbmc-java/exceptions22/test.desc
+++ b/regression/cbmc-java/exceptions22/test.desc
@@ -1,6 +1,6 @@
 CORE
 test.class
-
+--function test.main
 ^EXIT=0$
 ^SIGNAL=0$
 VERIFICATION SUCCESSFUL
diff --git a/regression/cbmc-java/external_getstatic1/test.desc b/regression/cbmc-java/external_getstatic1/test.desc
index dc5ca4fa5cb..c5038351062 100644
--- a/regression/cbmc-java/external_getstatic1/test.desc
+++ b/regression/cbmc-java/external_getstatic1/test.desc
@@ -1,6 +1,6 @@
 CORE
 test.class
-
+--function test.main
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/cbmc-java/inferlexicalscope1/test.desc b/regression/cbmc-java/inferlexicalscope1/test.desc
index f6c5dae4466..b8de396de71 100644
--- a/regression/cbmc-java/inferlexicalscope1/test.desc
+++ b/regression/cbmc-java/inferlexicalscope1/test.desc
@@ -1,6 +1,6 @@
 CORE
 test.class
---show-symbol-table
+--show-symbol-table --function test.main
 ^EXIT=0$
 ^SIGNAL=0$
 ^pc7:
diff --git a/regression/cbmc-java/inherited_static_field1/test.desc b/regression/cbmc-java/inherited_static_field1/test.desc
index 2907dba48a4..6d1cf2a4270 100644
--- a/regression/cbmc-java/inherited_static_field1/test.desc
+++ b/regression/cbmc-java/inherited_static_field1/test.desc
@@ -1,6 +1,6 @@
 CORE
 Test.class
-
+--function Test.main
 ^VERIFICATION SUCCESSFUL$
 --
 --
diff --git a/regression/cbmc-java/inherited_static_field10/test.desc b/regression/cbmc-java/inherited_static_field10/test.desc
index 21b4aa8958f..63e8c8db02d 100644
--- a/regression/cbmc-java/inherited_static_field10/test.desc
+++ b/regression/cbmc-java/inherited_static_field10/test.desc
@@ -1,6 +1,6 @@
 CORE
 Test.class
-
+--function Test.main
 Stub static field x found for non-stub type java::Test\. In future this will be a fatal error\.
 assertion at file Test\.java line 6 .* FAILURE
 ^VERIFICATION FAILED$
diff --git a/regression/cbmc-java/inherited_static_field2/test.desc b/regression/cbmc-java/inherited_static_field2/test.desc
index 03cdd9bf210..c6fde2b99c7 100644
--- a/regression/cbmc-java/inherited_static_field2/test.desc
+++ b/regression/cbmc-java/inherited_static_field2/test.desc
@@ -1,6 +1,6 @@
 CORE
 Test.class
-
+--function Test.main
 ^VERIFICATION SUCCESSFUL$
 --
 --
diff --git a/regression/cbmc-java/inherited_static_field3/test.desc b/regression/cbmc-java/inherited_static_field3/test.desc
index 7c103f56c23..a56e09480bc 100644
--- a/regression/cbmc-java/inherited_static_field3/test.desc
+++ b/regression/cbmc-java/inherited_static_field3/test.desc
@@ -1,6 +1,6 @@
 CORE
 Test.class
-
+--function Test.main
 ^VERIFICATION SUCCESSFUL$
 --
 --
diff --git a/regression/cbmc-java/inherited_static_field4/test.desc b/regression/cbmc-java/inherited_static_field4/test.desc
index 7654d272915..63d3b477175 100644
--- a/regression/cbmc-java/inherited_static_field4/test.desc
+++ b/regression/cbmc-java/inherited_static_field4/test.desc
@@ -1,6 +1,6 @@
 CORE
 Test.class
-
+--function Test.main
 assertion at file Test\.java line 6 .* FAILURE
 ^VERIFICATION FAILED$
 --
diff --git a/regression/cbmc-java/inherited_static_field5/test.desc b/regression/cbmc-java/inherited_static_field5/test.desc
index 648ed211410..9351c137b97 100644
--- a/regression/cbmc-java/inherited_static_field5/test.desc
+++ b/regression/cbmc-java/inherited_static_field5/test.desc
@@ -1,6 +1,6 @@
 CORE
 Test.class
-
+--function Test.main
 ^VERIFICATION SUCCESSFUL$
 --
 --
diff --git a/regression/cbmc-java/inherited_static_field6/test.desc b/regression/cbmc-java/inherited_static_field6/test.desc
index 37e554af6ca..1fc8f3e76cd 100644
--- a/regression/cbmc-java/inherited_static_field6/test.desc
+++ b/regression/cbmc-java/inherited_static_field6/test.desc
@@ -1,6 +1,6 @@
 CORE
 Test.class
-
+--function Test.main
 assertion at file Test\.java line 6 .* FAILURE
 ^VERIFICATION FAILED$
 --
diff --git a/regression/cbmc-java/inherited_static_field7/test.desc b/regression/cbmc-java/inherited_static_field7/test.desc
index f008fcef51b..606f5f04f93 100644
--- a/regression/cbmc-java/inherited_static_field7/test.desc
+++ b/regression/cbmc-java/inherited_static_field7/test.desc
@@ -1,6 +1,6 @@
 CORE
 Test.class
-
+--function Test.main
 ^VERIFICATION SUCCESSFUL$
 --
 --
diff --git a/regression/cbmc-java/inherited_static_field8/test.desc b/regression/cbmc-java/inherited_static_field8/test.desc
index 2a8234f4dc3..501b3260dd2 100644
--- a/regression/cbmc-java/inherited_static_field8/test.desc
+++ b/regression/cbmc-java/inherited_static_field8/test.desc
@@ -1,6 +1,6 @@
 CORE
 Test.class
-
+--function Test.main
 assertion at file Test\.java line 6 .* SUCCESS
 assertion at file Test\.java line 7 .* FAILURE
 ^VERIFICATION FAILED$
diff --git a/regression/cbmc-java/inherited_static_field9/test.desc b/regression/cbmc-java/inherited_static_field9/test.desc
index 91444da43c2..01318dfb9ec 100644
--- a/regression/cbmc-java/inherited_static_field9/test.desc
+++ b/regression/cbmc-java/inherited_static_field9/test.desc
@@ -1,6 +1,6 @@
 CORE
 Test.class
-
+--function Test.main
 Stub static field x found for non-stub type java::Test\. In future this will be a fatal error\.
 Stub static field x found for non-stub type java::Parent\. In future this will be a fatal error\.
 assertion at file Test\.java line 6 .* FAILURE
diff --git a/regression/cbmc-java/isnan1/test.desc b/regression/cbmc-java/isnan1/test.desc
index 44113191ad4..c03e247c9b1 100644
--- a/regression/cbmc-java/isnan1/test.desc
+++ b/regression/cbmc-java/isnan1/test.desc
@@ -1,6 +1,6 @@
 CORE
 test.class
-
+--function test.main
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
diff --git a/regression/cbmc-java/json_trace1/test.desc b/regression/cbmc-java/json_trace1/test.desc
index c7596faa19d..d0f9b27b618 100644
--- a/regression/cbmc-java/json_trace1/test.desc
+++ b/regression/cbmc-java/json_trace1/test.desc
@@ -1,6 +1,6 @@
 CORE
 Test.class
---cover location --trace --json-ui
+--cover location --trace --json-ui --function Test.main
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/cbmc-java/json_trace3/test.desc b/regression/cbmc-java/json_trace3/test.desc
index a8ae2a31a1e..85dc84641de 100644
--- a/regression/cbmc-java/json_trace3/test.desc
+++ b/regression/cbmc-java/json_trace3/test.desc
@@ -1,6 +1,6 @@
 CORE
 Test.class
---cover location --trace --json-ui --unwind 5
+--cover location --trace --json-ui --unwind 5 --function Test.main
 activate-multi-line-match
 EXIT=0
 SIGNAL=0
diff --git a/regression/cbmc-java/lazyloading_synthetic_method_cleanup1/check_clinit_normally_present.desc b/regression/cbmc-java/lazyloading_synthetic_method_cleanup1/check_clinit_normally_present.desc
index c27723b09f9..ddcd21bd5f2 100644
--- a/regression/cbmc-java/lazyloading_synthetic_method_cleanup1/check_clinit_normally_present.desc
+++ b/regression/cbmc-java/lazyloading_synthetic_method_cleanup1/check_clinit_normally_present.desc
@@ -1,6 +1,5 @@
 CORE
 Test.class
---show-goto-functions
+--show-goto-functions --function Test.main
 java::Unused::clinit_wrapper
 Unused\.<clinit>\(\)
-
diff --git a/regression/cbmc-java/lazyloading_synthetic_method_cleanup1/check_clinit_removed_by_lazy_loading.desc b/regression/cbmc-java/lazyloading_synthetic_method_cleanup1/check_clinit_removed_by_lazy_loading.desc
index f832b065f69..7cb991a807f 100644
--- a/regression/cbmc-java/lazyloading_synthetic_method_cleanup1/check_clinit_removed_by_lazy_loading.desc
+++ b/regression/cbmc-java/lazyloading_synthetic_method_cleanup1/check_clinit_removed_by_lazy_loading.desc
@@ -1,6 +1,6 @@
 CORE
 Test.class
---lazy-methods --show-goto-functions
+--lazy-methods --show-goto-functions --function Test.main
 --
 java::Unused::clinit_wrapper
 Unused\.<clinit>\(\)
diff --git a/regression/cbmc-java/lazyloading_synthetic_method_cleanup1/check_runs_with_lazy_loading.desc b/regression/cbmc-java/lazyloading_synthetic_method_cleanup1/check_runs_with_lazy_loading.desc
index a9222f08176..67aa49a0689 100644
--- a/regression/cbmc-java/lazyloading_synthetic_method_cleanup1/check_runs_with_lazy_loading.desc
+++ b/regression/cbmc-java/lazyloading_synthetic_method_cleanup1/check_runs_with_lazy_loading.desc
@@ -1,5 +1,4 @@
 CORE
 Test.class
---lazy-methods
+--lazy-methods --function Test.main
 VERIFICATION SUCCESSFUL
-
diff --git a/regression/cbmc-java/lazyloading_synthetic_method_cleanup2/check_clinit_normally_present.desc b/regression/cbmc-java/lazyloading_synthetic_method_cleanup2/check_clinit_normally_present.desc
index d3d2757212f..32ea1eabe00 100644
--- a/regression/cbmc-java/lazyloading_synthetic_method_cleanup2/check_clinit_normally_present.desc
+++ b/regression/cbmc-java/lazyloading_synthetic_method_cleanup2/check_clinit_normally_present.desc
@@ -1,7 +1,6 @@
 CORE
 Test.class
---show-goto-functions
+--show-goto-functions --function Test.main
 java::Unused1::clinit_wrapper
 java::Unused2::clinit_wrapper
 Unused2\.<clinit>\(\)
-
diff --git a/regression/cbmc-java/lazyloading_synthetic_method_cleanup2/check_clinit_removed_by_lazy_loading.desc b/regression/cbmc-java/lazyloading_synthetic_method_cleanup2/check_clinit_removed_by_lazy_loading.desc
index 0dcedea2911..3fb25e852a4 100644
--- a/regression/cbmc-java/lazyloading_synthetic_method_cleanup2/check_clinit_removed_by_lazy_loading.desc
+++ b/regression/cbmc-java/lazyloading_synthetic_method_cleanup2/check_clinit_removed_by_lazy_loading.desc
@@ -1,6 +1,6 @@
 CORE
 Test.class
---lazy-methods --show-goto-functions
+--lazy-methods --show-goto-functions --function Test.main
 --
 java::Unused1::clinit_wrapper
 java::Unused2::clinit_wrapper
diff --git a/regression/cbmc-java/lazyloading_synthetic_method_cleanup2/check_runs_with_lazy_loading.desc b/regression/cbmc-java/lazyloading_synthetic_method_cleanup2/check_runs_with_lazy_loading.desc
index a9222f08176..67aa49a0689 100644
--- a/regression/cbmc-java/lazyloading_synthetic_method_cleanup2/check_runs_with_lazy_loading.desc
+++ b/regression/cbmc-java/lazyloading_synthetic_method_cleanup2/check_runs_with_lazy_loading.desc
@@ -1,5 +1,4 @@
 CORE
 Test.class
---lazy-methods
+--lazy-methods --function Test.main
 VERIFICATION SUCCESSFUL
-
diff --git a/regression/cbmc-java/lazyloading_synthetic_method_cleanup3/check_clinit_normally_present.desc b/regression/cbmc-java/lazyloading_synthetic_method_cleanup3/check_clinit_normally_present.desc
index e412a962e54..689fdc3efad 100644
--- a/regression/cbmc-java/lazyloading_synthetic_method_cleanup3/check_clinit_normally_present.desc
+++ b/regression/cbmc-java/lazyloading_synthetic_method_cleanup3/check_clinit_normally_present.desc
@@ -1,5 +1,5 @@
 CORE
 Test.class
---show-goto-functions
+--show-goto-functions --function Test.main
 java::Opaque\.<clinit>:\(\)V
 java::Opaque::clinit_wrapper
diff --git a/regression/cbmc-java/lazyloading_synthetic_method_cleanup3/check_clinit_removed_by_lazy_loading.desc b/regression/cbmc-java/lazyloading_synthetic_method_cleanup3/check_clinit_removed_by_lazy_loading.desc
index 9b1fb07cc31..ec1d71302d6 100644
--- a/regression/cbmc-java/lazyloading_synthetic_method_cleanup3/check_clinit_removed_by_lazy_loading.desc
+++ b/regression/cbmc-java/lazyloading_synthetic_method_cleanup3/check_clinit_removed_by_lazy_loading.desc
@@ -1,6 +1,6 @@
 CORE
 Test.class
---lazy-methods --show-goto-functions
+--lazy-methods --show-goto-functions --function Test.main
 --
 java::Opaque\.<clinit>:\(\)V
 java::Opaque::clinit_wrapper
diff --git a/regression/cbmc-java/lazyloading_synthetic_method_cleanup3/check_runs_with_lazy_loading.desc b/regression/cbmc-java/lazyloading_synthetic_method_cleanup3/check_runs_with_lazy_loading.desc
index a9222f08176..67aa49a0689 100644
--- a/regression/cbmc-java/lazyloading_synthetic_method_cleanup3/check_runs_with_lazy_loading.desc
+++ b/regression/cbmc-java/lazyloading_synthetic_method_cleanup3/check_runs_with_lazy_loading.desc
@@ -1,5 +1,4 @@
 CORE
 Test.class
---lazy-methods
+--lazy-methods --function Test.main
 VERIFICATION SUCCESSFUL
-
diff --git a/regression/cbmc-java/putstatic_source_location/test.desc b/regression/cbmc-java/putstatic_source_location/test.desc
index fdb85eb8ee7..c788f292700 100644
--- a/regression/cbmc-java/putstatic_source_location/test.desc
+++ b/regression/cbmc-java/putstatic_source_location/test.desc
@@ -1,6 +1,6 @@
 CORE
 test.class
---show-goto-functions
+--show-goto-functions --function test.main
 ^EXIT=0$
 ^SIGNAL=0$
 test\.java line 5 function java::test.main:\(\)V bytecode-index 1
diff --git a/regression/cbmc-java/static_init1/test.desc b/regression/cbmc-java/static_init1/test.desc
index 30868289dae..74331f8c333 100644
--- a/regression/cbmc-java/static_init1/test.desc
+++ b/regression/cbmc-java/static_init1/test.desc
@@ -1,6 +1,6 @@
 CORE
 static_init.class
-
+--function static_init.main
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/cbmc-java/static_init2/test.desc b/regression/cbmc-java/static_init2/test.desc
index 30868289dae..74331f8c333 100644
--- a/regression/cbmc-java/static_init2/test.desc
+++ b/regression/cbmc-java/static_init2/test.desc
@@ -1,6 +1,6 @@
 CORE
 static_init.class
-
+--function static_init.main
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/cbmc-java/trace_options_json_extended/extended.desc b/regression/cbmc-java/trace_options_json_extended/extended.desc
index a0234582e1d..16819b0ce24 100644
--- a/regression/cbmc-java/trace_options_json_extended/extended.desc
+++ b/regression/cbmc-java/trace_options_json_extended/extended.desc
@@ -1,6 +1,6 @@
 CORE
 Test.class
---trace --json-ui --trace-json-extended
+--trace --json-ui --trace-json-extended --function Test.main
 ^EXIT=10$
 ^SIGNAL=0$
 rawLhs
diff --git a/regression/cbmc-java/trace_options_json_extended/non-extended.desc b/regression/cbmc-java/trace_options_json_extended/non-extended.desc
index d13bdcd5f3f..8691dc49359 100644
--- a/regression/cbmc-java/trace_options_json_extended/non-extended.desc
+++ b/regression/cbmc-java/trace_options_json_extended/non-extended.desc
@@ -1,6 +1,6 @@
 CORE
 Test.class
---trace --json-ui
+--trace --json-ui --function Test.main
 ^EXIT=10$
 ^SIGNAL=0$
 --
diff --git a/regression/cbmc-java/virtual7/test.desc b/regression/cbmc-java/virtual7/test.desc
index d873bbcc8f9..6e420f8430c 100644
--- a/regression/cbmc-java/virtual7/test.desc
+++ b/regression/cbmc-java/virtual7/test.desc
@@ -1,6 +1,6 @@
 CORE
 test.class
---show-goto-functions
+--show-goto-functions --function test.main
 ^EXIT=0$
 ^SIGNAL=0$
 IF.*"java::C".*THEN GOTO [12]
diff --git a/regression/cbmc-java/virtual8/test.desc b/regression/cbmc-java/virtual8/test.desc
index 774005ac03d..dd23bff445d 100644
--- a/regression/cbmc-java/virtual8/test.desc
+++ b/regression/cbmc-java/virtual8/test.desc
@@ -1,6 +1,6 @@
 CORE
 Test.class
---program-only
+--program-only --function Test.main
 ^EXIT=0$
 ^SIGNAL=0$
 C\.f
diff --git a/regression/jbmc-strings/java_append_char/test.desc b/regression/jbmc-strings/java_append_char/test.desc
index 783301b2d52..efe6c611b39 100644
--- a/regression/jbmc-strings/java_append_char/test.desc
+++ b/regression/jbmc-strings/java_append_char/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_append_char.class
---refine-strings --string-max-length 1000 --no-core-models
+--refine-strings --string-max-length 1000 --no-core-models --function test_append_char.main
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
diff --git a/regression/jbmc-strings/java_char_array_init/test.desc b/regression/jbmc-strings/java_char_array_init/test.desc
index e93fd2a4dc2..47fcb2fd1ce 100644
--- a/regression/jbmc-strings/java_char_array_init/test.desc
+++ b/regression/jbmc-strings/java_char_array_init/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_init.class
---refine-strings --string-max-length 1000
+--refine-strings --string-max-length 1000 --function test_init.main
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* file test_init.java line 31 .* SUCCESS$
diff --git a/regression/jbmc-strings/java_insert_char_array/test.desc b/regression/jbmc-strings/java_insert_char_array/test.desc
index ea77b6e60aa..012a7e34e22 100644
--- a/regression/jbmc-strings/java_insert_char_array/test.desc
+++ b/regression/jbmc-strings/java_insert_char_array/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_insert_char_array.class
---refine-strings --string-max-length 1000
+--refine-strings --string-max-length 1000 --function test_insert_char_array.main
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 28.* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_append_string/test.desc b/regression/strings-smoke-tests/java_append_string/test.desc
index 9b6882b5f3f..847ade7776d 100644
--- a/regression/strings-smoke-tests/java_append_string/test.desc
+++ b/regression/strings-smoke-tests/java_append_string/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_append_string.class
---refine-strings --verbosity 10 --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000 --function test_append_string.main
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/strings-smoke-tests/java_case/test.desc b/regression/strings-smoke-tests/java_case/test.desc
index bf6722dd2f8..18fa3cccaa9 100644
--- a/regression/strings-smoke-tests/java_case/test.desc
+++ b/regression/strings-smoke-tests/java_case/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_case.class
---refine-strings --verbosity 10 --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000 --function test_case.main
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* file test_case.java line 10 .* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_char_array/test.desc b/regression/strings-smoke-tests/java_char_array/test.desc
index 3b1bf17532a..5d9ef1fdd7c 100644
--- a/regression/strings-smoke-tests/java_char_array/test.desc
+++ b/regression/strings-smoke-tests/java_char_array/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_char_array.class
---refine-strings --verbosity 10 --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000 --function test_char_array.main
 ^EXIT=10$
 ^SIGNAL=0$
 .*assertion.* test_char_array.java line 7 .* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_insert_char_array/test.desc b/regression/strings-smoke-tests/java_insert_char_array/test.desc
index a0614d7f360..53af52fc3ef 100644
--- a/regression/strings-smoke-tests/java_insert_char_array/test.desc
+++ b/regression/strings-smoke-tests/java_insert_char_array/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_insert_char_array.class
---refine-strings --verbosity 10 --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000 --function test_insert_char_array.main
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* file test_insert_char_array.java line 20 .* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_int_to_string/test1.desc b/regression/strings-smoke-tests/java_int_to_string/test1.desc
index fd14afd9e7f..a8ace56c37b 100644
--- a/regression/strings-smoke-tests/java_int_to_string/test1.desc
+++ b/regression/strings-smoke-tests/java_int_to_string/test1.desc
@@ -1,6 +1,6 @@
 CORE
 Test1.class
---refine-strings --verbosity 10 --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000 --function Test1.main
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_int_to_string/test2.desc b/regression/strings-smoke-tests/java_int_to_string/test2.desc
index 08bb206db54..e068d78d000 100644
--- a/regression/strings-smoke-tests/java_int_to_string/test2.desc
+++ b/regression/strings-smoke-tests/java_int_to_string/test2.desc
@@ -1,6 +1,6 @@
 CORE
 Test2.class
---refine-strings --verbosity 10 --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000 --function Test2.main
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_int_to_string/test2_bug.desc b/regression/strings-smoke-tests/java_int_to_string/test2_bug.desc
index c2917e25045..dc7e825073c 100644
--- a/regression/strings-smoke-tests/java_int_to_string/test2_bug.desc
+++ b/regression/strings-smoke-tests/java_int_to_string/test2_bug.desc
@@ -1,6 +1,6 @@
 KNOWNBUG
 Test2.class
---refine-strings --verbosity 10
+--refine-strings --verbosity 10 --function Test2.main
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_int_to_string/test3.desc b/regression/strings-smoke-tests/java_int_to_string/test3.desc
index c17950bade2..b35b58c87fa 100644
--- a/regression/strings-smoke-tests/java_int_to_string/test3.desc
+++ b/regression/strings-smoke-tests/java_int_to_string/test3.desc
@@ -1,6 +1,6 @@
 CORE
 Test3.class
---refine-strings --verbosity 10 --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000 --function Test3.main
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_int_to_string/test4.desc b/regression/strings-smoke-tests/java_int_to_string/test4.desc
index e8085e4cc0b..3630073e1dd 100644
--- a/regression/strings-smoke-tests/java_int_to_string/test4.desc
+++ b/regression/strings-smoke-tests/java_int_to_string/test4.desc
@@ -1,6 +1,6 @@
 CORE
 Test4.class
---refine-strings --verbosity 10 --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000 --function Test4.main
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_int_to_string/test5.desc b/regression/strings-smoke-tests/java_int_to_string/test5.desc
index 7a6c4dab79d..9fdf756a99d 100644
--- a/regression/strings-smoke-tests/java_int_to_string/test5.desc
+++ b/regression/strings-smoke-tests/java_int_to_string/test5.desc
@@ -1,6 +1,6 @@
 CORE
 Test5.class
---refine-strings --verbosity 10 --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000 --function Test5.main
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_int_to_string_knownbug/test.desc b/regression/strings-smoke-tests/java_int_to_string_knownbug/test.desc
index 0d37463d104..4c289d1853c 100644
--- a/regression/strings-smoke-tests/java_int_to_string_knownbug/test.desc
+++ b/regression/strings-smoke-tests/java_int_to_string_knownbug/test.desc
@@ -1,6 +1,6 @@
 KNOWNBUG
 Test.class
---refine-strings --verbosity 10 --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000 --function Test.main
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_int_to_string_with_radix/test_binary1.desc b/regression/strings-smoke-tests/java_int_to_string_with_radix/test_binary1.desc
index 3b0e8c9f52e..f76d7849b64 100644
--- a/regression/strings-smoke-tests/java_int_to_string_with_radix/test_binary1.desc
+++ b/regression/strings-smoke-tests/java_int_to_string_with_radix/test_binary1.desc
@@ -1,6 +1,6 @@
 CORE
 Test_binary1.class
---refine-strings --verbosity 10 --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000 --function Test_binary1.main
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_int_to_string_with_radix/test_binary2.desc b/regression/strings-smoke-tests/java_int_to_string_with_radix/test_binary2.desc
index 4b75576a9e0..b6b50f07cb3 100644
--- a/regression/strings-smoke-tests/java_int_to_string_with_radix/test_binary2.desc
+++ b/regression/strings-smoke-tests/java_int_to_string_with_radix/test_binary2.desc
@@ -1,6 +1,6 @@
 CORE
 Test_binary2.class
---refine-strings --verbosity 10 --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000 --function Test_binary2.main
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_int_to_string_with_radix/test_binary3.desc b/regression/strings-smoke-tests/java_int_to_string_with_radix/test_binary3.desc
index c0dc5a0d100..0252051ba90 100644
--- a/regression/strings-smoke-tests/java_int_to_string_with_radix/test_binary3.desc
+++ b/regression/strings-smoke-tests/java_int_to_string_with_radix/test_binary3.desc
@@ -1,6 +1,6 @@
 CORE
 Test_binary3.class
---refine-strings --verbosity 10 --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000 --function Test_binary3.main
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_int_to_string_with_radix/test_decimal.desc b/regression/strings-smoke-tests/java_int_to_string_with_radix/test_decimal.desc
index 5df0fa0c612..391797533f5 100644
--- a/regression/strings-smoke-tests/java_int_to_string_with_radix/test_decimal.desc
+++ b/regression/strings-smoke-tests/java_int_to_string_with_radix/test_decimal.desc
@@ -1,6 +1,6 @@
 CORE
 Test_decimal.class
---refine-strings --verbosity 10 --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000 --function Test_decimal.main
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_int_to_string_with_radix/test_hex1.desc b/regression/strings-smoke-tests/java_int_to_string_with_radix/test_hex1.desc
index 65d42d9d4f4..e37cf5534de 100644
--- a/regression/strings-smoke-tests/java_int_to_string_with_radix/test_hex1.desc
+++ b/regression/strings-smoke-tests/java_int_to_string_with_radix/test_hex1.desc
@@ -1,6 +1,6 @@
 CORE
 Test_hex1.class
---refine-strings --verbosity 10 --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000 --function Test_hex1.main
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_int_to_string_with_radix/test_hex2.desc b/regression/strings-smoke-tests/java_int_to_string_with_radix/test_hex2.desc
index ca27aacf182..e6ca4960d19 100644
--- a/regression/strings-smoke-tests/java_int_to_string_with_radix/test_hex2.desc
+++ b/regression/strings-smoke-tests/java_int_to_string_with_radix/test_hex2.desc
@@ -1,6 +1,6 @@
 CORE
 Test_hex2.class
---refine-strings --verbosity 10 --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000 --function Test_hex2.main
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_int_to_string_with_radix/test_hex3.desc b/regression/strings-smoke-tests/java_int_to_string_with_radix/test_hex3.desc
index d100589824c..d2f4d7cbb1c 100644
--- a/regression/strings-smoke-tests/java_int_to_string_with_radix/test_hex3.desc
+++ b/regression/strings-smoke-tests/java_int_to_string_with_radix/test_hex3.desc
@@ -1,6 +1,6 @@
 CORE
 Test_hex3.class
---refine-strings --verbosity 10 --string-max-length 100
+--refine-strings --verbosity 10 --string-max-length 100 --function Test_hex3.main
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_int_to_string_with_radix/test_octal1.desc b/regression/strings-smoke-tests/java_int_to_string_with_radix/test_octal1.desc
index 16600fd2a12..a223a0e81df 100644
--- a/regression/strings-smoke-tests/java_int_to_string_with_radix/test_octal1.desc
+++ b/regression/strings-smoke-tests/java_int_to_string_with_radix/test_octal1.desc
@@ -1,6 +1,6 @@
 CORE
 Test_octal1.class
---refine-strings --verbosity 10 --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000 --function Test_octal1.main
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_int_to_string_with_radix/test_octal2.desc b/regression/strings-smoke-tests/java_int_to_string_with_radix/test_octal2.desc
index cbe2eab8212..229c999d00c 100644
--- a/regression/strings-smoke-tests/java_int_to_string_with_radix/test_octal2.desc
+++ b/regression/strings-smoke-tests/java_int_to_string_with_radix/test_octal2.desc
@@ -1,6 +1,6 @@
 CORE
 Test_octal2.class
---refine-strings --verbosity 10 --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000 --function Test_octal2.main
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_int_to_string_with_radix/test_octal3.desc b/regression/strings-smoke-tests/java_int_to_string_with_radix/test_octal3.desc
index a742982813e..8b9c5a50209 100644
--- a/regression/strings-smoke-tests/java_int_to_string_with_radix/test_octal3.desc
+++ b/regression/strings-smoke-tests/java_int_to_string_with_radix/test_octal3.desc
@@ -1,6 +1,6 @@
 CORE
 Test_octal3.class
---refine-strings --verbosity 10 --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000 --function Test_octal3.main
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_int_to_string_with_radix_knownbug/test_binary.desc b/regression/strings-smoke-tests/java_int_to_string_with_radix_knownbug/test_binary.desc
index c81c25f146f..6d5672788ae 100644
--- a/regression/strings-smoke-tests/java_int_to_string_with_radix_knownbug/test_binary.desc
+++ b/regression/strings-smoke-tests/java_int_to_string_with_radix_knownbug/test_binary.desc
@@ -1,6 +1,6 @@
 KNOWNBUG
 Test_binary.class
---refine-strings --verbosity 10 --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000 --function Test_binary.main
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_int_to_string_with_radix_knownbug/test_hex.desc b/regression/strings-smoke-tests/java_int_to_string_with_radix_knownbug/test_hex.desc
index 5fec73731fc..c5d33723394 100644
--- a/regression/strings-smoke-tests/java_int_to_string_with_radix_knownbug/test_hex.desc
+++ b/regression/strings-smoke-tests/java_int_to_string_with_radix_knownbug/test_hex.desc
@@ -1,6 +1,6 @@
 KNOWNBUG
 Test_hex.class
---refine-strings --verbosity 10 --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000 --function Test_hex.main
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_int_to_string_with_radix_knownbug/test_octal.desc b/regression/strings-smoke-tests/java_int_to_string_with_radix_knownbug/test_octal.desc
index c47d55b6cf3..135a6d1a4aa 100644
--- a/regression/strings-smoke-tests/java_int_to_string_with_radix_knownbug/test_octal.desc
+++ b/regression/strings-smoke-tests/java_int_to_string_with_radix_knownbug/test_octal.desc
@@ -1,6 +1,6 @@
 KNOWNBUG
 Test_octal.class
---refine-strings --verbosity 10 --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000 --function Test_octal.main
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_long_to_string/test1.desc b/regression/strings-smoke-tests/java_long_to_string/test1.desc
index fd14afd9e7f..a8ace56c37b 100644
--- a/regression/strings-smoke-tests/java_long_to_string/test1.desc
+++ b/regression/strings-smoke-tests/java_long_to_string/test1.desc
@@ -1,6 +1,6 @@
 CORE
 Test1.class
---refine-strings --verbosity 10 --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000 --function Test1.main
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_long_to_string/test2.desc b/regression/strings-smoke-tests/java_long_to_string/test2.desc
index a58153ecbd5..45859f9d225 100644
--- a/regression/strings-smoke-tests/java_long_to_string/test2.desc
+++ b/regression/strings-smoke-tests/java_long_to_string/test2.desc
@@ -1,6 +1,6 @@
 THOROUGH
 Test2.class
---refine-strings --verbosity 10 --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000 --function Test2.main
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_long_to_string/test3.desc b/regression/strings-smoke-tests/java_long_to_string/test3.desc
index 4cc0e5b4f0a..8f4c4c1aae9 100644
--- a/regression/strings-smoke-tests/java_long_to_string/test3.desc
+++ b/regression/strings-smoke-tests/java_long_to_string/test3.desc
@@ -1,6 +1,6 @@
 THOROUGH
 Test3.class
---refine-strings --verbosity 10 --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000 --function Test3.main
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_long_to_string/test4.desc b/regression/strings-smoke-tests/java_long_to_string/test4.desc
index 11df46814d6..9f0dea8b275 100644
--- a/regression/strings-smoke-tests/java_long_to_string/test4.desc
+++ b/regression/strings-smoke-tests/java_long_to_string/test4.desc
@@ -1,6 +1,6 @@
 THOROUGH
 Test4.class
---refine-strings --verbosity 10 --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000 --function Test4.main
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_long_to_string/test5.desc b/regression/strings-smoke-tests/java_long_to_string/test5.desc
index 7a6c4dab79d..9fdf756a99d 100644
--- a/regression/strings-smoke-tests/java_long_to_string/test5.desc
+++ b/regression/strings-smoke-tests/java_long_to_string/test5.desc
@@ -1,6 +1,6 @@
 CORE
 Test5.class
---refine-strings --verbosity 10 --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000 --function Test5.main
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_long_to_string_with_radix/test_binary1.desc b/regression/strings-smoke-tests/java_long_to_string_with_radix/test_binary1.desc
index 46852f73fd8..64b50f64e69 100644
--- a/regression/strings-smoke-tests/java_long_to_string_with_radix/test_binary1.desc
+++ b/regression/strings-smoke-tests/java_long_to_string_with_radix/test_binary1.desc
@@ -1,6 +1,6 @@
 THOROUGH
 Test_binary1.class
---refine-strings --verbosity 10 --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000 --function Test_binary1.main
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_long_to_string_with_radix/test_binary2.desc b/regression/strings-smoke-tests/java_long_to_string_with_radix/test_binary2.desc
index 88ecdd6658e..fe04564fdbc 100644
--- a/regression/strings-smoke-tests/java_long_to_string_with_radix/test_binary2.desc
+++ b/regression/strings-smoke-tests/java_long_to_string_with_radix/test_binary2.desc
@@ -1,6 +1,6 @@
 THOROUGH
 Test_binary2.class
---refine-strings --verbosity 10 --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000 --function Test_binary2.main
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_long_to_string_with_radix/test_binary3.desc b/regression/strings-smoke-tests/java_long_to_string_with_radix/test_binary3.desc
index 690a7051bff..22abe124fb8 100644
--- a/regression/strings-smoke-tests/java_long_to_string_with_radix/test_binary3.desc
+++ b/regression/strings-smoke-tests/java_long_to_string_with_radix/test_binary3.desc
@@ -1,6 +1,6 @@
 THOROUGH
 Test_binary3.class
---refine-strings --verbosity 10 --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000 --function Test_binary3.main
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_long_to_string_with_radix/test_decimal.desc b/regression/strings-smoke-tests/java_long_to_string_with_radix/test_decimal.desc
index 5df0fa0c612..391797533f5 100644
--- a/regression/strings-smoke-tests/java_long_to_string_with_radix/test_decimal.desc
+++ b/regression/strings-smoke-tests/java_long_to_string_with_radix/test_decimal.desc
@@ -1,6 +1,6 @@
 CORE
 Test_decimal.class
---refine-strings --verbosity 10 --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000 --function Test_decimal.main
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_long_to_string_with_radix/test_hex1.desc b/regression/strings-smoke-tests/java_long_to_string_with_radix/test_hex1.desc
index 65d42d9d4f4..e37cf5534de 100644
--- a/regression/strings-smoke-tests/java_long_to_string_with_radix/test_hex1.desc
+++ b/regression/strings-smoke-tests/java_long_to_string_with_radix/test_hex1.desc
@@ -1,6 +1,6 @@
 CORE
 Test_hex1.class
---refine-strings --verbosity 10 --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000 --function Test_hex1.main
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_long_to_string_with_radix/test_hex2.desc b/regression/strings-smoke-tests/java_long_to_string_with_radix/test_hex2.desc
index ca27aacf182..e6ca4960d19 100644
--- a/regression/strings-smoke-tests/java_long_to_string_with_radix/test_hex2.desc
+++ b/regression/strings-smoke-tests/java_long_to_string_with_radix/test_hex2.desc
@@ -1,6 +1,6 @@
 CORE
 Test_hex2.class
---refine-strings --verbosity 10 --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000 --function Test_hex2.main
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_long_to_string_with_radix/test_hex3.desc b/regression/strings-smoke-tests/java_long_to_string_with_radix/test_hex3.desc
index d100589824c..d2f4d7cbb1c 100644
--- a/regression/strings-smoke-tests/java_long_to_string_with_radix/test_hex3.desc
+++ b/regression/strings-smoke-tests/java_long_to_string_with_radix/test_hex3.desc
@@ -1,6 +1,6 @@
 CORE
 Test_hex3.class
---refine-strings --verbosity 10 --string-max-length 100
+--refine-strings --verbosity 10 --string-max-length 100 --function Test_hex3.main
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_long_to_string_with_radix/test_octal1.desc b/regression/strings-smoke-tests/java_long_to_string_with_radix/test_octal1.desc
index 87aad11f09f..6543f6938f7 100644
--- a/regression/strings-smoke-tests/java_long_to_string_with_radix/test_octal1.desc
+++ b/regression/strings-smoke-tests/java_long_to_string_with_radix/test_octal1.desc
@@ -1,6 +1,6 @@
 CORE
 Test_octal1.class
---refine-strings --verbosity 10 --string-max-length 100
+--refine-strings --verbosity 10 --string-max-length 100 --function Test_octal1.main
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_long_to_string_with_radix/test_octal2.desc b/regression/strings-smoke-tests/java_long_to_string_with_radix/test_octal2.desc
index 11904eb55b9..7597b88f4be 100644
--- a/regression/strings-smoke-tests/java_long_to_string_with_radix/test_octal2.desc
+++ b/regression/strings-smoke-tests/java_long_to_string_with_radix/test_octal2.desc
@@ -1,6 +1,6 @@
 CORE
 Test_octal2.class
---refine-strings --verbosity 10 --string-max-length 100
+--refine-strings --verbosity 10 --string-max-length 100 --function Test_octal2.main
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_long_to_string_with_radix/test_octal3.desc b/regression/strings-smoke-tests/java_long_to_string_with_radix/test_octal3.desc
index ef669e31737..aea786f5b92 100644
--- a/regression/strings-smoke-tests/java_long_to_string_with_radix/test_octal3.desc
+++ b/regression/strings-smoke-tests/java_long_to_string_with_radix/test_octal3.desc
@@ -1,6 +1,6 @@
 CORE
 Test_octal3.class
---refine-strings --verbosity 10 --string-max-length 100
+--refine-strings --verbosity 10 --string-max-length 100 --function Test_octal3.main
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_parseint/test1.desc b/regression/strings-smoke-tests/java_parseint/test1.desc
index 78d825da2ae..9b4e20397e0 100644
--- a/regression/strings-smoke-tests/java_parseint/test1.desc
+++ b/regression/strings-smoke-tests/java_parseint/test1.desc
@@ -1,6 +1,6 @@
 CORE
 Test1.class
---refine-strings --verbosity 10 --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000 --function Test1.main
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 8.* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_parseint/test2.desc b/regression/strings-smoke-tests/java_parseint/test2.desc
index 84540226f3c..eb61c1ce86a 100644
--- a/regression/strings-smoke-tests/java_parseint/test2.desc
+++ b/regression/strings-smoke-tests/java_parseint/test2.desc
@@ -1,6 +1,6 @@
 CORE
 Test2.class
---refine-strings --verbosity 10 --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000 --function Test2.main
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 9.* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_parseint_knownbug/test.desc b/regression/strings-smoke-tests/java_parseint_knownbug/test.desc
index aa80ccad92f..f71c35b54bd 100644
--- a/regression/strings-smoke-tests/java_parseint_knownbug/test.desc
+++ b/regression/strings-smoke-tests/java_parseint_knownbug/test.desc
@@ -1,6 +1,6 @@
 KNOWNBUG
 Test.class
---refine-strings --verbosity 10 --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000 --function Test.main
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 10.* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_parseint_with_radix/test1.desc b/regression/strings-smoke-tests/java_parseint_with_radix/test1.desc
index 78d825da2ae..9b4e20397e0 100644
--- a/regression/strings-smoke-tests/java_parseint_with_radix/test1.desc
+++ b/regression/strings-smoke-tests/java_parseint_with_radix/test1.desc
@@ -1,6 +1,6 @@
 CORE
 Test1.class
---refine-strings --verbosity 10 --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000 --function Test1.main
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 8.* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_parseint_with_radix/test2.desc b/regression/strings-smoke-tests/java_parseint_with_radix/test2.desc
index 40528a8244d..8ea06b614e0 100644
--- a/regression/strings-smoke-tests/java_parseint_with_radix/test2.desc
+++ b/regression/strings-smoke-tests/java_parseint_with_radix/test2.desc
@@ -1,6 +1,6 @@
 CORE
 Test2.class
---refine-strings --verbosity 10 --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000 --function Test2.main
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 8.* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_parseint_with_radix/test3.desc b/regression/strings-smoke-tests/java_parseint_with_radix/test3.desc
index ea37ca8efb1..1e96c531c29 100644
--- a/regression/strings-smoke-tests/java_parseint_with_radix/test3.desc
+++ b/regression/strings-smoke-tests/java_parseint_with_radix/test3.desc
@@ -1,6 +1,6 @@
 CORE
 Test3.class
---refine-strings --verbosity 10 --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000 --function Test3.main
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 8.* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_parseint_with_radix/test4.desc b/regression/strings-smoke-tests/java_parseint_with_radix/test4.desc
index aa4756341bb..e0980a2d899 100644
--- a/regression/strings-smoke-tests/java_parseint_with_radix/test4.desc
+++ b/regression/strings-smoke-tests/java_parseint_with_radix/test4.desc
@@ -1,6 +1,6 @@
 CORE
 Test4.class
---refine-strings --verbosity 10 --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000 --function Test4.main
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 8.* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_parseint_with_radix/test5.desc b/regression/strings-smoke-tests/java_parseint_with_radix/test5.desc
index ea45d5af377..b7f35f7dccb 100644
--- a/regression/strings-smoke-tests/java_parseint_with_radix/test5.desc
+++ b/regression/strings-smoke-tests/java_parseint_with_radix/test5.desc
@@ -1,6 +1,6 @@
 CORE
 Test5.class
---refine-strings --verbosity 10 --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000 --function Test5.main
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 8.* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_parseint_with_radix/test6.desc b/regression/strings-smoke-tests/java_parseint_with_radix/test6.desc
index 3ce216107c7..0f42ae7f205 100644
--- a/regression/strings-smoke-tests/java_parseint_with_radix/test6.desc
+++ b/regression/strings-smoke-tests/java_parseint_with_radix/test6.desc
@@ -1,6 +1,6 @@
 CORE
 Test6.class
---refine-strings --verbosity 10 --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000 --function Test6.main
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 9.* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_parselong/test_binary_min.desc b/regression/strings-smoke-tests/java_parselong/test_binary_min.desc
index 0271a0c984a..9243521d9ff 100644
--- a/regression/strings-smoke-tests/java_parselong/test_binary_min.desc
+++ b/regression/strings-smoke-tests/java_parselong/test_binary_min.desc
@@ -1,6 +1,6 @@
 CORE
 Test_binary_min.class
---refine-strings --verbosity 10 --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000 --function Test_binary_min.main
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 9.* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_parselong/test_decimal_max.desc b/regression/strings-smoke-tests/java_parselong/test_decimal_max.desc
index 640ed17fa83..9797e44dff0 100644
--- a/regression/strings-smoke-tests/java_parselong/test_decimal_max.desc
+++ b/regression/strings-smoke-tests/java_parselong/test_decimal_max.desc
@@ -1,6 +1,6 @@
 CORE
 Test_decimal_max.class
---refine-strings --verbosity 10 --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000 --function Test_decimal_max.main
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 9.* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_parselong/test_decimal_min.desc b/regression/strings-smoke-tests/java_parselong/test_decimal_min.desc
index 432fa01db5b..e2f1869d29d 100644
--- a/regression/strings-smoke-tests/java_parselong/test_decimal_min.desc
+++ b/regression/strings-smoke-tests/java_parselong/test_decimal_min.desc
@@ -1,6 +1,6 @@
 CORE
 Test_decimal_min.class
---refine-strings --verbosity 10 --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000 --function Test_decimal_min.main
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 9.* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_parselong/test_hex.desc b/regression/strings-smoke-tests/java_parselong/test_hex.desc
index 7dfd21113a5..7a991265f4c 100644
--- a/regression/strings-smoke-tests/java_parselong/test_hex.desc
+++ b/regression/strings-smoke-tests/java_parselong/test_hex.desc
@@ -1,6 +1,6 @@
 CORE
 Test_hex.class
---refine-strings --verbosity 10 --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000 --function Test_hex.main
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 8.* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_parselong/test_octal.desc b/regression/strings-smoke-tests/java_parselong/test_octal.desc
index b3310436432..a35595e7d2c 100644
--- a/regression/strings-smoke-tests/java_parselong/test_octal.desc
+++ b/regression/strings-smoke-tests/java_parselong/test_octal.desc
@@ -1,6 +1,6 @@
 CORE
 Test_octal.class
---refine-strings --verbosity 10 --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000 --function Test_octal.main
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 8.* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_value_of_long/test.desc b/regression/strings-smoke-tests/java_value_of_long/test.desc
index e4e7094d764..e91920c7478 100644
--- a/regression/strings-smoke-tests/java_value_of_long/test.desc
+++ b/regression/strings-smoke-tests/java_value_of_long/test.desc
@@ -1,6 +1,6 @@
 CORE
 test.class
---refine-strings --verbosity 10 --string-max-length 1000
+--refine-strings --verbosity 10 --string-max-length 1000 --function test.main
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* file test.java line 9 .* SUCCESS$
diff --git a/regression/strings-smoke-tests/max_input_length/MemberTest.desc b/regression/strings-smoke-tests/max_input_length/MemberTest.desc
index 01640d0a77c..2a62caa2eda 100644
--- a/regression/strings-smoke-tests/max_input_length/MemberTest.desc
+++ b/regression/strings-smoke-tests/max_input_length/MemberTest.desc
@@ -1,6 +1,6 @@
 CORE
 MemberTest.class
---refine-strings --verbosity 10 --string-max-length 29 --java-assume-inputs-non-null
+--refine-strings --verbosity 10 --string-max-length 29 --java-assume-inputs-non-null --function MemberTest.main
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$