Change option name to --refine-strings

Author: Joel Allred

src/cbmc/cbmc_parse_options.cpp

@@ -289,9 +289,9 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
     options.set_option("refine-arithmetic", true);
   }
 
-  if(cmdline.isset("string-refine"))
+  if(cmdline.isset("refine-strings"))
   {
-    options.set_option("string-refine", true);
+    options.set_option("refine-strings", true);
   }
 
   if(cmdline.isset("max-node-refinement"))
@@ -818,7 +818,7 @@ bool cbmc_parse_optionst::process_goto_program(
     goto_partial_inline(goto_functions, ns, ui_message_handler);
 
 
-    if(cmdline.isset("string-refine"))
+    if(cmdline.isset("refine-strings"))
     {
       status() << "Preprocessing for string refinement" << eom;
       string_refine_preprocesst(
@@ -1084,7 +1084,7 @@ void cbmc_parse_optionst::help()
     " --yices                      use Yices\n"
     " --z3                         use Z3\n"
     " --refine                     use refinement procedure (experimental)\n"
-    " --string-refine              use string refinement (experimental)\n"
+    " --refine-strings             use string refinement (experimental)\n"
     " --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(*)

src/cbmc/cbmc_parse_options.h

@@ -41,7 +41,7 @@ class optionst;
   "(no-sat-preprocessor)" \
   "(no-pretty-names)(beautify)" \
   "(dimacs)(refine)(max-node-refinement):(refine-arrays)(refine-arithmetic)"\
-  "(string-refine)" \
+  "(refine-strings)" \
   "(aig)(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \
   "(little-endian)(big-endian)" \
   "(show-goto-functions)(show-loops)" \

src/cbmc/cbmc_solvers.h

@@ -111,7 +111,7 @@ class cbmc_solverst:public messaget
       solver=get_dimacs();
     else if(options.get_bool_option("refine"))
       solver=get_bv_refinement();
-    else if(options.get_bool_option("string-refine"))
+    else if(options.get_bool_option("refine-strings"))
       solver=get_string_refinement();
     else if(options.get_bool_option("smt1"))
       solver=get_smt1(get_smt1_solver_type());

src/java_bytecode/java_bytecode_language.cpp

@@ -35,7 +35,7 @@ Author: Daniel Kroening, [email protected]
 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("string-refine");
+  string_refinement_enabled=cmd.isset("refine-strings");
   if(cmd.isset("java-max-input-array-length"))
     max_nondet_array_length=
       std::stoi(cmd.get_value("java-max-input-array-length"));