Merge pull request #4377 from svorenova/path-symex-while-has-properties-to-check

Single path symex only while there are properties to check

Author: tautschnig

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(