Remove --refine-strings from JBMC

Author: peterschrammel

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

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$

jbmc/src/jbmc/jbmc_parse_options.h

@@ -52,7 +52,6 @@ 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 */ \