Set paths-symex-explore-all when unwinding-assertions defaults to true

regression/cbmc/Array_operations4/program-only.desc

@@ -1,4 +1,4 @@
-CORE paths-lifo-expected-failure
+CORE
 main.c
 --program-only
 target!0@1#2 ==

regression/cbmc/array-cell-sensitivity15/test.desc

@@ -1,4 +1,4 @@
-CORE paths-lifo-expected-failure
+CORE
 access.c
 --program-only
 ^EXIT=0$

regression/cbmc/cover-failed-assertions/test-no-failed-assertions.desc

@@ -13,3 +13,4 @@ test.c
 --
 This is checking that without the --cover-failed-assertions flag we still get the same result as we did before adding
 it in this example.
+--paths mode explores one path at a time, so individual paths may not cover all blocks.

regression/cbmc/cover-failed-assertions/test.desc

@@ -11,3 +11,4 @@ test.c
 ^warning: ignoring
 --
 This is checking that the if statement body can actually be covered with the new flag
+--paths mode explores one path at a time, so individual paths may not cover all blocks.

regression/cbmc/fault_localization-stop_on_fail1/test.desc

@@ -7,3 +7,6 @@ main.c
 line . function main$
 ^VERIFICATION FAILED$
 --
+--
+--paths mode explores paths in a different order, finding a different failing
+assertion first, which changes the fault localization output.

regression/cbmc/outfile_no_dir/test.desc

@@ -1,4 +1,4 @@
-CORE paths-lifo-expected-failure
+CORE
 main.c
 --dimacs --outfile /xyz/out.dimacs
 ^EXIT=1$

regression/cbmc/sat-solver-error/test.desc

@@ -1,4 +1,4 @@
-CORE broken-z3-smt-backend broken-cprover-smt-backend paths-lifo-expected-failure no-new-smt
+CORE broken-z3-smt-backend broken-cprover-smt-backend no-new-smt
 test.c
 --sat-solver non-existing-solver
 ^EXIT=1$

regression/cbmc/unreachable-goto2/test-vccs.desc

@@ -1,4 +1,4 @@
-CORE paths-lifo-expected-failure
+CORE
 test.c
 --show-vcc --verbosity 8
 ^Generated 1 VCC\(s\), 1 remaining after simplification$

src/cbmc/cbmc_parse_options.cpp

@@ -15,6 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/exit_codes.h>
 #include <util/help_formatter.h>
 #include <util/invariant.h>
+#include <util/output_file.h>
 #include <util/unicode.h>
 #include <util/version.h>
 
@@ -125,6 +126,7 @@ void cbmc_parse_optionst::set_default_analysis_flags(
   if(!options.is_set("unwinding-assertions"))
   {
     options.set_option("unwinding-assertions", enabled);
+    options.set_option("paths-symex-explore-all", enabled);
   }
 
   if(enabled)
@@ -670,6 +672,23 @@ int cbmc_parse_optionst::doit()
   if(
     options.get_bool_option("dimacs") || !options.get_option("outfile").empty())
   {
+    // Validate outfile path early so that errors are reported even when
+    // single-path symex simplifies away all VCCs (and thus never creates
+    // the solver).
+    const std::string outfile = options.get_option("outfile");
+    if(!outfile.empty() && outfile != "-")
+    {
+      try
+      {
+        output_filet{outfile};
+      }
+      catch(const system_exceptiont &)
+      {
+        throw invalid_command_line_argument_exceptiont(
+          "failed to open file: " + outfile, "--outfile");
+      }
+    }
+
     if(options.get_bool_option("paths"))
     {
       stop_on_fail_verifiert<single_path_symex_checkert> verifier(

src/goto-checker/solver_factory.cpp

@@ -164,6 +164,18 @@ smt2_dect::solvert solver_factoryt::get_smt2_solver_type() const
   return s;
 }
 
+/// Check whether \p solver_name is a known SAT solver name. A solver may be
+/// known but not compiled in (in which case \ref get_sat_solver will fall back
+/// to the default solver with a warning).
+static bool is_known_sat_solver_name(const std::string &solver_name)
+{
+  return solver_name == "zchaff" || solver_name == "booleforce" ||
+         solver_name == "minisat1" || solver_name == "minisat2" ||
+         solver_name == "ipasir" || solver_name == "picosat" ||
+         solver_name == "lingeling" || solver_name == "glucose" ||
+         solver_name == "cadical";
+}
+
 /// Emit a warning for non-existent solver \p solver via \p message_handler.
 static void emit_solver_warning(
   message_handlert &message_handler,
@@ -314,6 +326,9 @@ get_sat_solver(message_handlert &message_handler, const optionst &options)
     }
     else
     {
+      INVARIANT(
+        !is_known_sat_solver_name(solver_option),
+        "known solver names should be handled above");
       messaget log(message_handler);
       log.error() << "unknown solver '" << solver_option << "'"
                   << messaget::eom;
@@ -625,7 +640,16 @@ static void parse_sat_options(const cmdlinet &cmdline, optionst &options)
     options.set_option("dimacs", true);
 
   if(cmdline.isset("sat-solver"))
-    options.set_option("sat-solver", cmdline.get_value("sat-solver"));
+  {
+    const std::string solver = cmdline.get_value("sat-solver");
+    options.set_option("sat-solver", solver);
+
+    if(!is_known_sat_solver_name(solver))
+    {
+      throw invalid_command_line_argument_exceptiont(
+        "unknown solver '" + solver + "'", "--sat-solver");
+    }
+  }
 }
 
 static void parse_smt2_options(const cmdlinet &cmdline, optionst &options)