Remove --refine-strings from tests

Author: peterschrammel

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

@@ -1,6 +1,6 @@
 CORE
 test.class
---refine-strings --max-nondet-string-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 --max-nondet-string-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 --max-nondet-string-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 --max-nondet-string-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 --max-nondet-string-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 --max-nondet-string-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 --max-nondet-string-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 --max-nondet-string-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 --max-nondet-string-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