Merge pull request #6126 from thomasspriggs/tas/solver_factory_cleanup

Solver factory cleanup

Author: thomasspriggs

regression/cbmc-incr-oneloop/simpleloop1/incremental_support.desc

@@ -0,0 +1,14 @@
+CORE
+main.c
+--incremental-loop main.0 --unwinding-assertions --dimacs
+^Invalid User Input$
+^Option: --incremental-loop$
+^Reason: the chosen solver does not support incremental solving$
+^EXIT=1$
+^SIGNAL=0$
+--
+^warning: ignoring
+^Unwinding loop
+--
+Test that an appropriate error is shown when using --incremental-loop in
+combination with a solver which does not support incremental solving.

src/goto-checker/solver_factory.cpp

@@ -411,7 +411,7 @@ void solver_factoryt::no_incremental_check()
 {
   const bool all_properties = options.get_bool_option("all-properties");
   const bool cover = options.is_set("cover");
-  const bool incremental_check = options.is_set("incremental-check");
+  const bool incremental_loop = options.is_set("incremental-loop");
 
   if(all_properties)
   {
@@ -424,10 +424,10 @@ void solver_factoryt::no_incremental_check()
     throw invalid_command_line_argument_exceptiont(
       "the chosen solver does not support incremental solving", "--cover");
   }
-  else if(incremental_check)
+  else if(incremental_loop)
   {
     throw invalid_command_line_argument_exceptiont(
       "the chosen solver does not support incremental solving",
-      "--incremental-check");
+      "--incremental-loop");
   }
 }

src/goto-checker/solver_factory.h

@@ -23,7 +23,7 @@ class propt;
 class decision_proceduret;
 class stack_decision_proceduret;
 
-class solver_factoryt
+class solver_factoryt final
 {
 public:
   /// Note: The solver returned will hold a reference to the namespace `ns`.
@@ -35,7 +35,7 @@ class solver_factoryt
 
   // The solver class,
   // which owns a variety of allocated objects.
-  class solvert
+  class solvert final
   {
   public:
     solvert() = default;