Merge pull request #6919 from tautschnig/cleanup/simplify-if

Remove unused option "simplify-if"

Author: NlightNFotis

jbmc/regression/jbmc/output-options/test.desc

@@ -12,7 +12,6 @@ propagation: "1"
 refine-strings: "1"
 sat-preprocessor: "1"
 simplify: "1"
-simplify-if: "1"
 symex-driven-lazy-loading: "0"
 throw-assertion-error: "1"
 throw-runtime-exceptions: "0"

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -99,7 +99,6 @@ void jbmc_parse_optionst::set_default_options(optionst &options)
   options.set_option("refine-strings", true);
   options.set_option("simple-slice", true);
   options.set_option("simplify", true);
-  options.set_option("simplify-if", true);
   options.set_option("show-goto-symex-steps", false);
 
   // Other default
@@ -242,10 +241,6 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options)
     "slice-formula",
     cmdline.isset("slice-formula"));
 
-  // simplify if conditions and branches
-  if(cmdline.isset("no-simplify-if"))
-    options.set_option("simplify-if", false);
-
   if(cmdline.isset("arrays-uf-always"))
     options.set_option("arrays-uf", "always");
   else if(cmdline.isset("arrays-uf-never"))

src/cbmc/cbmc_parse_options.cpp

@@ -107,7 +107,6 @@ void cbmc_parse_optionst::set_default_options(optionst &options)
   options.set_option("propagation", true);
   options.set_option("simple-slice", true);
   options.set_option("simplify", true);
-  options.set_option("simplify-if", true);
   options.set_option("show-goto-symex-steps", false);
   options.set_option("show-points-to-sets", false);
   options.set_option("show-array-constraints", false);
@@ -284,10 +283,6 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
   if(cmdline.isset("slice-formula"))
     options.set_option("slice-formula", true);
 
-  // simplify if conditions and branches
-  if(cmdline.isset("no-simplify-if"))
-    options.set_option("simplify-if", false);
-
   if(cmdline.isset("arrays-uf-always"))
     options.set_option("arrays-uf", "always");
   else if(cmdline.isset("arrays-uf-never"))