diff --git a/jbmc/regression/jbmc-strings/StringEquals/test_verify.desc b/jbmc/regression/jbmc-strings/StringEquals/test_verify.desc
index f13e27ac930..01bf846bfdc 100644
--- a/jbmc/regression/jbmc-strings/StringEquals/test_verify.desc
+++ b/jbmc/regression/jbmc-strings/StringEquals/test_verify.desc
@@ -1,6 +1,6 @@
 KNOWNBUG
 Test.class
---refine-strings --string-max-input-length 5 --string-max-length 100 --unwind 10 --function Test.verify --java-throw-runtime-exceptions
+--refine-strings --string-max-input-length 5 --string-max-length 100 --unwind 10 --function Test.verify --throw-runtime-exceptions
 ^EXIT=0$
 ^SIGNAL=0$
 assertion at file Test.java line 60 .* SUCCESS
diff --git a/jbmc/regression/jbmc-strings/StringLastIndexOf/test.desc b/jbmc/regression/jbmc-strings/StringLastIndexOf/test.desc
index 4f1852669c0..2e18576f085 100644
--- a/jbmc/regression/jbmc-strings/StringLastIndexOf/test.desc
+++ b/jbmc/regression/jbmc-strings/StringLastIndexOf/test.desc
@@ -1,6 +1,6 @@
 CORE
 Test.class
---function Test.check --refine-strings --string-max-length 100
+--function Test.check --refine-strings --string-max-input-length 100
 ^EXIT=10$
 ^SIGNAL=0$
 assertion at file Test.java line 11 .* SUCCESS$
diff --git a/jbmc/regression/jbmc-strings/char_escape/test.desc b/jbmc/regression/jbmc-strings/char_escape/test.desc
index 53ab05408c9..fea3171d5b6 100644
--- a/jbmc/regression/jbmc-strings/char_escape/test.desc
+++ b/jbmc/regression/jbmc-strings/char_escape/test.desc
@@ -3,4 +3,4 @@ Test.class
 --refine-strings --function Test.test --cover location --trace --json-ui
 ^EXIT=0$
 ^SIGNAL=0$
-20 of 23 covered \(87.0%\)|30 of 44 covered \(68.2%\)
+20 of 22 covered \(90.9%\)|30 of 44 covered \(68.2%\)
diff --git a/jbmc/regression/jbmc/ArithmeticException1/test.desc b/jbmc/regression/jbmc/ArithmeticException1/test.desc
index e8f7c941fd4..0339ff4f6d5 100644
--- a/jbmc/regression/jbmc/ArithmeticException1/test.desc
+++ b/jbmc/regression/jbmc/ArithmeticException1/test.desc
@@ -1,6 +1,6 @@
 CORE
 ArithmeticExceptionTest.class
---java-throw-runtime-exceptions
+--throw-runtime-exceptions
 ^EXIT=10$
 ^SIGNAL=0$
 ^.*assertion at file ArithmeticExceptionTest.java line 8 function.*: FAILURE$
diff --git a/jbmc/regression/jbmc/ArithmeticException2/test.desc b/jbmc/regression/jbmc/ArithmeticException2/test.desc
index 00820d86c6e..510065d60f0 100644
--- a/jbmc/regression/jbmc/ArithmeticException2/test.desc
+++ b/jbmc/regression/jbmc/ArithmeticException2/test.desc
@@ -1,6 +1,6 @@
 CORE
 ArithmeticExceptionTest.class
---java-throw-runtime-exceptions
+--throw-runtime-exceptions
 ^EXIT=10$
 ^SIGNAL=0$
 ^.*assertion at file ArithmeticExceptionTest.java line 9 function.*: FAILURE$
diff --git a/jbmc/regression/jbmc/ArithmeticException3/test.desc b/jbmc/regression/jbmc/ArithmeticException3/test.desc
index e8f7c941fd4..0339ff4f6d5 100644
--- a/jbmc/regression/jbmc/ArithmeticException3/test.desc
+++ b/jbmc/regression/jbmc/ArithmeticException3/test.desc
@@ -1,6 +1,6 @@
 CORE
 ArithmeticExceptionTest.class
---java-throw-runtime-exceptions
+--throw-runtime-exceptions
 ^EXIT=10$
 ^SIGNAL=0$
 ^.*assertion at file ArithmeticExceptionTest.java line 8 function.*: FAILURE$
diff --git a/jbmc/regression/jbmc/ArithmeticException4/test.desc b/jbmc/regression/jbmc/ArithmeticException4/test.desc
index 00820d86c6e..510065d60f0 100644
--- a/jbmc/regression/jbmc/ArithmeticException4/test.desc
+++ b/jbmc/regression/jbmc/ArithmeticException4/test.desc
@@ -1,6 +1,6 @@
 CORE
 ArithmeticExceptionTest.class
---java-throw-runtime-exceptions
+--throw-runtime-exceptions
 ^EXIT=10$
 ^SIGNAL=0$
 ^.*assertion at file ArithmeticExceptionTest.java line 9 function.*: FAILURE$
diff --git a/jbmc/regression/jbmc/ArithmeticException5/test.desc b/jbmc/regression/jbmc/ArithmeticException5/test.desc
index d57ec32a9a9..508682718d6 100644
--- a/jbmc/regression/jbmc/ArithmeticException5/test.desc
+++ b/jbmc/regression/jbmc/ArithmeticException5/test.desc
@@ -1,6 +1,6 @@
 CORE
 ArithmeticExceptionTest.class
---java-throw-runtime-exceptions
+--throw-runtime-exceptions
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL
diff --git a/jbmc/regression/jbmc/ArithmeticException6/test.desc b/jbmc/regression/jbmc/ArithmeticException6/test.desc
index 8cd09de8d51..17a0f6b4323 100644
--- a/jbmc/regression/jbmc/ArithmeticException6/test.desc
+++ b/jbmc/regression/jbmc/ArithmeticException6/test.desc
@@ -1,6 +1,6 @@
 CORE
 ArithmeticExceptionTest.class
---java-throw-runtime-exceptions --function ArithmeticExceptionTest.main
+--throw-runtime-exceptions --function ArithmeticExceptionTest.main
 ^EXIT=10$
 ^SIGNAL=0$
 ^.*assertion at file ArithmeticExceptionTest.java line 7 function.*: FAILURE$
diff --git a/jbmc/regression/jbmc/ArithmeticException7/test.desc b/jbmc/regression/jbmc/ArithmeticException7/test.desc
index e8f7c941fd4..0339ff4f6d5 100644
--- a/jbmc/regression/jbmc/ArithmeticException7/test.desc
+++ b/jbmc/regression/jbmc/ArithmeticException7/test.desc
@@ -1,6 +1,6 @@
 CORE
 ArithmeticExceptionTest.class
---java-throw-runtime-exceptions
+--throw-runtime-exceptions
 ^EXIT=10$
 ^SIGNAL=0$
 ^.*assertion at file ArithmeticExceptionTest.java line 8 function.*: FAILURE$
diff --git a/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException1/test.desc b/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException1/test.desc
index e6216e07c79..2904f44355d 100644
--- a/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException1/test.desc
+++ b/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException1/test.desc
@@ -1,6 +1,6 @@
 CORE
 ArrayIndexOutOfBoundsExceptionTest.class
---java-throw-runtime-exceptions
+--throw-runtime-exceptions
 ^EXIT=10$
 ^SIGNAL=0$
 ^.*assertion at file ArrayIndexOutOfBoundsExceptionTest.java line 8 function.*: FAILURE$
diff --git a/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException2/test.desc b/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException2/test.desc
index e6216e07c79..2904f44355d 100644
--- a/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException2/test.desc
+++ b/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException2/test.desc
@@ -1,6 +1,6 @@
 CORE
 ArrayIndexOutOfBoundsExceptionTest.class
---java-throw-runtime-exceptions
+--throw-runtime-exceptions
 ^EXIT=10$
 ^SIGNAL=0$
 ^.*assertion at file ArrayIndexOutOfBoundsExceptionTest.java line 8 function.*: FAILURE$
diff --git a/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/test.desc b/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/test.desc
index e6216e07c79..2904f44355d 100644
--- a/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/test.desc
+++ b/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/test.desc
@@ -1,6 +1,6 @@
 CORE
 ArrayIndexOutOfBoundsExceptionTest.class
---java-throw-runtime-exceptions
+--throw-runtime-exceptions
 ^EXIT=10$
 ^SIGNAL=0$
 ^.*assertion at file ArrayIndexOutOfBoundsExceptionTest.java line 8 function.*: FAILURE$
diff --git a/jbmc/regression/jbmc/ClassCastException1/test.desc b/jbmc/regression/jbmc/ClassCastException1/test.desc
index fa84bf185ab..9dd470b881c 100644
--- a/jbmc/regression/jbmc/ClassCastException1/test.desc
+++ b/jbmc/regression/jbmc/ClassCastException1/test.desc
@@ -1,6 +1,6 @@
 CORE
 ClassCastExceptionTest.class
---java-throw-runtime-exceptions
+--throw-runtime-exceptions
 ^EXIT=10$
 ^SIGNAL=0$
 ^.*assertion at file ClassCastExceptionTest.java line 8 function.*: FAILURE$
diff --git a/jbmc/regression/jbmc/ClassCastException2/test.desc b/jbmc/regression/jbmc/ClassCastException2/test.desc
index c593280efe5..e9be3a9d818 100644
--- a/jbmc/regression/jbmc/ClassCastException2/test.desc
+++ b/jbmc/regression/jbmc/ClassCastException2/test.desc
@@ -1,6 +1,6 @@
 CORE
 ClassCastExceptionTest.class
---java-throw-runtime-exceptions
+--throw-runtime-exceptions
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/jbmc/regression/jbmc/ClassCastException3/test.desc b/jbmc/regression/jbmc/ClassCastException3/test.desc
index e2188d63898..e6ba629de3a 100644
--- a/jbmc/regression/jbmc/ClassCastException3/test.desc
+++ b/jbmc/regression/jbmc/ClassCastException3/test.desc
@@ -1,6 +1,6 @@
 CORE
 ClassCastExceptionTest.class
---java-throw-runtime-exceptions
+--throw-runtime-exceptions
 ^EXIT=10$
 ^SIGNAL=0$
 ^.*assertion at file ClassCastExceptionTest.java line 12 function.*: FAILURE$
diff --git a/jbmc/regression/jbmc/NegativeArraySizeException1/test.desc b/jbmc/regression/jbmc/NegativeArraySizeException1/test.desc
index a203a79a628..3c7006827de 100644
--- a/jbmc/regression/jbmc/NegativeArraySizeException1/test.desc
+++ b/jbmc/regression/jbmc/NegativeArraySizeException1/test.desc
@@ -1,6 +1,6 @@
 CORE
 NegativeArraySizeExceptionTest.class
---java-throw-runtime-exceptions
+--throw-runtime-exceptions
 ^EXIT=10$
 ^SIGNAL=0$
 ^.*assertion at file NegativeArraySizeExceptionTest.java line 7 function.*: FAILURE$
diff --git a/jbmc/regression/jbmc/NegativeArraySizeException2/test.desc b/jbmc/regression/jbmc/NegativeArraySizeException2/test.desc
index a203a79a628..3c7006827de 100644
--- a/jbmc/regression/jbmc/NegativeArraySizeException2/test.desc
+++ b/jbmc/regression/jbmc/NegativeArraySizeException2/test.desc
@@ -1,6 +1,6 @@
 CORE
 NegativeArraySizeExceptionTest.class
---java-throw-runtime-exceptions
+--throw-runtime-exceptions
 ^EXIT=10$
 ^SIGNAL=0$
 ^.*assertion at file NegativeArraySizeExceptionTest.java line 7 function.*: FAILURE$
diff --git a/jbmc/regression/jbmc/NullPointerException2/test.desc b/jbmc/regression/jbmc/NullPointerException2/test.desc
index e4ad2c5739d..94828524b2f 100644
--- a/jbmc/regression/jbmc/NullPointerException2/test.desc
+++ b/jbmc/regression/jbmc/NullPointerException2/test.desc
@@ -1,6 +1,6 @@
 CORE
 Test.class
---java-throw-runtime-exceptions
+--throw-runtime-exceptions
 ^EXIT=10$
 ^SIGNAL=0$
 ^.*assertion at file Test.java line 14 function.*: FAILURE$
diff --git a/jbmc/regression/jbmc/NullPointerException3/test.desc b/jbmc/regression/jbmc/NullPointerException3/test.desc
index e4ad2c5739d..94828524b2f 100644
--- a/jbmc/regression/jbmc/NullPointerException3/test.desc
+++ b/jbmc/regression/jbmc/NullPointerException3/test.desc
@@ -1,6 +1,6 @@
 CORE
 Test.class
---java-throw-runtime-exceptions
+--throw-runtime-exceptions
 ^EXIT=10$
 ^SIGNAL=0$
 ^.*assertion at file Test.java line 14 function.*: FAILURE$
diff --git a/jbmc/regression/jbmc/NullPointerException4/test.desc b/jbmc/regression/jbmc/NullPointerException4/test.desc
index 800755d16bb..8ec1d555381 100644
--- a/jbmc/regression/jbmc/NullPointerException4/test.desc
+++ b/jbmc/regression/jbmc/NullPointerException4/test.desc
@@ -1,6 +1,6 @@
 CORE
 Test.class
---java-throw-runtime-exceptions
+--throw-runtime-exceptions
 ^EXIT=10$
 ^SIGNAL=0$
 ^.*assertion at file Test.java line 12 function.*: FAILURE$
diff --git a/jbmc/regression/jbmc/annotations1/show_annotation_symbol.desc b/jbmc/regression/jbmc/annotations1/show_annotation_symbol.desc
index 0735ec2d46d..320f8ac345a 100644
--- a/jbmc/regression/jbmc/annotations1/show_annotation_symbol.desc
+++ b/jbmc/regression/jbmc/annotations1/show_annotation_symbol.desc
@@ -1,6 +1,6 @@
 CORE
 annotations.class
---verbosity 10 --show-symbol-table --function annotations.main
+--no-lazy-methods --verbosity 10 --show-symbol-table --function annotations.main
 ^EXIT=0$
 ^SIGNAL=0$
 ^Type\.\.\.\.\.\.\.\.: @java::ClassAnnotation struct annotations
diff --git a/jbmc/regression/jbmc/cast_null2/test.desc b/jbmc/regression/jbmc/cast_null2/test.desc
index b71b059cd5a..5cce3d56aa5 100644
--- a/jbmc/regression/jbmc/cast_null2/test.desc
+++ b/jbmc/regression/jbmc/cast_null2/test.desc
@@ -1,6 +1,6 @@
 CORE
 test.class
---java-throw-runtime-exceptions --function test.main
+--throw-runtime-exceptions --function test.main
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/jbmc/regression/jbmc/coreModels/test.desc b/jbmc/regression/jbmc/coreModels/test.desc
index 4bda1b0ed61..9390687e25c 100644
--- a/jbmc/regression/jbmc/coreModels/test.desc
+++ b/jbmc/regression/jbmc/coreModels/test.desc
@@ -1,6 +1,6 @@
 CORE
 test.class
---show-symbol-table --cp ../../../src/java_bytecode/library/core-models.jar:.
+--no-lazy-methods --no-refine-strings --show-symbol-table --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
 ^EXIT=0$
 ^SIGNAL=0$
 ^Symbol\s*\.*\: java\:\:org\.cprover\.CProver\.\<init\>\:\(\)V$
diff --git a/jbmc/regression/jbmc/exceptions21/test.desc b/jbmc/regression/jbmc/exceptions21/test.desc
index 24040e046e4..ee88ed7a0a2 100644
--- a/jbmc/regression/jbmc/exceptions21/test.desc
+++ b/jbmc/regression/jbmc/exceptions21/test.desc
@@ -1,6 +1,6 @@
 CORE
 test.class
---function test.f --java-throw-runtime-exceptions
+--function test.f --throw-runtime-exceptions
 ^EXIT=0$
 ^SIGNAL=0$
 VERIFICATION SUCCESSFUL
diff --git a/jbmc/regression/jbmc/exceptions23/test.desc b/jbmc/regression/jbmc/exceptions23/test.desc
index c99eef557dd..69bf18ce113 100644
--- a/jbmc/regression/jbmc/exceptions23/test.desc
+++ b/jbmc/regression/jbmc/exceptions23/test.desc
@@ -1,6 +1,6 @@
 CORE
 test.class
---java-throw-runtime-exceptions --function test.main
+--throw-runtime-exceptions --function test.main
 ^EXIT=10$
 ^SIGNAL=0$
 VERIFICATION FAILED
diff --git a/jbmc/regression/jbmc/exceptions24/test.desc b/jbmc/regression/jbmc/exceptions24/test.desc
index a58943b5d28..403750992f2 100644
--- a/jbmc/regression/jbmc/exceptions24/test.desc
+++ b/jbmc/regression/jbmc/exceptions24/test.desc
@@ -1,6 +1,6 @@
 CORE
 test.class
---java-throw-runtime-exceptions --function test.main
+--throw-runtime-exceptions --function test.main
 ^EXIT=10$
 ^SIGNAL=0$
 VERIFICATION FAILED
diff --git a/jbmc/regression/jbmc/generic_class_bound1/test.desc b/jbmc/regression/jbmc/generic_class_bound1/test.desc
index d4d425ec194..6f623851472 100644
--- a/jbmc/regression/jbmc/generic_class_bound1/test.desc
+++ b/jbmc/regression/jbmc/generic_class_bound1/test.desc
@@ -1,6 +1,6 @@
 CORE symex-driven-lazy-loading-expected-failure
 Gn.class
---cover location
+--cover location --no-lazy-methods --no-refine-strings
 ^EXIT=0$
 ^SIGNAL=0$
 .*file Gn.java line 6 function java::Gn.\<init\>:\(\)V bytecode-index 1 block .: FAILED
diff --git a/jbmc/regression/jbmc/lambda2/test_no_crash.desc b/jbmc/regression/jbmc/lambda2/test_no_crash.desc
index f05242bf10d..0a2a94c84a3 100644
--- a/jbmc/regression/jbmc/lambda2/test_no_crash.desc
+++ b/jbmc/regression/jbmc/lambda2/test_no_crash.desc
@@ -1,6 +1,6 @@
 CORE symex-driven-lazy-loading-expected-failure
 SymStream.class
---verbosity 10 --show-goto-functions
+--no-lazy-methods --verbosity 10 --show-goto-functions
 ^EXIT=0
 ^SIGNAL=0
 --
diff --git a/jbmc/regression/jbmc/lazyloading_synthetic_method_cleanup1/check_clinit_normally_present.desc b/jbmc/regression/jbmc/lazyloading_synthetic_method_cleanup1/check_clinit_normally_present.desc
index 56fb8f416a6..300b49f25b6 100644
--- a/jbmc/regression/jbmc/lazyloading_synthetic_method_cleanup1/check_clinit_normally_present.desc
+++ b/jbmc/regression/jbmc/lazyloading_synthetic_method_cleanup1/check_clinit_normally_present.desc
@@ -1,6 +1,6 @@
 CORE symex-driven-lazy-loading-expected-failure
 Test.class
---show-goto-functions --function Test.main
+--no-lazy-methods --show-goto-functions --function Test.main
 java::Unused::clinit_wrapper
 Unused\.<clinit>\(\)
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc/lazyloading_synthetic_method_cleanup2/check_clinit_normally_present.desc b/jbmc/regression/jbmc/lazyloading_synthetic_method_cleanup2/check_clinit_normally_present.desc
index 3bb1dc48487..46ace60fa73 100644
--- a/jbmc/regression/jbmc/lazyloading_synthetic_method_cleanup2/check_clinit_normally_present.desc
+++ b/jbmc/regression/jbmc/lazyloading_synthetic_method_cleanup2/check_clinit_normally_present.desc
@@ -1,6 +1,6 @@
 CORE symex-driven-lazy-loading-expected-failure
 Test.class
---show-goto-functions --function Test.main
+--no-lazy-methods --show-goto-functions --function Test.main
 java::Unused1::clinit_wrapper
 java::Unused2::clinit_wrapper
 Unused2\.<clinit>\(\)
diff --git a/jbmc/regression/jbmc/lazyloading_synthetic_method_cleanup3/check_clinit_normally_present.desc b/jbmc/regression/jbmc/lazyloading_synthetic_method_cleanup3/check_clinit_normally_present.desc
index a52f8d6cd60..2c0d3865f1e 100644
--- a/jbmc/regression/jbmc/lazyloading_synthetic_method_cleanup3/check_clinit_normally_present.desc
+++ b/jbmc/regression/jbmc/lazyloading_synthetic_method_cleanup3/check_clinit_normally_present.desc
@@ -1,6 +1,6 @@
 CORE symex-driven-lazy-loading-expected-failure
 Test.class
---show-goto-functions --function Test.main
+--no-lazy-methods --show-goto-functions --function Test.main
 java::Opaque\.<clinit>:\(\)V
 java::Opaque::clinit_wrapper
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc/lvt-groovy/test.desc b/jbmc/regression/jbmc/lvt-groovy/test.desc
index 6f8c52c05ca..d78a7de8454 100644
--- a/jbmc/regression/jbmc/lvt-groovy/test.desc
+++ b/jbmc/regression/jbmc/lvt-groovy/test.desc
@@ -1,6 +1,6 @@
 CORE symex-driven-lazy-loading-expected-failure
 DetectSplitPackagesTask.class
---show-symbol-table
+--show-symbol-table --no-lazy-methods --no-refine-strings
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/jbmc/regression/jbmc/no-main-int-array-maybe-null1/test.desc b/jbmc/regression/jbmc/no-main-int-array-maybe-null1/test.desc
index 57b29af8ed2..fa4cca3f657 100644
--- a/jbmc/regression/jbmc/no-main-int-array-maybe-null1/test.desc
+++ b/jbmc/regression/jbmc/no-main-int-array-maybe-null1/test.desc
@@ -1,6 +1,6 @@
 CORE
 Main.class
---function Main.main --java-throw-runtime-exceptions
+--function Main.main --throw-runtime-exceptions
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
diff --git a/jbmc/regression/jbmc/package_friendly1/test.desc b/jbmc/regression/jbmc/package_friendly1/test.desc
index e3250bd8d47..efd3f766756 100644
--- a/jbmc/regression/jbmc/package_friendly1/test.desc
+++ b/jbmc/regression/jbmc/package_friendly1/test.desc
@@ -1,6 +1,6 @@
 CORE symex-driven-lazy-loading-expected-failure
 main.class
---java-load-class package_friendly1 --java-load-class package_friendly2 --show-goto-functions
+--no-lazy-methods --java-load-class package_friendly1 --java-load-class package_friendly2 --show-goto-functions
 ^main[.]main[\(].*[\)].*$
 ^package_friendly2[.]operation2[\(][\)].*$
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc/provide_object_implementation/test.desc b/jbmc/regression/jbmc/provide_object_implementation/test.desc
index 381ae109d1e..ff8518e73f9 100644
--- a/jbmc/regression/jbmc/provide_object_implementation/test.desc
+++ b/jbmc/regression/jbmc/provide_object_implementation/test.desc
@@ -1,6 +1,6 @@
 CORE symex-driven-lazy-loading-expected-failure
 java/lang/Object.class
-
+--no-lazy-methods
 ^EXIT=6$
 ^SIGNAL=0$
 ^the program has no entry point$
diff --git a/jbmc/regression/strings-smoke-tests/java_append_string/test_substring.desc b/jbmc/regression/strings-smoke-tests/java_append_string/test_substring.desc
index dfddb22d72b..a6272d26347 100644
--- a/jbmc/regression/strings-smoke-tests/java_append_string/test_substring.desc
+++ b/jbmc/regression/strings-smoke-tests/java_append_string/test_substring.desc
@@ -1,6 +1,6 @@
 CORE
 test_append_string.class
---refine-strings  --string-max-length 10 --function test_append_string.check --java-assume-inputs-non-null
+--refine-strings  --string-max-input-length 10 --function test_append_string.check --java-assume-inputs-non-null
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.*\].* line 22.* SUCCESS$
diff --git a/jbmc/src/java_bytecode/java_bytecode_language.cpp b/jbmc/src/java_bytecode/java_bytecode_language.cpp
index 76d5b0d839c..663eab78563 100644
--- a/jbmc/src/java_bytecode/java_bytecode_language.cpp
+++ b/jbmc/src/java_bytecode/java_bytecode_language.cpp
@@ -45,24 +45,46 @@ Author: Daniel Kroening, kroening@kroening.com
 void java_bytecode_languaget::get_language_options(const cmdlinet &cmd)
 {
   assume_inputs_non_null=cmd.isset("java-assume-inputs-non-null");
-  string_refinement_enabled=cmd.isset("refine-strings");
-  throw_runtime_exceptions=cmd.isset("java-throw-runtime-exceptions");
+  string_refinement_enabled = !cmd.isset("no-refine-strings");
+  throw_runtime_exceptions =
+    cmd.isset("java-throw-runtime-exceptions") || // will go away
+    cmd.isset("throw-runtime-exceptions");
   assert_uncaught_exceptions = !cmd.isset("disable-uncaught-exception-check");
   throw_assertion_error = cmd.isset("throw-assertion-error");
   threading_support = cmd.isset("java-threading");
 
-  if(cmd.isset("java-max-input-array-length"))
-    object_factory_parameters.max_nondet_array_length=
+  if(cmd.isset("java-max-input-array-length")) // will go away
+  {
+    object_factory_parameters.max_nondet_array_length =
       safe_string2size_t(cmd.get_value("java-max-input-array-length"));
-  if(cmd.isset("java-max-input-tree-depth"))
-    object_factory_parameters.max_nondet_tree_depth=
+  }
+  if(cmd.isset("max-nondet-array-length"))
+  {
+    object_factory_parameters.max_nondet_array_length =
+      safe_string2size_t(cmd.get_value("max-nondet-array-length"));
+  }
+
+  if(cmd.isset("java-max-input-tree-depth")) // will go away
+  {
+    object_factory_parameters.max_nondet_tree_depth =
       safe_string2size_t(cmd.get_value("java-max-input-tree-depth"));
-  if(cmd.isset("string-max-input-length"))
-    object_factory_parameters.max_nondet_string_length=
+  }
+  if(cmd.isset("max-nondet-tree-depth"))
+  {
+    object_factory_parameters.max_nondet_tree_depth =
+      safe_string2size_t(cmd.get_value("max-nondet-tree-depth"));
+  }
+
+  if(cmd.isset("string-max-input-length")) // will go away
+  {
+    object_factory_parameters.max_nondet_string_length =
       safe_string2size_t(cmd.get_value("string-max-input-length"));
-  else if(cmd.isset("string-max-length"))
+  }
+  if(cmd.isset("max-nondet-string-length"))
+  {
     object_factory_parameters.max_nondet_string_length =
-      safe_string2size_t(cmd.get_value("string-max-length"));
+      safe_string2size_t(cmd.get_value("max-nondet-string-length"));
+  }
 
   object_factory_parameters.string_printable = cmd.isset("string-printable");
   if(cmd.isset("java-max-vla-length"))
@@ -70,7 +92,7 @@ void java_bytecode_languaget::get_language_options(const cmdlinet &cmd)
       safe_string2size_t(cmd.get_value("java-max-vla-length"));
   if(cmd.isset("symex-driven-lazy-loading"))
     lazy_methods_mode=LAZY_METHODS_MODE_EXTERNAL_DRIVER;
-  else if(cmd.isset("lazy-methods"))
+  else if(!cmd.isset("no-lazy-methods"))
     lazy_methods_mode=LAZY_METHODS_MODE_CONTEXT_INSENSITIVE;
   else
     lazy_methods_mode=LAZY_METHODS_MODE_EAGER;
diff --git a/jbmc/src/java_bytecode/java_bytecode_language.h b/jbmc/src/java_bytecode/java_bytecode_language.h
index 8c3ca46d77a..9a742b37099 100644
--- a/jbmc/src/java_bytecode/java_bytecode_language.h
+++ b/jbmc/src/java_bytecode/java_bytecode_language.h
@@ -31,12 +31,16 @@ Author: Daniel Kroening, kroening@kroening.com
   "(disable-uncaught-exception-check)" \
   "(throw-assertion-error)" \
   "(java-assume-inputs-non-null)" \
-  "(java-throw-runtime-exceptions)" \
-  "(java-max-input-array-length):" \
-  "(java-max-input-tree-depth):" \
+  "(java-throw-runtime-exceptions)" /* will go away */ \
+  "(throw-runtime-exceptions)" \
+  "(java-max-input-array-length):" /* will go away */ \
+  "(max-nondet-array-length):" \
+  "(java-max-input-tree-depth):"   /* will go away */ \
+  "(max-nondet-tree-depth):" \
   "(java-max-vla-length):" \
   "(java-cp-include-files):" \
-  "(lazy-methods)" \
+  "(lazy-methods)"                 /* will go away */ \
+  "(no-lazy-methods)" \
   "(lazy-methods-extra-entry-point):" \
   "(java-load-class):" \
   "(java-no-load-class):"
@@ -49,16 +53,18 @@ Author: Daniel Kroening, kroening@kroening.com
   "                                  at the location of the assert statement\n"                  /* NOLINT(*) */ \
   " --java-assume-inputs-non-null    never initialize reference-typed parameter to the\n"        /* NOLINT(*) */ \
   "                                  entry point with null\n"                                    /* NOLINT(*) */ \
-  " --java-throw-runtime-exceptions  make implicit runtime exceptions explicit\n"                /* NOLINT(*) */ \
-  " --java-max-input-array-length N  limit input array size to <= N\n"                           /* NOLINT(*) */ \
-  " --java-max-input-tree-depth N    object references are (deterministically) set to null in\n" /* NOLINT(*) */ \
-  "                                  the object\n"                                               /* NOLINT(*) */ \
+  " --throw-runtime-exceptions       make implicit runtime exceptions explicit\n"                /* NOLINT(*) */ \
+  " --max-nondet-array-length N      limit nondet (e.g. input) array size to <= N\n"                           /* NOLINT(*) */ \
+  " --max-nondet-tree-depth N        limit size of nondet (e.g. input) object tree;\n" /* NOLINT(*) */ \
+  "                                  at level N references are set to null\n" /* NOLINT(*) */ \
   " --java-max-vla-length            limit the length of user-code-created arrays\n"             /* NOLINT(*) */ \
   " --java-cp-include-files          regexp or JSON list of files to load (with '@' prefix)\n"   /* NOLINT(*) */ \
-  " --lazy-methods                   only translate methods that appear to be reachable from\n"  /* NOLINT(*) */ \
-  "                                  the --function entry point or main class\n"                 /* NOLINT(*) */ \
+  " --no-lazy-methods                load and translate all methods given on the command line\n" /* NOLINT(*) */ \
+  "                                  and in --classpath\n"                                       /* NOLINT(*) */ \
+  "                                  Default is to load methods that appear to be\n"  /* NOLINT(*) */ \
+  "                                  reachable from the --function entry point or main class\n"       /* NOLINT(*) */ \
   "                                  Note --show-symbol-table/goto-functions/properties output\n"/* NOLINT(*) */ \
-  "                                  will be restricted to loaded methods in this case\n"        /* NOLINT(*) */ \
+  "                                  are restricted to loaded methods by default\n"        /* NOLINT(*) */ \
   " --lazy-methods-extra-entry-point METHODNAME\n"                                               /* NOLINT(*) */ \
   "                                  treat METHODNAME as a possible program entry point for\n"   /* NOLINT(*) */ \
   "                                  the purpose of lazy method loading\n"                       /* NOLINT(*) */ \
diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp
index 7d04c553b96..0283c9346f6 100644
--- a/jbmc/src/jbmc/jbmc_parse_options.cpp
+++ b/jbmc/src/jbmc/jbmc_parse_options.cpp
@@ -242,7 +242,7 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options)
     options.set_option("refine-arithmetic", true);
   }
 
-  if(cmdline.isset("refine-strings"))
+  if(!cmdline.isset("no-refine-strings"))
   {
     options.set_option("refine-strings", true);
     options.set_option("string-printable", cmdline.isset("string-printable"));
@@ -1140,10 +1140,10 @@ void jbmc_parse_optionst::help()
     " --yices                      use Yices\n"
     " --z3                         use Z3\n"
     " --refine                     use refinement procedure (experimental)\n"
-    " --refine-strings             use string refinement (experimental)\n"
+    " --no-refine-strings          turn off string refinement\n"
     " --string-printable           add constraint that strings are printable (experimental)\n" // NOLINT(*)
     " --string-max-length          add constraint on the length of strings\n" // NOLINT(*)
-    " --string-max-input-length    add constraint on the length of input strings\n" // NOLINT(*)
+    " --max-nondet-string-length   bound the length of nondet (e.g. input) strings\n" // NOLINT(*)
     " --outfile filename           output formula to given file\n"
     " --arrays-uf-never            never turn arrays into uninterpreted functions\n" // NOLINT(*)
     " --arrays-uf-always           always turn arrays into uninterpreted functions\n" // NOLINT(*)
diff --git a/jbmc/src/jbmc/jbmc_parse_options.h b/jbmc/src/jbmc/jbmc_parse_options.h
index 616b1d1b9d9..9f5da915be3 100644
--- a/jbmc/src/jbmc/jbmc_parse_options.h
+++ b/jbmc/src/jbmc/jbmc_parse_options.h
@@ -55,10 +55,12 @@ class optionst;
   "(no-sat-preprocessor)" \
   "(beautify)" \
   "(dimacs)(refine)(max-node-refinement):(refine-arrays)(refine-arithmetic)"\
-  "(refine-strings)" \
+  "(refine-strings)" /* will go away */ \
+  "(no-refine-strings)" \
   "(string-printable)" \
   "(string-max-length):" \
-  "(string-max-input-length):" \
+  "(string-max-input-length):" /* will go away */ \
+  "(max-nondet-string-length):" \
   "(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \
   OPT_SHOW_GOTO_FUNCTIONS \
   OPT_SHOW_CLASS_HIERARCHY \
diff --git a/jbmc/src/jdiff/jdiff_parse_options.cpp b/jbmc/src/jdiff/jdiff_parse_options.cpp
index 877aef28c1b..f22a5d722c5 100644
--- a/jbmc/src/jdiff/jdiff_parse_options.cpp
+++ b/jbmc/src/jdiff/jdiff_parse_options.cpp
@@ -88,6 +88,12 @@ void jdiff_parse_optionst::get_command_line_options(optionst &options)
     exit(1);
   }
 
+  // TODO: improve this when language front ends have been
+  //   disentangled from command line parsing
+  // we always require these options
+  cmdline.set("no-lazy-methods");
+  cmdline.set("no-refine-strings");
+
   if(cmdline.isset("cover"))
     parse_cover_options(cmdline, options);
 
diff --git a/jbmc/src/jdiff/jdiff_parse_options.h b/jbmc/src/jdiff/jdiff_parse_options.h
index b23af102930..e562e55a833 100644
--- a/jbmc/src/jdiff/jdiff_parse_options.h
+++ b/jbmc/src/jdiff/jdiff_parse_options.h
@@ -35,6 +35,8 @@ class optionst;
   OPT_GOTO_CHECK \
   "(cover):" \
   "(verbosity):(version)" \
+  "(no-lazy-methods)" /* should go away */ \
+  "(no-refine-strings)" /* should go away */ \
   OPT_TIMESTAMP \
   "u(unified)(change-impact)(forward-impact)(backward-impact)" \
   "(compact-output)"
diff --git a/jbmc/unit/java-testing-utils/load_java_class.cpp b/jbmc/unit/java-testing-utils/load_java_class.cpp
index 29d303a1605..82cab0fd0a0 100644
--- a/jbmc/unit/java-testing-utils/load_java_class.cpp
+++ b/jbmc/unit/java-testing-utils/load_java_class.cpp
@@ -38,17 +38,10 @@ symbol_tablet load_java_class_lazy(
   const std::string &class_path,
   const std::string &main)
 {
-  free_form_cmdlinet lazy_command_line;
-  lazy_command_line.add_flag("lazy-methods");
-
   register_language(new_java_bytecode_language);
 
   return load_java_class(
-    java_class_name,
-    class_path,
-    main,
-    get_language_from_mode(ID_java),
-    lazy_command_line);
+    java_class_name, class_path, main, get_language_from_mode(ID_java));
 }
 
 /// Go through the process of loading, type-checking and finalising loading a
@@ -65,10 +58,18 @@ symbol_tablet load_java_class(
   const std::string &class_path,
   const std::string &main)
 {
+  free_form_cmdlinet command_line;
+  command_line.add_flag("no-lazy-methods");
+  command_line.add_flag("no-refine-strings");
+
   register_language(new_java_bytecode_language);
 
   return load_java_class(
-    java_class_name, class_path, main, get_language_from_mode(ID_java));
+    java_class_name,
+    class_path,
+    main,
+    get_language_from_mode(ID_java),
+    command_line);
 }
 
 /// Go through the process of loading, type-checking and finalising loading a
@@ -161,7 +162,9 @@ symbol_tablet load_java_class(
   const std::string &main,
   std::unique_ptr<languaget> &&java_lang)
 {
-  cmdlinet command_line;
+  free_form_cmdlinet command_line;
+  command_line.add_flag("no-lazy-methods");
+  command_line.add_flag("no-refine-strings");
   // TODO(tkiley): This doesn't do anything as "java-cp-include-files" is an
   // TODO(tkiley): unknown argument. This could be changed by using the
   // TODO(tkiley): free_form_cmdlinet however this causes some tests to fail.