Finish path exploration early if possible

If no command line options have been specified that require exhaustive
path exploration, finish path symex as soon as there are no properties
left to check.

Author: svorenova

src/cbmc/cbmc_parse_options.cpp

@@ -279,7 +279,10 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
 
   // generate unwinding assertions
   if(cmdline.isset("unwinding-assertions"))
+  {
     options.set_option("unwinding-assertions", true);
+    options.set_option("paths-symex-explore-all", true);
+  }
 
   if(cmdline.isset("partial-loops"))
     options.set_option("partial-loops", true);
@@ -416,9 +419,12 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
   }
 
   if(cmdline.isset("symex-coverage-report"))
+  {
     options.set_option(
       "symex-coverage-report",
       cmdline.get_value("symex-coverage-report"));
+    options.set_option("paths-symex-explore-all", true);
+  }
 
   if(cmdline.isset("validate-ssa-equation"))
   {

src/goto-checker/single_path_symex_checker.cpp

@@ -70,7 +70,9 @@ operator()(propertiest &properties)
       goto_symext::get_goto_function(goto_model), symex_symbol_table);
   }
 
-  while(!worklist->empty())
+  while(!worklist->empty() &&
+        (options.get_bool_option("paths-symex-explore-all") ||
+         has_properties_to_check(properties)))
   {
     path_storaget::patht &resume = worklist->peek();
     symex_bmct symex(

src/goto-checker/single_path_symex_only_checker.cpp

@@ -53,7 +53,9 @@ operator()(propertiest &properties)
       goto_symext::get_goto_function(goto_model), symex_symbol_table);
   }
 
-  while(!worklist->empty())
+  while(!worklist->empty() &&
+        (options.get_bool_option("paths-symex-explore-all") ||
+         has_properties_to_check(properties)))
   {
     path_storaget::patht &resume = worklist->peek();
     symex_bmct symex(