Remove the string-non-empty option

This had no effect on the solver, so should not be used.

Author: romainbrenguier

src/cbmc/cbmc_parse_options.cpp

@@ -271,7 +271,6 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
   if(cmdline.isset("refine-strings"))
   {
     options.set_option("refine-strings", true);
-    options.set_option("string-non-empty", cmdline.isset("string-non-empty"));
     options.set_option("string-printable", cmdline.isset("string-printable"));
     if(cmdline.isset("string-max-length"))
       options.set_option(
@@ -1009,7 +1008,6 @@ void cbmc_parse_optionst::help()
     " --z3                         use Z3\n"
     " --refine                     use refinement procedure (experimental)\n"
     " --refine-strings             use string refinement (experimental)\n"
-    " --string-non-empty           add constraint that strings are non empty (experimental)\n" // NOLINT(*)
     " --string-printable           add constraint that strings are printable (experimental)\n" // NOLINT(*)
     " --string-max-length          add constraint on the length of strings\n" // NOLINT(*)
     " --string-max-input-length    add constraint on the length of input strings\n" // NOLINT(*)

src/cbmc/cbmc_parse_options.h

@@ -44,7 +44,6 @@ class optionst;
   "(no-pretty-names)(beautify)" \
   "(dimacs)(refine)(max-node-refinement):(refine-arrays)(refine-arithmetic)"\
   "(refine-strings)" \
-  "(string-non-empty)" \
   "(string-printable)" \
   "(string-max-length):" \
   "(string-max-input-length):" \

src/jbmc/jbmc_parse_options.cpp

@@ -246,7 +246,6 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options)
   if(cmdline.isset("refine-strings"))
   {
     options.set_option("refine-strings", true);
-    options.set_option("string-non-empty", cmdline.isset("string-non-empty"));
     options.set_option("string-printable", cmdline.isset("string-printable"));
     if(cmdline.isset("string-max-length"))
       options.set_option(
@@ -910,7 +909,6 @@ void jbmc_parse_optionst::help()
     " --z3                         use Z3\n"
     " --refine                     use refinement procedure (experimental)\n"
     " --refine-strings             use string refinement (experimental)\n"
-    " --string-non-empty           add constraint that strings are non empty (experimental)\n" // NOLINT(*)
     " --string-printable           add constraint that strings are printable (experimental)\n" // NOLINT(*)
     " --string-max-length          add constraint on the length of strings\n" // NOLINT(*)
     " --string-max-input-length    add constraint on the length of input strings\n" // NOLINT(*)

src/jbmc/jbmc_parse_options.h

@@ -44,7 +44,6 @@ class optionst;
   "(no-pretty-names)(beautify)" \
   "(dimacs)(refine)(max-node-refinement):(refine-arrays)(refine-arithmetic)"\
   "(refine-strings)" \
-  "(string-non-empty)" \
   "(string-printable)" \
   "(string-max-length):" \
   "(string-max-input-length):" \