Further JBMC options clean-up

jbmc/regression/jbmc-strings/CharacterGetNumericValue/test.desc

@@ -1,6 +1,6 @@
 CORE
 test.class
---refine-strings --string-max-length 1000
+--max-nondet-string-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 assertion at file test.java line 8 .* SUCCESS$

jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/test.desc

@@ -1,12 +1,12 @@
 CORE
 Test.class
---function Test.testme
+--no-refine-strings --function Test.testme
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
 type mismatch
 --
 Before cbmc#2472 this would assume that StringBuilder's direct parent was
-java.lang.Object, causing a type mismatch when --refine-strings was not in use
+java.lang.Object, causing a type mismatch when --no-refine-strings was in use
 (which at the time would assume that parent-child relationship)

jbmc/regression/jbmc-strings/RegexMatches01/test.desc

@@ -1,6 +1,6 @@
 FUTURE
 RegexMatches01.class
---refine-strings --string-max-length 1000 --unwind 100
+--max-nondet-string-length 1000 --unwind 100
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

jbmc/regression/jbmc-strings/RegexMatches02/test.desc

@@ -1,6 +1,6 @@
 FUTURE
 RegexMatches02.class
---refine-strings --string-max-length 1000 --unwind 100
+--max-nondet-string-length 1000 --unwind 100
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

jbmc/regression/jbmc-strings/RegexSubstitution01/test.desc

@@ -1,6 +1,6 @@
 FUTURE
 RegexSubstitution01.class
---refine-strings --string-max-length 1000
+--max-nondet-string-length 1000
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

jbmc/regression/jbmc-strings/RegexSubstitution02/test.desc

@@ -1,6 +1,6 @@
 FUTURE
 RegexSubstitution02.class
---refine-strings --string-max-length 1000
+--max-nondet-string-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

jbmc/regression/jbmc-strings/RegexSubstitution03/test.desc

@@ -1,6 +1,6 @@
 FUTURE
 RegexSubstitution03.class
---refine-strings --string-max-length 1000
+--max-nondet-string-length 1000
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

jbmc/regression/jbmc-strings/StartsWith/test.desc

@@ -1,6 +1,6 @@
 CORE
 Test.class
---refine-strings --string-max-input-length 10 --unwind 10 --function Test.check
+--max-nondet-string-length 10 --unwind 10 --function Test.check
 ^EXIT=10$
 ^SIGNAL=0$
 assertion at file Test.java line 31 .*: SUCCESS

jbmc/regression/jbmc-strings/StartsWith/test_det.desc

@@ -1,6 +1,6 @@
 CORE
 Test.class
---refine-strings --string-max-input-length 100 --unwind 10 --function Test.checkDet
+--max-nondet-string-length 100 --unwind 10 --function Test.checkDet
 ^EXIT=10$
 ^SIGNAL=0$
 assertion at file Test.java line 41 .*: SUCCESS

jbmc/regression/jbmc-strings/StartsWith/test_nondet.desc

@@ -1,6 +1,6 @@
 CORE
 Test.class
---refine-strings --string-max-input-length 100 --unwind 10 --function Test.checkNonDet
+--max-nondet-string-length 100 --unwind 10 --function Test.checkNonDet
 ^EXIT=10$
 ^SIGNAL=0$
 assertion at file Test.java line 66 .*: SUCCESS

jbmc/regression/jbmc-strings/StaticCharMethods01/test.desc

@@ -1,6 +1,6 @@
 CORE
 StaticCharMethods01.class
---refine-strings --string-max-length 1000
+--max-nondet-string-length 1000
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

jbmc/regression/jbmc-strings/StaticCharMethods02/test.desc

@@ -1,6 +1,6 @@
 CORE
 StaticCharMethods02.class
---refine-strings --string-max-length 1000
+--max-nondet-string-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

jbmc/regression/jbmc-strings/StaticCharMethods03/test.desc

@@ -1,6 +1,6 @@
 CORE
 StaticCharMethods03.class
---refine-strings --string-max-length 1000
+--max-nondet-string-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion\.1\] .* line 6 .* FAILURE$

jbmc/regression/jbmc-strings/StaticCharMethods04/test.desc

@@ -1,6 +1,6 @@
 CORE
 StaticCharMethods04.class
---refine-strings --string-max-length 1000
+--max-nondet-string-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

jbmc/regression/jbmc-strings/StaticCharMethods05/test.desc

@@ -1,6 +1,6 @@
 CORE
 StaticCharMethods05.class
---refine-strings --string-max-length 1000
+--max-nondet-string-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion\.1\] .* line 12 .* FAILURE$

jbmc/regression/jbmc-strings/StaticCharMethods06/test.desc

@@ -1,6 +1,6 @@
 FUTURE
 StaticCharMethods06.class
---refine-strings --string-max-length 1000
+--max-nondet-string-length 1000
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

jbmc/regression/jbmc-strings/StringArray/test.desc

@@ -1,6 +1,6 @@
 CORE
 Test.class
---refine-strings --function Test.check --string-max-input-length 1000
+--function Test.check --max-nondet-string-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion\.1\].* line 20.* SUCCESS$

jbmc/regression/jbmc-strings/StringBuilderAppend01/test.desc

@@ -1,6 +1,6 @@
 FUTURE
 StringBuilderAppend01.class
---refine-strings --string-max-length 1000
+--max-nondet-string-length 1000
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

jbmc/regression/jbmc-strings/StringBuilderAppend02/test.desc

@@ -1,6 +1,6 @@
 FUTURE
 StringBuilderAppend02.class
---refine-strings --string-max-length 1000
+--max-nondet-string-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

jbmc/regression/jbmc-strings/StringBuilderCapLen01/test.desc

@@ -1,6 +1,6 @@
 FUTURE
 StringBuilderCapLen01.class
---refine-strings --string-max-length 1000
+--max-nondet-string-length 1000
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

jbmc/regression/jbmc-strings/StringBuilderCapLen02/test.desc

@@ -1,6 +1,6 @@
 FUTURE
 StringBuilderCapLen02.class
---refine-strings --string-max-length 1000
+--max-nondet-string-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

jbmc/regression/jbmc-strings/StringBuilderCapLen03/test.desc

@@ -1,6 +1,6 @@
 FUTURE
 StringBuilderCapLen03.class
---refine-strings --string-max-length 1000
+--max-nondet-string-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

jbmc/regression/jbmc-strings/StringBuilderCapLen04/test.desc

@@ -1,6 +1,6 @@
 FUTURE
 StringBuilderCapLen04.class
---refine-strings --string-max-length 1000
+--max-nondet-string-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

jbmc/regression/jbmc-strings/StringBuilderChars01/test.desc

@@ -1,6 +1,6 @@
 FUTURE
 StringBuilderChars01.class
---refine-strings --string-max-length 1000 --unwind 100
+--max-nondet-string-length 1000 --unwind 100
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

jbmc/regression/jbmc-strings/StringBuilderChars02/test.desc

@@ -1,6 +1,6 @@
 FUTURE
 StringBuilderChars02.class
---refine-strings --string-max-length 1000 --unwind 100
+--max-nondet-string-length 1000 --unwind 100
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

jbmc/regression/jbmc-strings/StringBuilderChars03/test.desc

@@ -1,6 +1,6 @@
 FUTURE
 StringBuilderChars03.class
---refine-strings --string-max-length 1000 --unwind 100
+--max-nondet-string-length 1000 --unwind 100
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

jbmc/regression/jbmc-strings/StringBuilderChars04/test.desc

@@ -1,6 +1,6 @@
 FUTURE
 StringBuilderChars04.class
---refine-strings --string-max-length 1000 --unwind 100
+--max-nondet-string-length 1000 --unwind 100
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

jbmc/regression/jbmc-strings/StringBuilderChars05/test.desc

@@ -1,6 +1,6 @@
 FUTURE
 StringBuilderChars05.class
---refine-strings --string-max-length 1000 --unwind 100
+--max-nondet-string-length 1000 --unwind 100
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

jbmc/regression/jbmc-strings/StringBuilderChars06/test.desc

@@ -1,6 +1,6 @@
 FUTURE
 StringBuilderChars06.class
---refine-strings --string-max-length 1000 --unwind 100
+--max-nondet-string-length 1000 --unwind 100
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

jbmc/regression/jbmc-strings/StringBuilderConstructors01/test.desc

@@ -1,6 +1,6 @@
 KNOWNBUG
 StringBuilderConstructors01.class
---refine-strings --string-max-length 1000
+--max-nondet-string-length 1000
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

jbmc/regression/jbmc-strings/StringBuilderConstructors02/test.desc

@@ -1,6 +1,6 @@
 KNOWNBUG
 StringBuilderConstructors02.class
---refine-strings --string-max-length 1000
+--max-nondet-string-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

jbmc/regression/jbmc-strings/StringBuilderInsert/test.desc

@@ -1,6 +1,6 @@
 CORE
 Test.class
---refine-strings --function Test.check
+--function Test.check
 ^EXIT=10$
 ^SIGNAL=0$
 assertion at file Test.java line 13 .*: SUCCESS

jbmc/regression/jbmc-strings/StringBuilderInsertDelete01/test.desc

@@ -1,6 +1,6 @@
 FUTURE
 StringBuilderInsertDelete01.class
---refine-strings --string-max-length 1000
+--max-nondet-string-length 1000
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

jbmc/regression/jbmc-strings/StringBuilderInsertDelete02/test.desc

@@ -1,6 +1,6 @@
 FUTURE
 StringBuilderInsertDelete02.class
---refine-strings --string-max-length 1000
+--max-nondet-string-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

jbmc/regression/jbmc-strings/StringBuilderInsertDelete03/test.desc

@@ -1,6 +1,6 @@
 FUTURE
 StringBuilderInsertDelete03.class
---refine-strings --string-max-length 1000
+--max-nondet-string-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

jbmc/regression/jbmc-strings/StringCompare01/test.desc

@@ -1,6 +1,6 @@
 FUTURE
 StringCompare01.class
---refine-strings --string-max-length 1000
+--max-nondet-string-length 1000
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

jbmc/regression/jbmc-strings/StringCompare02/test.desc

@@ -1,6 +1,6 @@
 CORE
 StringCompare02.class
---refine-strings --string-max-length 1000
+--max-nondet-string-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion\.1\] .* line 12 .* FAILURE$

jbmc/regression/jbmc-strings/StringCompare03/test.desc

@@ -1,6 +1,6 @@
 CORE
 StringCompare03.class
---refine-strings --string-max-length 1000
+--max-nondet-string-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion\.1\] .* line 12 .* FAILURE$

jbmc/regression/jbmc-strings/StringCompare04/test.desc

@@ -1,6 +1,6 @@
 CORE
 StringCompare04.class
---refine-strings --string-max-length 1000
+--max-nondet-string-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

jbmc/regression/jbmc-strings/StringCompare05/test.desc

@@ -1,6 +1,6 @@
 CORE
 StringCompare05.class
---refine-strings --string-max-length 1000
+--max-nondet-string-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

jbmc/regression/jbmc-strings/StringConcat/test_buffer_det.desc

@@ -1,6 +1,6 @@
 CORE
 Test.class
---refine-strings --string-max-length 1000 --string-max-input-length 100 --function Test.bufferDet --depth 10000  --verbosity 10
+--max-nondet-string-length 100 --function Test.bufferDet --depth 10000  --verbosity 10
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

jbmc/regression/jbmc-strings/StringConcat/test_buffer_nondet_loop.desc

@@ -1,6 +1,6 @@
 CORE
 Test.class
---refine-strings --string-max-length 1000 --string-max-input-length 100 --function Test.bufferNonDetLoop --depth 10000 --unwind 5  --verbosity 10  --property 'java::Test.bufferNonDetLoop:(ILjava/lang/String;)Ljava/lang/String;.assertion.1'
+--max-nondet-string-length 100 --function Test.bufferNonDetLoop --depth 10000 --unwind 5  --verbosity 10  --property 'java::Test.bufferNonDetLoop:(ILjava/lang/String;)Ljava/lang/String;.assertion.1'
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

jbmc/regression/jbmc-strings/StringConcat/test_buffer_nondet_loop2.desc

@@ -1,6 +1,6 @@
 CORE
 Test.class
---refine-strings --string-max-length 1000 --string-max-input-length 100 --function Test.bufferNonDetLoop2 --depth 10000 --unwind 5  --verbosity 10
+--max-nondet-string-length 100 --function Test.bufferNonDetLoop2 --depth 10000 --unwind 5  --verbosity 10
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

jbmc/regression/jbmc-strings/StringConcat/test_buffer_nondet_loop3.desc

@@ -1,6 +1,6 @@
 CORE
 Test.class
---refine-strings --string-max-length 1000 --string-max-input-length 100 --function Test.bufferNonDetLoop3 --depth 10000 --unwind 5  --verbosity 10
+--max-nondet-string-length 100 --function Test.bufferNonDetLoop3 --depth 10000 --unwind 5  --verbosity 10
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

jbmc/regression/jbmc-strings/StringConcat/test_buffer_nondet_loop4.desc

@@ -1,6 +1,6 @@
 CORE
 Test.class
---refine-strings --string-max-length 1000 --string-max-input-length 100 --function Test.bufferNonDetLoop4 --depth 10000 --unwind 5  --verbosity 10 --property 'java::Test.bufferNonDetLoop4:(IILjava/lang/String;)Ljava/lang/String;.assertion.1'
+--max-nondet-string-length 100 --function Test.bufferNonDetLoop4 --depth 10000 --unwind 5  --verbosity 10 --property 'java::Test.bufferNonDetLoop4:(IILjava/lang/String;)Ljava/lang/String;.assertion.1'
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

jbmc/regression/jbmc-strings/StringConcat/test_buffer_nondet_loop5.desc

@@ -1,6 +1,6 @@
 CORE
 Test.class
---refine-strings --string-max-length 1000 --string-max-input-length 100 --function Test.bufferNonDetLoop5 --depth 10000 --unwind 3 --verbosity 10
+--max-nondet-string-length 100 --function Test.bufferNonDetLoop5 --depth 10000 --unwind 3 --verbosity 10
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

jbmc/regression/jbmc-strings/StringConcat/test_char_buffer_det.desc

@@ -1,6 +1,6 @@
 CORE
 Test.class
---refine-strings --string-max-length 1000 --string-max-input-length 100 --function Test.charBufferDet --depth 10000  --verbosity 10
+--max-nondet-string-length 100 --function Test.charBufferDet --depth 10000  --verbosity 10
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

jbmc/regression/jbmc-strings/StringConcat/test_char_buffer_det_loop.desc

@@ -1,6 +1,6 @@
 CORE
 Test.class
---refine-strings --string-max-length 1000 --string-max-input-length 100 --function Test.charBufferDetLoop --depth 10000 --unwind 5  --verbosity 10
+--max-nondet-string-length 100 --function Test.charBufferDetLoop --depth 10000 --unwind 5  --verbosity 10
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

jbmc/regression/jbmc-strings/StringConcat/test_char_buffer_det_loop2.desc

@@ -1,6 +1,6 @@
 CORE
 Test.class
---refine-strings --string-max-length 1000 --string-max-input-length 100 --function Test.charBufferDetLoop2 --depth 10000 --unwind 5  --verbosity 10
+--max-nondet-string-length 100 --function Test.charBufferDetLoop2 --depth 10000 --unwind 5  --verbosity 10
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$