diff --git a/jbmc/regression/jbmc-concurrency/anonymous-java.lang.thread/test.desc b/jbmc/regression/jbmc-concurrency/anonymous-java.lang.thread/test.desc
index e7468745c1d..b1a75f2563d 100644
--- a/jbmc/regression/jbmc-concurrency/anonymous-java.lang.thread/test.desc
+++ b/jbmc/regression/jbmc-concurrency/anonymous-java.lang.thread/test.desc
@@ -1,6 +1,6 @@
 CORE
 A.class
---function 'A.me:()V' --lazy-methods --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading
+--function 'A.me:()V' --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/jbmc/regression/jbmc-concurrency/anonymous-java.lang.thread/test2.desc b/jbmc/regression/jbmc-concurrency/anonymous-java.lang.thread/test2.desc
index 4918125c3a4..a262228e038 100644
--- a/jbmc/regression/jbmc-concurrency/anonymous-java.lang.thread/test2.desc
+++ b/jbmc/regression/jbmc-concurrency/anonymous-java.lang.thread/test2.desc
@@ -1,5 +1,5 @@
 CORE
 A.class
---function 'A.me2:()V' --lazy-methods --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
+--function 'A.me2:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
diff --git a/jbmc/regression/jbmc-concurrency/explicit-thread-blocks/test.desc b/jbmc/regression/jbmc-concurrency/explicit-thread-blocks/test.desc
index 1538f4a7c5c..01ab8385b37 100644
--- a/jbmc/regression/jbmc-concurrency/explicit-thread-blocks/test.desc
+++ b/jbmc/regression/jbmc-concurrency/explicit-thread-blocks/test.desc
@@ -1,6 +1,6 @@
 CORE
 A.class
---function 'A.me:()V' --lazy-methods --java-threading
+--function 'A.me:()V' --java-threading
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL
diff --git a/jbmc/regression/jbmc-concurrency/explicit-thread-blocks/test2.desc b/jbmc/regression/jbmc-concurrency/explicit-thread-blocks/test2.desc
index f7ae486d700..545f4effa2b 100644
--- a/jbmc/regression/jbmc-concurrency/explicit-thread-blocks/test2.desc
+++ b/jbmc/regression/jbmc-concurrency/explicit-thread-blocks/test2.desc
@@ -1,5 +1,5 @@
 CORE
 A.class
---function 'A.me2:()V' --lazy-methods --java-threading
+--function 'A.me2:()V' --java-threading
 ^SIGNAL=0$
 ^VERIFICATION FAILED
diff --git a/jbmc/regression/jbmc-concurrency/get-current-thread/test.desc b/jbmc/regression/jbmc-concurrency/get-current-thread/test.desc
index ff0c14e3779..500630ed419 100644
--- a/jbmc/regression/jbmc-concurrency/get-current-thread/test.desc
+++ b/jbmc/regression/jbmc-concurrency/get-current-thread/test.desc
@@ -1,6 +1,6 @@
 CORE
 A.class
---function 'A.me:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --lazy-methods
+--function 'A.me:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL
diff --git a/jbmc/regression/jbmc-concurrency/get-current-thread/test4.desc b/jbmc/regression/jbmc-concurrency/get-current-thread/test4.desc
index f3bc4b1b843..3ea7924ede3 100644
--- a/jbmc/regression/jbmc-concurrency/get-current-thread/test4.desc
+++ b/jbmc/regression/jbmc-concurrency/get-current-thread/test4.desc
@@ -1,6 +1,6 @@
 CORE
 A.class
---function 'A.me4:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --lazy-methods
+--function 'A.me4:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL
diff --git a/jbmc/regression/jbmc-concurrency/get-current-thread/test5.desc b/jbmc/regression/jbmc-concurrency/get-current-thread/test5.desc
index 88b37371847..9deba6c12de 100644
--- a/jbmc/regression/jbmc-concurrency/get-current-thread/test5.desc
+++ b/jbmc/regression/jbmc-concurrency/get-current-thread/test5.desc
@@ -1,6 +1,6 @@
 CORE
 A.class
---function 'A.me5:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --lazy-methods
+--function 'A.me5:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL
diff --git a/jbmc/regression/jbmc-concurrency/get-current-thread/test6.desc b/jbmc/regression/jbmc-concurrency/get-current-thread/test6.desc
index 7ba18d7a64e..a939961f4a4 100644
--- a/jbmc/regression/jbmc-concurrency/get-current-thread/test6.desc
+++ b/jbmc/regression/jbmc-concurrency/get-current-thread/test6.desc
@@ -1,6 +1,6 @@
 CORE
 A.class
---function 'A.me6:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --lazy-methods
+--function 'A.me6:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL
diff --git a/jbmc/regression/jbmc-concurrency/java-lang-runnable/test.desc b/jbmc/regression/jbmc-concurrency/java-lang-runnable/test.desc
index 95ec31a0c1f..c58629abd8d 100644
--- a/jbmc/regression/jbmc-concurrency/java-lang-runnable/test.desc
+++ b/jbmc/regression/jbmc-concurrency/java-lang-runnable/test.desc
@@ -1,6 +1,6 @@
 CORE
 A.class
---function 'A.me:()V' --lazy-methods --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading
+--function 'A.me:()V' --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL
diff --git a/jbmc/regression/jbmc-concurrency/java-lang-runnable/test2.desc b/jbmc/regression/jbmc-concurrency/java-lang-runnable/test2.desc
index 4ba443c769d..6d75ed56e19 100644
--- a/jbmc/regression/jbmc-concurrency/java-lang-runnable/test2.desc
+++ b/jbmc/regression/jbmc-concurrency/java-lang-runnable/test2.desc
@@ -1,5 +1,5 @@
 CORE
 A.class
---function 'A.me2:()V' --lazy-methods --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading
+--function 'A.me2:()V' --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading
 ^SIGNAL=0$
 ^VERIFICATION FAILED
diff --git a/jbmc/regression/jbmc-concurrency/java-lang-runnable/test3.desc b/jbmc/regression/jbmc-concurrency/java-lang-runnable/test3.desc
index 248eae75e64..5efe6550efd 100644
--- a/jbmc/regression/jbmc-concurrency/java-lang-runnable/test3.desc
+++ b/jbmc/regression/jbmc-concurrency/java-lang-runnable/test3.desc
@@ -1,6 +1,6 @@
 CORE
 A.class
---function 'A.me4:()V' --lazy-methods --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading
+--function 'A.me4:()V' --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL
diff --git a/jbmc/regression/jbmc-concurrency/java-lang-runnable/test4.desc b/jbmc/regression/jbmc-concurrency/java-lang-runnable/test4.desc
index 3db62d553c4..5ae79f1f394 100644
--- a/jbmc/regression/jbmc-concurrency/java-lang-runnable/test4.desc
+++ b/jbmc/regression/jbmc-concurrency/java-lang-runnable/test4.desc
@@ -1,6 +1,6 @@
 CORE
 A.class
---function 'A.me3:()V' --lazy-methods --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading
+--function 'A.me3:()V' --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL
diff --git a/jbmc/regression/jbmc-concurrency/java-lang-thread/test.desc b/jbmc/regression/jbmc-concurrency/java-lang-thread/test.desc
index f28b716eea4..3076c2d7519 100644
--- a/jbmc/regression/jbmc-concurrency/java-lang-thread/test.desc
+++ b/jbmc/regression/jbmc-concurrency/java-lang-thread/test.desc
@@ -1,6 +1,6 @@
 CORE
 A.class
---function 'A.me:()V'  --lazy-methods --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading
+--function 'A.me:()V'  --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL
diff --git a/jbmc/regression/jbmc-concurrency/java-lang-thread/test2.desc b/jbmc/regression/jbmc-concurrency/java-lang-thread/test2.desc
index 29e9ced78d0..9f2b09a20a9 100644
--- a/jbmc/regression/jbmc-concurrency/java-lang-thread/test2.desc
+++ b/jbmc/regression/jbmc-concurrency/java-lang-thread/test2.desc
@@ -1,5 +1,5 @@
 CORE
 A.class
---function 'A.me2:()V' --lazy-methods --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading
+--function 'A.me2:()V' --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
diff --git a/jbmc/regression/jbmc-concurrency/java-lang-thread/test3.desc b/jbmc/regression/jbmc-concurrency/java-lang-thread/test3.desc
index 2ba7df863b5..5c9593f210a 100644
--- a/jbmc/regression/jbmc-concurrency/java-lang-thread/test3.desc
+++ b/jbmc/regression/jbmc-concurrency/java-lang-thread/test3.desc
@@ -1,6 +1,6 @@
 CORE
 A.class
---function 'A.me4:()V' --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading --lazy-methods
+--function 'A.me4:()V' --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/jbmc/regression/jbmc-concurrency/java-lang-thread/test4.desc b/jbmc/regression/jbmc-concurrency/java-lang-thread/test4.desc
index ad3b3639ce5..82910e4f4cf 100644
--- a/jbmc/regression/jbmc-concurrency/java-lang-thread/test4.desc
+++ b/jbmc/regression/jbmc-concurrency/java-lang-thread/test4.desc
@@ -1,6 +1,6 @@
 CORE
 A.class
---function 'A.me3:()V' --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading --lazy-methods
+--function 'A.me3:()V' --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/jbmc/regression/jbmc-concurrency/several-threads/test.desc b/jbmc/regression/jbmc-concurrency/several-threads/test.desc
index ffdd51daf44..599838f0a5e 100644
--- a/jbmc/regression/jbmc-concurrency/several-threads/test.desc
+++ b/jbmc/regression/jbmc-concurrency/several-threads/test.desc
@@ -1,6 +1,6 @@
 CORE
 A.class
---function A.me --lazy-methods --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading
+--function A.me --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL
diff --git a/jbmc/regression/jbmc-concurrency/several-threads/test2.desc b/jbmc/regression/jbmc-concurrency/several-threads/test2.desc
index cdf16ddd945..a6dcc84f557 100644
--- a/jbmc/regression/jbmc-concurrency/several-threads/test2.desc
+++ b/jbmc/regression/jbmc-concurrency/several-threads/test2.desc
@@ -1,5 +1,5 @@
 CORE
 A.class
---function A.me2 --lazy-methods --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading
+--function A.me2 --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
diff --git a/jbmc/regression/jbmc-concurrency/several-threads/test3.desc b/jbmc/regression/jbmc-concurrency/several-threads/test3.desc
index 71b16a75d28..f9e1cd58abe 100644
--- a/jbmc/regression/jbmc-concurrency/several-threads/test3.desc
+++ b/jbmc/regression/jbmc-concurrency/several-threads/test3.desc
@@ -1,6 +1,6 @@
 CORE
 A.class
---function A.me3 --lazy-methods --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading --unwind 3
+--function A.me3 --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading --unwind 3
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/jbmc/regression/jbmc-concurrency/synchronized-blocks-illegal-state/test.desc b/jbmc/regression/jbmc-concurrency/synchronized-blocks-illegal-state/test.desc
index 82ef54ea9ea..47a4a6772fa 100644
--- a/jbmc/regression/jbmc-concurrency/synchronized-blocks-illegal-state/test.desc
+++ b/jbmc/regression/jbmc-concurrency/synchronized-blocks-illegal-state/test.desc
@@ -1,6 +1,6 @@
 KNOWNBUG
 Sync.class
---lazy-methods --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading
+--cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/jbmc/regression/jbmc-concurrency/synchronized-blocks-throw/test.desc b/jbmc/regression/jbmc-concurrency/synchronized-blocks-throw/test.desc
index 493e8c23d1f..f430244ad39 100644
--- a/jbmc/regression/jbmc-concurrency/synchronized-blocks-throw/test.desc
+++ b/jbmc/regression/jbmc-concurrency/synchronized-blocks-throw/test.desc
@@ -1,6 +1,6 @@
 KNOWNBUG
 Sync.class
---cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --lazy-methods --java-threading
+--cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
diff --git a/jbmc/regression/jbmc-concurrency/synchronized-blocks/test.desc b/jbmc/regression/jbmc-concurrency/synchronized-blocks/test.desc
index 7b00c254ec0..b26f5016061 100644
--- a/jbmc/regression/jbmc-concurrency/synchronized-blocks/test.desc
+++ b/jbmc/regression/jbmc-concurrency/synchronized-blocks/test.desc
@@ -1,6 +1,6 @@
 CORE
 A.class
---function 'A.me0:()V' --lazy-methods
+--function 'A.me0:()V'
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/jbmc/regression/jbmc-concurrency/synchronized-blocks/test1.desc b/jbmc/regression/jbmc-concurrency/synchronized-blocks/test1.desc
index 7912d6324d2..9232ded906f 100644
--- a/jbmc/regression/jbmc-concurrency/synchronized-blocks/test1.desc
+++ b/jbmc/regression/jbmc-concurrency/synchronized-blocks/test1.desc
@@ -1,6 +1,6 @@
 CORE
 A.class
---function 'A.me0:()V' --lazy-methods --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --show-goto-functions --java-threading
+--function 'A.me0:()V' --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --show-goto-functions --java-threading
 ATOMIC_BEGIN
 ATOMIC_END
 --
diff --git a/jbmc/regression/jbmc-concurrency/synchronized-blocks/test3.desc b/jbmc/regression/jbmc-concurrency/synchronized-blocks/test3.desc
index 46957f0ab60..74628ecb54d 100644
--- a/jbmc/regression/jbmc-concurrency/synchronized-blocks/test3.desc
+++ b/jbmc/regression/jbmc-concurrency/synchronized-blocks/test3.desc
@@ -1,6 +1,6 @@
 CORE
 A.class
---function 'A.me0:()V' --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --lazy-methods --java-threading
+--function 'A.me0:()V' --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/jbmc/regression/jbmc-concurrency/synchronized-blocks/test4.desc b/jbmc/regression/jbmc-concurrency/synchronized-blocks/test4.desc
index 32d07281ff0..f3105e01093 100644
--- a/jbmc/regression/jbmc-concurrency/synchronized-blocks/test4.desc
+++ b/jbmc/regression/jbmc-concurrency/synchronized-blocks/test4.desc
@@ -1,6 +1,6 @@
 CORE
 A.class
---function 'A.aStatic' --lazy-methods
+--function 'A.aStatic'
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/jbmc/regression/jbmc-concurrency/synchronized-blocks/test_sync.desc b/jbmc/regression/jbmc-concurrency/synchronized-blocks/test_sync.desc
index 9db7060779c..534e87da451 100644
--- a/jbmc/regression/jbmc-concurrency/synchronized-blocks/test_sync.desc
+++ b/jbmc/regression/jbmc-concurrency/synchronized-blocks/test_sync.desc
@@ -1,6 +1,6 @@
 CORE
 A.class
---function 'A.me2:()V' --java-threading --lazy-methods --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
+--function 'A.me2:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/jbmc/regression/jbmc-concurrency/synchronized-blocks/test_sync_baseline.desc b/jbmc/regression/jbmc-concurrency/synchronized-blocks/test_sync_baseline.desc
index 5a49dc43ea9..3d50a965b8c 100644
--- a/jbmc/regression/jbmc-concurrency/synchronized-blocks/test_sync_baseline.desc
+++ b/jbmc/regression/jbmc-concurrency/synchronized-blocks/test_sync_baseline.desc
@@ -1,6 +1,6 @@
 CORE
 A.class
---function 'A.me1:()V' --java-threading --lazy-methods --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
+--function 'A.me1:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/jbmc/regression/jbmc-concurrency/synchronized-method-illegal-state/test.desc b/jbmc/regression/jbmc-concurrency/synchronized-method-illegal-state/test.desc
index 0f19f7ef937..0dfad82a676 100644
--- a/jbmc/regression/jbmc-concurrency/synchronized-method-illegal-state/test.desc
+++ b/jbmc/regression/jbmc-concurrency/synchronized-method-illegal-state/test.desc
@@ -1,6 +1,6 @@
 CORE
 Sync.class
---cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --lazy-methods --java-threading
+--cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/jbmc/regression/jbmc-concurrency/synchronized-methods/test1.desc b/jbmc/regression/jbmc-concurrency/synchronized-methods/test1.desc
index 3f672821a9f..08f6afeac48 100644
--- a/jbmc/regression/jbmc-concurrency/synchronized-methods/test1.desc
+++ b/jbmc/regression/jbmc-concurrency/synchronized-methods/test1.desc
@@ -1,6 +1,6 @@
 CORE
 A.class
---function 'A.me1:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --show-goto-functions --lazy-methods
+--function 'A.me1:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --show-goto-functions
 ATOMIC_BEGIN
 ATOMIC_END
 --
diff --git a/jbmc/regression/jbmc-concurrency/synchronized-methods/test2.desc b/jbmc/regression/jbmc-concurrency/synchronized-methods/test2.desc
index 9ac158bd5e6..f77d63f540a 100644
--- a/jbmc/regression/jbmc-concurrency/synchronized-methods/test2.desc
+++ b/jbmc/regression/jbmc-concurrency/synchronized-methods/test2.desc
@@ -1,6 +1,6 @@
 CORE
 A.class
---function 'A.me1:()V' --java-threading --lazy-methods --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --show-goto-functions
+--function 'A.me1:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --show-goto-functions
 ATOMIC_BEGIN
 ATOMIC_END
 --
diff --git a/jbmc/regression/jbmc-concurrency/synchronized-methods/test3.desc b/jbmc/regression/jbmc-concurrency/synchronized-methods/test3.desc
index 5931228cfa1..bad4684aeb4 100644
--- a/jbmc/regression/jbmc-concurrency/synchronized-methods/test3.desc
+++ b/jbmc/regression/jbmc-concurrency/synchronized-methods/test3.desc
@@ -1,6 +1,6 @@
 CORE
 A.class
---function 'A.me1:()V' --java-threading --lazy-methods --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
+--function 'A.me1:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL
diff --git a/jbmc/regression/jbmc-concurrency/synchronized-methods/test_sync.desc b/jbmc/regression/jbmc-concurrency/synchronized-methods/test_sync.desc
index a4e95fbedeb..131f69beaee 100644
--- a/jbmc/regression/jbmc-concurrency/synchronized-methods/test_sync.desc
+++ b/jbmc/regression/jbmc-concurrency/synchronized-methods/test_sync.desc
@@ -1,6 +1,6 @@
 CORE
 A.class
---function 'A.me3:()V' --java-threading --lazy-methods --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
+--function 'A.me3:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/jbmc/regression/jbmc-concurrency/synchronized-methods/test_sync_baseline.desc b/jbmc/regression/jbmc-concurrency/synchronized-methods/test_sync_baseline.desc
index 9db7060779c..534e87da451 100644
--- a/jbmc/regression/jbmc-concurrency/synchronized-methods/test_sync_baseline.desc
+++ b/jbmc/regression/jbmc-concurrency/synchronized-methods/test_sync_baseline.desc
@@ -1,6 +1,6 @@
 CORE
 A.class
---function 'A.me2:()V' --java-threading --lazy-methods --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
+--function 'A.me2:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/jbmc/regression/jbmc-concurrency/synchronized-methods/test_sync_static.desc b/jbmc/regression/jbmc-concurrency/synchronized-methods/test_sync_static.desc
index c9301aa8459..19a3619ea42 100644
--- a/jbmc/regression/jbmc-concurrency/synchronized-methods/test_sync_static.desc
+++ b/jbmc/regression/jbmc-concurrency/synchronized-methods/test_sync_static.desc
@@ -1,6 +1,6 @@
 KNOWNBUG
 A.class
---function 'A.me4:()V' --java-threading --lazy-methods --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
+--function 'A.me4:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/jbmc/regression/jbmc/NondetInit/test_lazy.desc b/jbmc/regression/jbmc/NondetInit/test_lazy.desc
index bf052725744..4f5f49d33fe 100644
--- a/jbmc/regression/jbmc/NondetInit/test_lazy.desc
+++ b/jbmc/regression/jbmc/NondetInit/test_lazy.desc
@@ -1,9 +1,9 @@
 CORE symex-driven-lazy-loading-expected-failure
 Test.class
---function Test.check --lazy-methods
+--function Test.check
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$
 --
 --
-This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods
+This doesn't work under symex-driven lazy loading because it is incompatible with lazy-methods (default)
diff --git a/jbmc/regression/jbmc/annotations1/show_annotation_symbol.desc b/jbmc/regression/jbmc/annotations1/show_annotation_symbol.desc
index 320f8ac345a..fdcfd0fbaf5 100644
--- a/jbmc/regression/jbmc/annotations1/show_annotation_symbol.desc
+++ b/jbmc/regression/jbmc/annotations1/show_annotation_symbol.desc
@@ -9,4 +9,4 @@ annotations.class
 --
 --
 The purpose of the test is ensuring that annotations can be shown in the symbol
-table.
\ No newline at end of file
+table.
diff --git a/jbmc/regression/jbmc/class-literals/test_lazy.desc b/jbmc/regression/jbmc/class-literals/test_lazy.desc
index 6cef52b953b..2a261398fb8 100644
--- a/jbmc/regression/jbmc/class-literals/test_lazy.desc
+++ b/jbmc/regression/jbmc/class-literals/test_lazy.desc
@@ -1,6 +1,6 @@
 CORE symex-driven-lazy-loading-expected-failure
 Test.class
---lazy-methods --function Test.main
+--function Test.main
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/jbmc/regression/jbmc/cprover-always-load-nondet-initialize/test.desc b/jbmc/regression/jbmc/cprover-always-load-nondet-initialize/test.desc
index 66e55f3e8d7..7c4117e0a10 100644
--- a/jbmc/regression/jbmc/cprover-always-load-nondet-initialize/test.desc
+++ b/jbmc/regression/jbmc/cprover-always-load-nondet-initialize/test.desc
@@ -1,6 +1,6 @@
 KNOWNBUG
 Test.class
---function Test.test --show-goto-functions --lazy-methods
+--function Test.test --show-goto-functions
 EXIT=0
 SIGNAL=0
 ObjectWithNondetInitialize\.cproverNondetInitialize\(\)
diff --git a/jbmc/regression/jbmc/enum_switch/test.desc b/jbmc/regression/jbmc/enum_switch/test.desc
index 6001b0456fb..12d0de868f0 100644
--- a/jbmc/regression/jbmc/enum_switch/test.desc
+++ b/jbmc/regression/jbmc/enum_switch/test.desc
@@ -1,6 +1,6 @@
 CORE symex-driven-lazy-loading-expected-failure
 com/diffblue/regression/Foo.class
---trace --depth 1024 --java-max-vla-length 16 --refine-strings --max-nondet-string-length 20 --string-printable --unwind 10 --function "com.diffblue.regression.Foo.foo" --java-unwind-enum-static
+--trace --depth 1024 --java-max-vla-length 16 --max-nondet-string-length 20 --string-printable --unwind 10 --function "com.diffblue.regression.Foo.foo" --java-unwind-enum-static
 assertion at file com/diffblue/regression/Foo.java line 8 .*: FAILURE
 assertion at file com/diffblue/regression/Foo.java line 11 .*: FAILURE
 assertion at file com/diffblue/regression/Foo.java line 14 .*: FAILURE
diff --git a/jbmc/regression/jbmc/json_trace1/test.desc b/jbmc/regression/jbmc/json_trace1/test.desc
index 52971e9fbd3..80d23cda46c 100644
--- a/jbmc/regression/jbmc/json_trace1/test.desc
+++ b/jbmc/regression/jbmc/json_trace1/test.desc
@@ -6,4 +6,4 @@ Test.class
 --
 ^warning: ignoring
 --
-Tests that it doesn't crash.
\ No newline at end of file
+Tests that it doesn't crash.
diff --git a/jbmc/regression/jbmc/lazyloading1/test.desc b/jbmc/regression/jbmc/lazyloading1/test.desc
index 245446c791a..fd6b98321e1 100644
--- a/jbmc/regression/jbmc/lazyloading1/test.desc
+++ b/jbmc/regression/jbmc/lazyloading1/test.desc
@@ -1,10 +1,10 @@
 CORE symex-driven-lazy-loading-expected-failure
 test.class
---lazy-methods --verbosity 10 --function test.main
+--verbosity 10 --function test.main
 ^EXIT=0$
 ^SIGNAL=0$
 elaborate java::A\.f:\(\)V
 --
 elaborate java::B\.g:\(\)V
 --
-This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods
+This doesn't work under symex-driven lazy loading because it is incompatible with lazy-methods (default)
diff --git a/jbmc/regression/jbmc/lazyloading10/test.desc b/jbmc/regression/jbmc/lazyloading10/test.desc
index eb5a2d31e3b..9941229be9a 100644
--- a/jbmc/regression/jbmc/lazyloading10/test.desc
+++ b/jbmc/regression/jbmc/lazyloading10/test.desc
@@ -1,9 +1,9 @@
 CORE symex-driven-lazy-loading-expected-failure
 test.class
---lazy-methods --verbosity 10 --function test.f --lazy-methods-extra-entry-point test.sety
+--verbosity 10 --function test.f --lazy-methods-extra-entry-point test.sety
 ^SIGNAL=0$
 CI lazy methods: elaborate java::test\.sety:\(I\)V
 CI lazy methods: elaborate java::test\.sety:\(F\)V
 --
 --
-This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods
+This doesn't work under symex-driven lazy loading because it is incompatible with lazy-methods (default)
diff --git a/jbmc/regression/jbmc/lazyloading11/test.desc b/jbmc/regression/jbmc/lazyloading11/test.desc
index 3a3b51770a6..cacd6e6ba89 100644
--- a/jbmc/regression/jbmc/lazyloading11/test.desc
+++ b/jbmc/regression/jbmc/lazyloading11/test.desc
@@ -1,6 +1,6 @@
 CORE symex-driven-lazy-loading-expected-failure
 test.class
---lazy-methods --verbosity 10 --function test.f --lazy-methods-extra-entry-point 'test.sety:\(I\)V' --lazy-methods-extra-entry-point 'test.sety:\(F\)V'
+--verbosity 10 --function test.f --lazy-methods-extra-entry-point 'test.sety:\(I\)V' --lazy-methods-extra-entry-point 'test.sety:\(F\)V'
 ^EXIT=0$
 ^SIGNAL=0$
 VERIFICATION SUCCESSFUL
@@ -9,4 +9,4 @@ CI lazy methods: elaborate java::test\.sety:\(F\)V
 --
 CI lazy methods: elaborate java::test\.setx:\(I\)V
 --
-This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods
+This doesn't work under symex-driven lazy loading because it is incompatible with lazy-methods (default)
diff --git a/jbmc/regression/jbmc/lazyloading2/test.desc b/jbmc/regression/jbmc/lazyloading2/test.desc
index 245446c791a..fd6b98321e1 100644
--- a/jbmc/regression/jbmc/lazyloading2/test.desc
+++ b/jbmc/regression/jbmc/lazyloading2/test.desc
@@ -1,10 +1,10 @@
 CORE symex-driven-lazy-loading-expected-failure
 test.class
---lazy-methods --verbosity 10 --function test.main
+--verbosity 10 --function test.main
 ^EXIT=0$
 ^SIGNAL=0$
 elaborate java::A\.f:\(\)V
 --
 elaborate java::B\.g:\(\)V
 --
-This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods
+This doesn't work under symex-driven lazy loading because it is incompatible with lazy-methods (default)
diff --git a/jbmc/regression/jbmc/lazyloading3/test.desc b/jbmc/regression/jbmc/lazyloading3/test.desc
index 245446c791a..fd6b98321e1 100644
--- a/jbmc/regression/jbmc/lazyloading3/test.desc
+++ b/jbmc/regression/jbmc/lazyloading3/test.desc
@@ -1,10 +1,10 @@
 CORE symex-driven-lazy-loading-expected-failure
 test.class
---lazy-methods --verbosity 10 --function test.main
+--verbosity 10 --function test.main
 ^EXIT=0$
 ^SIGNAL=0$
 elaborate java::A\.f:\(\)V
 --
 elaborate java::B\.g:\(\)V
 --
-This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods
+This doesn't work under symex-driven lazy loading because it is incompatible with lazy-methods (default)
diff --git a/jbmc/regression/jbmc/lazyloading4/test.desc b/jbmc/regression/jbmc/lazyloading4/test.desc
index 9df5b91931e..48a505bdd0b 100644
--- a/jbmc/regression/jbmc/lazyloading4/test.desc
+++ b/jbmc/regression/jbmc/lazyloading4/test.desc
@@ -1,9 +1,9 @@
 CORE symex-driven-lazy-loading-expected-failure
 Main.class
---lazy-methods
+
 ^EXIT=0$
 ^SIGNAL=0$
 VERIFICATION SUCCESSFUL
 --
 --
-This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods
+This doesn't work under symex-driven lazy loading because it is incompatible with lazy-methods (default)
diff --git a/jbmc/regression/jbmc/lazyloading5/test.desc b/jbmc/regression/jbmc/lazyloading5/test.desc
index fa309520217..fad1a03d88c 100644
--- a/jbmc/regression/jbmc/lazyloading5/test.desc
+++ b/jbmc/regression/jbmc/lazyloading5/test.desc
@@ -1,9 +1,9 @@
 CORE symex-driven-lazy-loading-expected-failure
 test.class
---lazy-methods --function test.main
+--function test.main
 ^EXIT=0$
 ^SIGNAL=0$
 VERIFICATION SUCCESSFUL
 --
 --
-This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods
+This doesn't work under symex-driven lazy loading because it is incompatible with lazy-methods (default)
diff --git a/jbmc/regression/jbmc/lazyloading6/test.desc b/jbmc/regression/jbmc/lazyloading6/test.desc
index ce055cbbc7b..950ac43acaf 100644
--- a/jbmc/regression/jbmc/lazyloading6/test.desc
+++ b/jbmc/regression/jbmc/lazyloading6/test.desc
@@ -1,6 +1,6 @@
 CORE symex-driven-lazy-loading-expected-failure
 test.class
---lazy-methods --verbosity 10 --function test.f --lazy-methods-extra-entry-point test.setx
+--verbosity 10 --function test.f --lazy-methods-extra-entry-point test.setx
 ^EXIT=0$
 ^SIGNAL=0$
 VERIFICATION SUCCESSFUL
@@ -9,4 +9,4 @@ CI lazy methods: elaborate java::test\.setx:\(I\)V
 CI lazy methods: elaborate java::test\.sety:\(I\)V
 CI lazy methods: elaborate java::test\.sety:\(F\)V
 --
-This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods
+This doesn't work under symex-driven lazy loading because it is incompatible with lazy-methods (default)
diff --git a/jbmc/regression/jbmc/lazyloading7/test.desc b/jbmc/regression/jbmc/lazyloading7/test.desc
index 10f1aee96f2..f6315b69542 100644
--- a/jbmc/regression/jbmc/lazyloading7/test.desc
+++ b/jbmc/regression/jbmc/lazyloading7/test.desc
@@ -1,6 +1,6 @@
 CORE symex-driven-lazy-loading-expected-failure
 test.class
---lazy-methods --verbosity 10 --function test.f --lazy-methods-extra-entry-point 'test.sety:\(I\)V'
+--verbosity 10 --function test.f --lazy-methods-extra-entry-point 'test.sety:\(I\)V'
 ^EXIT=0$
 ^SIGNAL=0$
 VERIFICATION SUCCESSFUL
@@ -9,4 +9,4 @@ CI lazy methods: elaborate java::test\.sety:\(I\)V
 CI lazy methods: elaborate java::test\.setx:\(I\)V
 CI lazy methods: elaborate java::test\.sety:\(F\)V
 --
-This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods
+This doesn't work under symex-driven lazy loading because it is incompatible with lazy-methods (default)
diff --git a/jbmc/regression/jbmc/lazyloading8/test.desc b/jbmc/regression/jbmc/lazyloading8/test.desc
index ab66e0958ab..735db0f1c28 100644
--- a/jbmc/regression/jbmc/lazyloading8/test.desc
+++ b/jbmc/regression/jbmc/lazyloading8/test.desc
@@ -1,6 +1,6 @@
 CORE symex-driven-lazy-loading-expected-failure
 test.class
---lazy-methods --verbosity 10 --function test.f --lazy-methods-extra-entry-point 'test.sety:\(F\)V'
+--verbosity 10 --function test.f --lazy-methods-extra-entry-point 'test.sety:\(F\)V'
 ^EXIT=0$
 ^SIGNAL=0$
 VERIFICATION SUCCESSFUL
@@ -9,4 +9,4 @@ CI lazy methods: elaborate java::test\.sety:\(F\)V
 CI lazy methods: elaborate java::test\.sety:\(I\)V
 CI lazy methods: elaborate java::test\.setx:\(I\)V
 --
-This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods
+This doesn't work under symex-driven lazy loading because it is incompatible with lazy-methods (default)
diff --git a/jbmc/regression/jbmc/lazyloading9/test.desc b/jbmc/regression/jbmc/lazyloading9/test.desc
index 09f407629c7..05f8a0782e7 100644
--- a/jbmc/regression/jbmc/lazyloading9/test.desc
+++ b/jbmc/regression/jbmc/lazyloading9/test.desc
@@ -1,6 +1,6 @@
 CORE symex-driven-lazy-loading-expected-failure
 test.class
---lazy-methods --verbosity 10 --function test.f --lazy-methods-extra-entry-point 'test.*'
+--verbosity 10 --function test.f --lazy-methods-extra-entry-point 'test.*'
 ^EXIT=0$
 ^SIGNAL=0$
 VERIFICATION SUCCESSFUL
@@ -9,4 +9,4 @@ CI lazy methods: elaborate java::test\.sety:\(I\)V
 CI lazy methods: elaborate java::test\.sety:\(F\)V
 --
 --
-This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods
+This doesn't work under symex-driven lazy loading because it is incompatible with lazy-methods (default)
diff --git a/jbmc/regression/jbmc/lazyloading_array_parameter/test.desc b/jbmc/regression/jbmc/lazyloading_array_parameter/test.desc
index 51ac926c68a..a34bd47c32e 100644
--- a/jbmc/regression/jbmc/lazyloading_array_parameter/test.desc
+++ b/jbmc/regression/jbmc/lazyloading_array_parameter/test.desc
@@ -1,10 +1,10 @@
 CORE symex-driven-lazy-loading-expected-failure
 test.class
---lazy-methods --verbosity 10 --function test.g
+--verbosity 10 --function test.g
 ^EXIT=0$
 ^SIGNAL=0$
 elaborate java::test\.f:\(\)I
 VERIFICATION SUCCESSFUL
 --
 --
-This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods
+This doesn't work under symex-driven lazy loading because it is incompatible with lazy-methods (default)
diff --git a/jbmc/regression/jbmc/lazyloading_cyclic_class/test.desc b/jbmc/regression/jbmc/lazyloading_cyclic_class/test.desc
index fec143df213..ff27c0471a6 100644
--- a/jbmc/regression/jbmc/lazyloading_cyclic_class/test.desc
+++ b/jbmc/regression/jbmc/lazyloading_cyclic_class/test.desc
@@ -1,9 +1,9 @@
 CORE symex-driven-lazy-loading-expected-failure
 test.class
---lazy-methods --verbosity 10 --function test.test
+--verbosity 10 --function test.test
 ^EXIT=0$
 ^SIGNAL=0$
 elaborate java::Base\.f:\(\)V
 --
 --
-This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods
+This doesn't work under symex-driven lazy loading because it is incompatible with lazy-methods (default)
diff --git a/jbmc/regression/jbmc/lazyloading_indirect_array_parameter/test.desc b/jbmc/regression/jbmc/lazyloading_indirect_array_parameter/test.desc
index 51ac926c68a..a34bd47c32e 100644
--- a/jbmc/regression/jbmc/lazyloading_indirect_array_parameter/test.desc
+++ b/jbmc/regression/jbmc/lazyloading_indirect_array_parameter/test.desc
@@ -1,10 +1,10 @@
 CORE symex-driven-lazy-loading-expected-failure
 test.class
---lazy-methods --verbosity 10 --function test.g
+--verbosity 10 --function test.g
 ^EXIT=0$
 ^SIGNAL=0$
 elaborate java::test\.f:\(\)I
 VERIFICATION SUCCESSFUL
 --
 --
-This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods
+This doesn't work under symex-driven lazy loading because it is incompatible with lazy-methods (default)
diff --git a/jbmc/regression/jbmc/lazyloading_indirect_generic_array_parameter/test.desc b/jbmc/regression/jbmc/lazyloading_indirect_generic_array_parameter/test.desc
index 51ac926c68a..a34bd47c32e 100644
--- a/jbmc/regression/jbmc/lazyloading_indirect_generic_array_parameter/test.desc
+++ b/jbmc/regression/jbmc/lazyloading_indirect_generic_array_parameter/test.desc
@@ -1,10 +1,10 @@
 CORE symex-driven-lazy-loading-expected-failure
 test.class
---lazy-methods --verbosity 10 --function test.g
+--verbosity 10 --function test.g
 ^EXIT=0$
 ^SIGNAL=0$
 elaborate java::test\.f:\(\)I
 VERIFICATION SUCCESSFUL
 --
 --
-This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods
+This doesn't work under symex-driven lazy loading because it is incompatible with lazy-methods (default)
diff --git a/jbmc/regression/jbmc/lazyloading_inheritance/test.desc b/jbmc/regression/jbmc/lazyloading_inheritance/test.desc
index 76ed72b1f69..555d93815a2 100644
--- a/jbmc/regression/jbmc/lazyloading_inheritance/test.desc
+++ b/jbmc/regression/jbmc/lazyloading_inheritance/test.desc
@@ -1,6 +1,6 @@
 CORE symex-driven-lazy-loading-expected-failure
 test.class
---lazy-methods --verbosity 10 --function test.test
+--verbosity 10 --function test.test
 ^EXIT=0$
 ^SIGNAL=0$
 elaborate java::Base\.f:\(\)V
@@ -8,4 +8,4 @@ elaborate java::Base\.f:\(\)V
 elaborate java::Derived\.f:\(\)V
 elaborate java::Middle\.f:\(\)V
 --
-This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods
+This doesn't work under symex-driven lazy loading because it is incompatible with lazy-methods (default)
diff --git a/jbmc/regression/jbmc/lazyloading_inheritance_field/test.desc b/jbmc/regression/jbmc/lazyloading_inheritance_field/test.desc
index fec143df213..ff27c0471a6 100644
--- a/jbmc/regression/jbmc/lazyloading_inheritance_field/test.desc
+++ b/jbmc/regression/jbmc/lazyloading_inheritance_field/test.desc
@@ -1,9 +1,9 @@
 CORE symex-driven-lazy-loading-expected-failure
 test.class
---lazy-methods --verbosity 10 --function test.test
+--verbosity 10 --function test.test
 ^EXIT=0$
 ^SIGNAL=0$
 elaborate java::Base\.f:\(\)V
 --
 --
-This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods
+This doesn't work under symex-driven lazy loading because it is incompatible with lazy-methods (default)
diff --git a/jbmc/regression/jbmc/lazyloading_multiple_array_types/test.desc b/jbmc/regression/jbmc/lazyloading_multiple_array_types/test.desc
index faa9503717a..5d0e1e2b27e 100644
--- a/jbmc/regression/jbmc/lazyloading_multiple_array_types/test.desc
+++ b/jbmc/regression/jbmc/lazyloading_multiple_array_types/test.desc
@@ -1,6 +1,6 @@
 CORE symex-driven-lazy-loading-expected-failure
 Test.class
---lazy-methods --verbosity 10 --function Test.check
+--verbosity 10 --function Test.check
 ^EXIT=0$
 ^SIGNAL=0$
 elaborate java::A\.f:\(\)I
@@ -8,4 +8,4 @@ elaborate java::B\.g:\(\)I
 VERIFICATION SUCCESSFUL
 --
 --
-This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods
+This doesn't work under symex-driven lazy loading because it is incompatible with lazy-methods (default)
diff --git a/jbmc/regression/jbmc/lazyloading_multiple_generic_parameters/test.desc b/jbmc/regression/jbmc/lazyloading_multiple_generic_parameters/test.desc
index 51ac926c68a..a34bd47c32e 100644
--- a/jbmc/regression/jbmc/lazyloading_multiple_generic_parameters/test.desc
+++ b/jbmc/regression/jbmc/lazyloading_multiple_generic_parameters/test.desc
@@ -1,10 +1,10 @@
 CORE symex-driven-lazy-loading-expected-failure
 test.class
---lazy-methods --verbosity 10 --function test.g
+--verbosity 10 --function test.g
 ^EXIT=0$
 ^SIGNAL=0$
 elaborate java::test\.f:\(\)I
 VERIFICATION SUCCESSFUL
 --
 --
-This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods
+This doesn't work under symex-driven lazy loading because it is incompatible with lazy-methods (default)
diff --git a/jbmc/regression/jbmc/lazyloading_nested_generic_parameters/test.desc b/jbmc/regression/jbmc/lazyloading_nested_generic_parameters/test.desc
index 579f3933553..0860db2b50d 100644
--- a/jbmc/regression/jbmc/lazyloading_nested_generic_parameters/test.desc
+++ b/jbmc/regression/jbmc/lazyloading_nested_generic_parameters/test.desc
@@ -1,6 +1,6 @@
 KNOWNBUG
 test.class
---lazy-methods --verbosity 10 --function test.g
+--verbosity 10 --function test.g
 ^EXIT=0$
 ^SIGNAL=0$
 elaborate java::test\.f:\(\)I
@@ -11,4 +11,4 @@ The right methods are loaded, but verification is not successful
 because __CPROVER_start doesn't create appropriately typed input for
 this kind of nested generic parameter, so dynamic cast checks fail upon
 fetching the generic type's field.
-This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods
+This doesn't work under symex-driven lazy loading because it is incompatible with lazy-methods (default)
diff --git a/jbmc/regression/jbmc/lazyloading_no_candidates/test.desc b/jbmc/regression/jbmc/lazyloading_no_candidates/test.desc
index a7920b53795..36cdc472496 100644
--- a/jbmc/regression/jbmc/lazyloading_no_candidates/test.desc
+++ b/jbmc/regression/jbmc/lazyloading_no_candidates/test.desc
@@ -1,10 +1,10 @@
 CORE symex-driven-lazy-loading-expected-failure
 Test.class
---lazy-methods --show-goto-functions --verbosity 10 --function Test.main
+--show-goto-functions --verbosity 10 --function Test.main
 ^EXIT=0$
 ^SIGNAL=0$
 ^CI lazy methods: elaborate java::Test\$intf\.f:\(\)V$
 Test\$intf\.f:\(\)V\(\);$
 --
 --
-This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods
+This doesn't work under symex-driven lazy loading because it is incompatible with lazy-methods (default)
diff --git a/jbmc/regression/jbmc/lazyloading_opaquereturn/test.desc b/jbmc/regression/jbmc/lazyloading_opaquereturn/test.desc
index 882dc0b8b44..422bcd0309b 100644
--- a/jbmc/regression/jbmc/lazyloading_opaquereturn/test.desc
+++ b/jbmc/regression/jbmc/lazyloading_opaquereturn/test.desc
@@ -1,6 +1,6 @@
 CORE symex-driven-lazy-loading-expected-failure
 TestClass.class
---function TestClass.testFunction --lazy-methods --verbosity 10
+--function TestClass.testFunction --verbosity 10
 CI lazy methods: elaborate java::Foo\.cproverNondetInitialize:\(\)V
 CI lazy methods: elaborate java::Bar\.cproverNondetInitialize:\(\)V
 CI lazy methods: elaborate java::Baz\.cproverNondetInitialize:\(\)V
@@ -10,4 +10,4 @@ CI lazy methods: elaborate java::GenFiller\.cproverNondetInitialize:\(\)V
 Testing that the return type of an opaque method is correctly elaborated. The
 cproverNondetInitialize should be loaded for all classes where an instance might
 be seen.
-This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods
+This doesn't work under symex-driven lazy loading because it is incompatible with lazy-methods (default)
diff --git a/jbmc/regression/jbmc/lazyloading_recursive_class/test.desc b/jbmc/regression/jbmc/lazyloading_recursive_class/test.desc
index fec143df213..ff27c0471a6 100644
--- a/jbmc/regression/jbmc/lazyloading_recursive_class/test.desc
+++ b/jbmc/regression/jbmc/lazyloading_recursive_class/test.desc
@@ -1,9 +1,9 @@
 CORE symex-driven-lazy-loading-expected-failure
 test.class
---lazy-methods --verbosity 10 --function test.test
+--verbosity 10 --function test.test
 ^EXIT=0$
 ^SIGNAL=0$
 elaborate java::Base\.f:\(\)V
 --
 --
-This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods
+This doesn't work under symex-driven lazy loading because it is incompatible with lazy-methods (default)
diff --git a/jbmc/regression/jbmc/lazyloading_synthetic_method_cleanup1/check_clinit_removed_by_lazy_loading.desc b/jbmc/regression/jbmc/lazyloading_synthetic_method_cleanup1/check_clinit_removed_by_lazy_loading.desc
index 78f4c4ccdb4..3bfc140fff3 100644
--- a/jbmc/regression/jbmc/lazyloading_synthetic_method_cleanup1/check_clinit_removed_by_lazy_loading.desc
+++ b/jbmc/regression/jbmc/lazyloading_synthetic_method_cleanup1/check_clinit_removed_by_lazy_loading.desc
@@ -1,10 +1,10 @@
 CORE symex-driven-lazy-loading-expected-failure
 Test.class
---lazy-methods --show-goto-functions --function Test.main
+--show-goto-functions --function Test.main
 ^EXIT=0$
 ^SIGNAL=0$
 --
 java::Unused::clinit_wrapper
 Unused\.<clinit>\(\)
 --
-This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods
+This doesn't work under symex-driven lazy loading because it is incompatible with lazy-methods (default)
diff --git a/jbmc/regression/jbmc/lazyloading_synthetic_method_cleanup1/check_runs_with_lazy_loading.desc b/jbmc/regression/jbmc/lazyloading_synthetic_method_cleanup1/check_runs_with_lazy_loading.desc
index 3a9e95ea6e9..68a1ab63f3a 100644
--- a/jbmc/regression/jbmc/lazyloading_synthetic_method_cleanup1/check_runs_with_lazy_loading.desc
+++ b/jbmc/regression/jbmc/lazyloading_synthetic_method_cleanup1/check_runs_with_lazy_loading.desc
@@ -1,9 +1,9 @@
 CORE symex-driven-lazy-loading-expected-failure
 Test.class
---lazy-methods --function Test.main
+--function Test.main
 VERIFICATION SUCCESSFUL
 ^EXIT=0$
 ^SIGNAL=0$
 --
 --
-This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods
+This doesn't work under symex-driven lazy loading because it is incompatible with lazy-methods (default)
diff --git a/jbmc/regression/jbmc/lazyloading_synthetic_method_cleanup2/check_clinit_removed_by_lazy_loading.desc b/jbmc/regression/jbmc/lazyloading_synthetic_method_cleanup2/check_clinit_removed_by_lazy_loading.desc
index d0cc65b168d..cecf1766d59 100644
--- a/jbmc/regression/jbmc/lazyloading_synthetic_method_cleanup2/check_clinit_removed_by_lazy_loading.desc
+++ b/jbmc/regression/jbmc/lazyloading_synthetic_method_cleanup2/check_clinit_removed_by_lazy_loading.desc
@@ -1,6 +1,6 @@
 CORE symex-driven-lazy-loading-expected-failure
 Test.class
---lazy-methods --show-goto-functions --function Test.main
+--show-goto-functions --function Test.main
 ^EXIT=0$
 ^SIGNAL=0$
 --
@@ -8,4 +8,4 @@ java::Unused1::clinit_wrapper
 java::Unused2::clinit_wrapper
 Unused2\.<clinit>\(\)
 --
-This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods
+This doesn't work under symex-driven lazy loading because it is incompatible with lazy-methods (default)
diff --git a/jbmc/regression/jbmc/lazyloading_synthetic_method_cleanup2/check_runs_with_lazy_loading.desc b/jbmc/regression/jbmc/lazyloading_synthetic_method_cleanup2/check_runs_with_lazy_loading.desc
index 3a9e95ea6e9..68a1ab63f3a 100644
--- a/jbmc/regression/jbmc/lazyloading_synthetic_method_cleanup2/check_runs_with_lazy_loading.desc
+++ b/jbmc/regression/jbmc/lazyloading_synthetic_method_cleanup2/check_runs_with_lazy_loading.desc
@@ -1,9 +1,9 @@
 CORE symex-driven-lazy-loading-expected-failure
 Test.class
---lazy-methods --function Test.main
+--function Test.main
 VERIFICATION SUCCESSFUL
 ^EXIT=0$
 ^SIGNAL=0$
 --
 --
-This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods
+This doesn't work under symex-driven lazy loading because it is incompatible with lazy-methods (default)
diff --git a/jbmc/regression/jbmc/lazyloading_synthetic_method_cleanup3/check_clinit_removed_by_lazy_loading.desc b/jbmc/regression/jbmc/lazyloading_synthetic_method_cleanup3/check_clinit_removed_by_lazy_loading.desc
index ee136e386e8..452fe1057ea 100644
--- a/jbmc/regression/jbmc/lazyloading_synthetic_method_cleanup3/check_clinit_removed_by_lazy_loading.desc
+++ b/jbmc/regression/jbmc/lazyloading_synthetic_method_cleanup3/check_clinit_removed_by_lazy_loading.desc
@@ -1,10 +1,10 @@
 CORE symex-driven-lazy-loading-expected-failure
 Test.class
---lazy-methods --show-goto-functions --function Test.main
+--show-goto-functions --function Test.main
 ^EXIT=0$
 ^SIGNAL=0$
 --
 java::Opaque\.<clinit>:\(\)V
 java::Opaque::clinit_wrapper
 --
-This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods
+This doesn't work under symex-driven lazy loading because it is incompatible with lazy-methods (default)
diff --git a/jbmc/regression/jbmc/lazyloading_synthetic_method_cleanup3/check_runs_with_lazy_loading.desc b/jbmc/regression/jbmc/lazyloading_synthetic_method_cleanup3/check_runs_with_lazy_loading.desc
index 3a9e95ea6e9..68a1ab63f3a 100644
--- a/jbmc/regression/jbmc/lazyloading_synthetic_method_cleanup3/check_runs_with_lazy_loading.desc
+++ b/jbmc/regression/jbmc/lazyloading_synthetic_method_cleanup3/check_runs_with_lazy_loading.desc
@@ -1,9 +1,9 @@
 CORE symex-driven-lazy-loading-expected-failure
 Test.class
---lazy-methods --function Test.main
+--function Test.main
 VERIFICATION SUCCESSFUL
 ^EXIT=0$
 ^SIGNAL=0$
 --
 --
-This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods
+This doesn't work under symex-driven lazy loading because it is incompatible with lazy-methods (default)
diff --git a/jbmc/regression/jbmc/phi-merge_uninitialized_values/field.desc b/jbmc/regression/jbmc/phi-merge_uninitialized_values/field.desc
index f83a55f6641..043877a2083 100644
--- a/jbmc/regression/jbmc/phi-merge_uninitialized_values/field.desc
+++ b/jbmc/regression/jbmc/phi-merge_uninitialized_values/field.desc
@@ -13,4 +13,4 @@ statement:
 
  (guard ? dynamic_object2@3#1 : dynamic_object3@3#0)
 
-Should not appear. First regex deals with when the gen zero is the latter position, second when it's in the former.
\ No newline at end of file
+Should not appear. First regex deals with when the gen zero is the latter position, second when it's in the former.
diff --git a/jbmc/regression/jbmc/phi-merge_uninitialized_values/local.desc b/jbmc/regression/jbmc/phi-merge_uninitialized_values/local.desc
index 0369f5967a7..00d1f483af2 100644
--- a/jbmc/regression/jbmc/phi-merge_uninitialized_values/local.desc
+++ b/jbmc/regression/jbmc/phi-merge_uninitialized_values/local.desc
@@ -13,4 +13,4 @@ statement:
 
  (guard ? dynamic_object2@3#1 : dynamic_object3@3#0)
 
-Should not appear. First regex deals with when the gen zero is the latter position, second when it's in the former.
\ No newline at end of file
+Should not appear. First regex deals with when the gen zero is the latter position, second when it's in the former.
diff --git a/jbmc/regression/jbmc/phi-merge_uninitialized_values/static_field.desc b/jbmc/regression/jbmc/phi-merge_uninitialized_values/static_field.desc
index 6289e5f872a..09065cbb5c6 100644
--- a/jbmc/regression/jbmc/phi-merge_uninitialized_values/static_field.desc
+++ b/jbmc/regression/jbmc/phi-merge_uninitialized_values/static_field.desc
@@ -13,4 +13,4 @@ statement:
 
  (guard ? dynamic_object2@3#1 : dynamic_object3@3#0)
 
-Should not appear. First regex deals with when the gen zero is the latter position, second when it's in the former.
\ No newline at end of file
+Should not appear. First regex deals with when the gen zero is the latter position, second when it's in the former.
diff --git a/jbmc/regression/jbmc/remove_virtual_function_typecast/test.desc b/jbmc/regression/jbmc/remove_virtual_function_typecast/test.desc
index defa750d6ab..19f4520679f 100644
--- a/jbmc/regression/jbmc/remove_virtual_function_typecast/test.desc
+++ b/jbmc/regression/jbmc/remove_virtual_function_typecast/test.desc
@@ -1,6 +1,6 @@
 CORE symex-driven-lazy-loading-expected-failure
 VirtualFunctions.class
---lazy-methods --java-max-vla-length 48 --unwind 8 --java-unwind-enum-static --trace --function VirtualFunctions.check --show-goto-functions
+--java-max-vla-length 48 --unwind 8 --java-unwind-enum-static --trace --function VirtualFunctions.check --show-goto-functions
  \(struct VirtualFunctions\$B \*\)a \. VirtualFunctions\$B\.f:\(\)V\(\);$
  a \. VirtualFunctions\$A\.f:\(\)V\(\);$
  b \. VirtualFunctions\$B\.f:\(\)V\(\);$
@@ -9,4 +9,4 @@ VirtualFunctions.class
 ^SIGNAL=0$
 --
 --
-This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods
+This doesn't work under symex-driven lazy loading because it is incompatible with lazy-methods (default)
diff --git a/jbmc/regression/jbmc/removed_virtual_functions/test.desc b/jbmc/regression/jbmc/removed_virtual_functions/test.desc
index 632fb272be9..07f70aeaf7c 100644
--- a/jbmc/regression/jbmc/removed_virtual_functions/test.desc
+++ b/jbmc/regression/jbmc/removed_virtual_functions/test.desc
@@ -1,10 +1,10 @@
 CORE symex-driven-lazy-loading-expected-failure
 ArrayListEquals.class
---lazy-methods --java-max-vla-length 48 --unwind 8 --java-unwind-enum-static --trace --function ArrayListEquals.check2 --show-goto-functions
+--java-max-vla-length 48 --unwind 8 --java-unwind-enum-static --trace --function ArrayListEquals.check2 --show-goto-functions
 e2 . ArrayList\$Itr.hasNext:\(\)Z\(\);
 ^EXIT=0$
 ^SIGNAL=0$
 --
 e2 . ListIterator.hasNext:\(\)Z\(\);
 --
-This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods
+This doesn't work under symex-driven lazy loading because it is incompatible with lazy-methods (default)
diff --git a/jbmc/regression/jbmc/string_field_aliasing/test.desc b/jbmc/regression/jbmc/string_field_aliasing/test.desc
index f3e41c0662f..62e5918320d 100644
--- a/jbmc/regression/jbmc/string_field_aliasing/test.desc
+++ b/jbmc/regression/jbmc/string_field_aliasing/test.desc
@@ -1,6 +1,6 @@
 CORE
 Cart.class
---cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --trace --java-max-vla-length 96 --refine-strings --java-unwind-enum-static --max-nondet-string-length 200 --unwind 4 Cart.class --function Cart.checkTax4 --string-printable
+--cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --trace --java-max-vla-length 96 --java-unwind-enum-static --max-nondet-string-length 200 --unwind 4 Cart.class --function Cart.checkTax4 --string-printable
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
diff --git a/jbmc/src/java_bytecode/java_bytecode_language.cpp b/jbmc/src/java_bytecode/java_bytecode_language.cpp
index e55fc3e0a03..4e62c8d5683 100644
--- a/jbmc/src/java_bytecode/java_bytecode_language.cpp
+++ b/jbmc/src/java_bytecode/java_bytecode_language.cpp
@@ -46,40 +46,23 @@ 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("no-refine-strings");
-  throw_runtime_exceptions =
-    cmd.isset("java-throw-runtime-exceptions") || // will go away
-    cmd.isset("throw-runtime-exceptions");
+  throw_runtime_exceptions = 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")) // will go away
-  {
-    object_factory_parameters.max_nondet_array_length =
-      safe_string2size_t(cmd.get_value("java-max-input-array-length"));
-  }
   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("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"));
-  }
   if(cmd.isset("max-nondet-string-length"))
   {
     object_factory_parameters.max_nondet_string_length =
diff --git a/jbmc/src/java_bytecode/java_bytecode_language.h b/jbmc/src/java_bytecode/java_bytecode_language.h
index c72a492f504..cd428390f74 100644
--- a/jbmc/src/java_bytecode/java_bytecode_language.h
+++ b/jbmc/src/java_bytecode/java_bytecode_language.h
@@ -31,15 +31,11 @@ Author: Daniel Kroening, kroening@kroening.com
   "(disable-uncaught-exception-check)" \
   "(throw-assertion-error)" \
   "(java-assume-inputs-non-null)" \
-  "(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)" /* will go away */ \
   "(no-lazy-methods)" \
   "(lazy-methods-extra-entry-point):" \
   "(java-load-class):" \
diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp
index 7d134f4dfff..ddfa8cbe9fc 100644
--- a/jbmc/src/jbmc/jbmc_parse_options.cpp
+++ b/jbmc/src/jbmc/jbmc_parse_options.cpp
@@ -355,7 +355,6 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options)
     for(const char *opt :
       { "nondet-static",
         "full-slice",
-        "lazy-methods",
         "reachability-slice",
         "reachability-slice-fb" })
     {
@@ -485,18 +484,16 @@ int jbmc_parse_optionst::doit()
   }
 
   object_factory_params.max_nondet_array_length =
-    cmdline.isset("java-max-input-array-length")
-      ? std::stoul(cmdline.get_value("java-max-input-array-length"))
+    cmdline.isset("max-nondet-array-length")
+      ? std::stoul(cmdline.get_value("max-nondet-array-length"))
       : MAX_NONDET_ARRAY_LENGTH_DEFAULT;
   object_factory_params.max_nondet_string_length =
     cmdline.isset("max-nondet-string-length")
       ? std::stoul(cmdline.get_value("max-nondet-string-length"))
-      : cmdline.isset("string-max-input-length") // obsolete; will go away
-        ? std::stoul(cmdline.get_value("string-max-input-length"))
-        : MAX_NONDET_STRING_LENGTH;
+      : MAX_NONDET_STRING_LENGTH;
   object_factory_params.max_nondet_tree_depth =
-    cmdline.isset("java-max-input-tree-depth")
-      ? std::stoul(cmdline.get_value("java-max-input-tree-depth"))
+    cmdline.isset("max-nondet-tree-depth")
+      ? std::stoul(cmdline.get_value("max-nondet-tree-depth"))
       : MAX_NONDET_TREE_DEPTH;
 
   stub_objects_are_not_null = cmdline.isset("java-assume-inputs-non-null");
@@ -1087,9 +1084,7 @@ void jbmc_parse_optionst::help()
     " --yices                      use Yices\n"
     " --z3                         use Z3\n"
     " --refine                     use refinement procedure (experimental)\n"
-    " --no-refine-strings          turn off string refinement\n"
-    " --string-printable           restrict to printable strings (experimental)\n" // NOLINT(*)
-    " --max-nondet-string-length   bound the length of nondet (e.g. input) strings\n" // NOLINT(*)
+    HELP_STRING_REFINEMENT
     " --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 69d7f5a0a8b..f7566cce981 100644
--- a/jbmc/src/jbmc/jbmc_parse_options.h
+++ b/jbmc/src/jbmc/jbmc_parse_options.h
@@ -29,6 +29,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <goto-symex/path_storage.h>
 
+#include <solvers/refinement/string_refinement.h>
+
 #include <java_bytecode/java_bytecode_language.h>
 
 class bmct;
@@ -52,11 +54,7 @@ class optionst;
   "(no-sat-preprocessor)" \
   "(beautify)" \
   "(dimacs)(refine)(max-node-refinement):(refine-arrays)(refine-arithmetic)"\
-  "(refine-strings)" /* will go away */ \
-  "(no-refine-strings)" \
-  "(string-printable)" \
-  "(string-max-input-length):" /* will go away */ \
-  "(max-nondet-string-length):" \
+  OPT_STRING_REFINEMENT \
   "(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \
   OPT_SHOW_GOTO_FUNCTIONS \
   OPT_SHOW_CLASS_HIERARCHY \
diff --git a/jbmc/src/jbmc/module_dependencies.txt b/jbmc/src/jbmc/module_dependencies.txt
index 1c492ac0359..e32209916e0 100644
--- a/jbmc/src/jbmc/module_dependencies.txt
+++ b/jbmc/src/jbmc/module_dependencies.txt
@@ -9,4 +9,5 @@ jbmc
 langapi # should go away
 linking
 pointer-analysis
+solvers/refinement
 util
diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
index 964b64410f2..b59f801b08e 100644
--- a/src/cbmc/cbmc_parse_options.cpp
+++ b/src/cbmc/cbmc_parse_options.cpp
@@ -300,9 +300,6 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
   {
     options.set_option("refine-strings", true);
     options.set_option("string-printable", cmdline.isset("string-printable"));
-    if(cmdline.isset("string-max-length"))
-      options.set_option(
-        "string-max-length", cmdline.get_value("string-max-length"));
   }
 
   if(cmdline.isset("max-node-refinement"))
@@ -962,11 +959,7 @@ void cbmc_parse_optionst::help()
     " --yices                      use Yices\n"
     " --z3                         use Z3\n"
     " --refine                     use refinement procedure (experimental)\n"
-    " --refine-strings             use string refinement (experimental)\n"
-    " --string-printable           add constraint that strings are printable (experimental)\n" // NOLINT(*)
-    " --string-max-input-length    add constraint on the length of input strings\n" // NOLINT(*)
-    " --string-max-length          add constraint on the length of strings\n"
-    "                              (deprecated: use string-max-input-length instead)\n" // NOLINT(*)
+    HELP_STRING_REFINEMENT_CBMC
     " --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/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h
index d36f976573a..fcc207ffb20 100644
--- a/src/cbmc/cbmc_parse_options.h
+++ b/src/cbmc/cbmc_parse_options.h
@@ -22,6 +22,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <goto-programs/goto_trace.h>
 
+#include <solvers/refinement/string_refinement.h>
+
 #include "bmc.h"
 #include "xml_interface.h"
 #include "cbmc_solvers.h"
@@ -48,10 +50,7 @@ class optionst;
   "(no-sat-preprocessor)" \
   "(beautify)" \
   "(dimacs)(refine)(max-node-refinement):(refine-arrays)(refine-arithmetic)"\
-  "(refine-strings)" \
-  "(string-printable)" \
-  "(string-max-length):" \
-  "(string-max-input-length):" \
+  OPT_STRING_REFINEMENT_CBMC \
   "(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \
   "(little-endian)(big-endian)" \
   OPT_SHOW_GOTO_FUNCTIONS \
diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp
index 42599b48378..d9262493cfb 100644
--- a/src/solvers/refinement/string_refinement.cpp
+++ b/src/solvers/refinement/string_refinement.cpp
@@ -924,7 +924,7 @@ static optionalt<exprt> get_array(
   {
     stream << "(sr::get_array) long string (size " << format(arr.length())
            << " = " << n << ") " << format(arr) << eom;
-    stream << "(sr::get_array) consider reducing string-max-input-length so "
+    stream << "(sr::get_array) consider reducing max-nondet-string-length so "
               "that no string exceeds "
            << MAX_CONCRETE_STRING_SIZE
            << " in length and "
diff --git a/src/solvers/refinement/string_refinement.h b/src/solvers/refinement/string_refinement.h
index 76bc3cc06c7..7ee5a580d26 100644
--- a/src/solvers/refinement/string_refinement.h
+++ b/src/solvers/refinement/string_refinement.h
@@ -29,6 +29,28 @@ Author: Alberto Griggio, alberto.griggio@gmail.com
 #include <solvers/refinement/string_refinement_invariant.h>
 #include <solvers/refinement/string_refinement_util.h>
 
+// clang-format off
+#define OPT_STRING_REFINEMENT \
+  "(no-refine-strings)" \
+  "(string-printable)" \
+  "(max-nondet-string-length):"
+
+#define HELP_STRING_REFINEMENT \
+  " --no-refine-strings          turn off string refinement\n" \
+  " --string-printable           restrict to printable strings (experimental)\n" /* NOLINT(*) */ \
+  " --max-nondet-string-length n bound the length of nondet (e.g. input) strings\n" /* NOLINT(*) */
+
+// The integration of the string solver into CBMC is incomplete. Therefore,
+// it is not turned on by default and not all options are available.
+#define OPT_STRING_REFINEMENT_CBMC \
+  "(refine-strings)" \
+  "(string-printable)"
+
+#define HELP_STRING_REFINEMENT_CBMC \
+  " --refine-strings             use string refinement (experimental)\n" \
+  " --string-printable           restrict to printable strings (experimental)\n" /* NOLINT(*) */
+// clang-format on
+
 #define DEFAULT_MAX_NB_REFINEMENT std::numeric_limits<size_t>::max()
 
 class string_refinementt final: public bv_refinementt