Add a test for unknown solver

Author: zhassan-aws

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

@@ -0,0 +1,9 @@
+#include <assert.h>
+
+int main()
+{
+  unsigned x;
+  unsigned y = 0;
+  assert(x * y == y);
+  return 0;
+}

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

@@ -0,0 +1,7 @@
+CORE broken-z3-smt-backend broken-cprover-smt-backend 
+test.c
+--sat-solver non-existing-solver
+^EXIT=1$
+^SIGNAL=0$
+unknown solver 'non-existing-solver'
+--

src/goto-checker/solver_factory.cpp

@@ -13,6 +13,7 @@ Author: Daniel Kroening, Peter Schrammel
 
 #include <util/cmdline.h>
 #include <util/exception_utils.h>
+#include <util/exit_codes.h>
 #include <util/make_unique.h>
 #include <util/message.h>
 #include <util/options.h>
@@ -330,6 +331,7 @@ std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_sat_solver()
   {
     messaget log(message_handler);
     log.error() << "unknown solver '" << solver_option << "'" << messaget::eom;
+    exit(CPROVER_EXIT_USAGE_ERROR);
   }
   if(!solver_set)
   {