Fix handling of sat-solver option

Author: zhassan-aws

src/goto-checker/solver_factory.cpp

@@ -213,125 +213,128 @@ make_satcheck_prop(message_handlert &message_handler, const optionst &options)
 std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_sat_solver()
 {
   auto solver = util_make_unique<solvert>();
-  const std::string &solver_option = options.get_option("sat-solver");
   bool solver_set = false;
-  if(solver_option == "zchaff")
+  if(options.is_set("sat-solver"))
   {
+    const std::string &solver_option = options.get_option("sat-solver");
+    if(solver_option == "zchaff")
+    {
 #if defined SATCHECK_ZCHAFF
-    solver->set_prop(
-      make_satcheck_prop<satcheck_zchafft>(message_handler, options));
-    solver_set = true;
+      solver->set_prop(
+        make_satcheck_prop<satcheck_zchafft>(message_handler, options));
+      solver_set = true;
 #else
-    emit_solver_warning("zchaff");
+      emit_solver_warning("zchaff");
 #endif
-  }
-  else if(solver_option == "booleforce")
-  {
+    }
+    else if(solver_option == "booleforce")
+    {
 #if defined SATCHECK_BOOLERFORCE
-    solver->set_prop(
-      make_satcheck_prop<satcheck_booleforcet>(message_handler, options));
-    solver_set = true;
+      solver->set_prop(
+        make_satcheck_prop<satcheck_booleforcet>(message_handler, options));
+      solver_set = true;
 #else
-    emit_solver_warning("booleforce");
+      emit_solver_warning("booleforce");
 #endif
-  }
-  else if(solver_option == "minisat1")
-  {
+    }
+    else if(solver_option == "minisat1")
+    {
 #if defined SATCHECK_MINISAT1
-    solver->set_prop(
-      make_satcheck_prop<satcheck_minisat1t>(message_handler, options));
-    solver_set = true;
+      solver->set_prop(
+        make_satcheck_prop<satcheck_minisat1t>(message_handler, options));
+      solver_set = true;
 #else
-    emit_solver_warning("minisat1");
+      emit_solver_warning("minisat1");
 #endif
-  }
-  else if(solver_option == "minisat2")
-  {
-#if defined SATCHECK_MINISAT2
-    if(
-      options.get_bool_option("beautify") ||
-      !options.get_bool_option("sat-preprocessor")) // no simplifier
-    {
-      // simplifier won't work with beautification
-      solver->set_prop(make_satcheck_prop<satcheck_minisat_no_simplifiert>(
-        message_handler, options));
     }
-    else // with simplifier
+    else if(solver_option == "minisat2")
     {
-      solver->set_prop(make_satcheck_prop<satcheck_minisat_simplifiert>(
-        message_handler, options));
-    }
-    solver_set = true;
+#if defined SATCHECK_MINISAT2
+      if(
+        options.get_bool_option("beautify") ||
+        !options.get_bool_option("sat-preprocessor")) // no simplifier
+      {
+        // simplifier won't work with beautification
+        solver->set_prop(make_satcheck_prop<satcheck_minisat_no_simplifiert>(
+          message_handler, options));
+      }
+      else // with simplifier
+      {
+        solver->set_prop(make_satcheck_prop<satcheck_minisat_simplifiert>(
+          message_handler, options));
+      }
+      solver_set = true;
 #else
-    emit_solver_warning("minisat2");
+      emit_solver_warning("minisat2");
 #endif
-  }
-  else if(solver_option == "ipasir")
-  {
+    }
+    else if(solver_option == "ipasir")
+    {
 #if defined SATCHECK_IPASIR
-    solver->set_prop(
-      make_satcheck_prop<satcheck_ipasirt>(message_handler, options));
-    solver_set = true;
+      solver->set_prop(
+        make_satcheck_prop<satcheck_ipasirt>(message_handler, options));
+      solver_set = true;
 #else
-    emit_solver_warning("ipasir");
+      emit_solver_warning("ipasir");
 #endif
-  }
-  else if(solver_option == "picosat")
-  {
+    }
+    else if(solver_option == "picosat")
+    {
 #if defined SATCHECK_PICOSAT
-    solver->set_prop(
-      make_satcheck_prop<satcheck_picosatt>(message_handler, options));
-    solver_set = true;
+      solver->set_prop(
+        make_satcheck_prop<satcheck_picosatt>(message_handler, options));
+      solver_set = true;
 #else
-    emit_solver_warning("picosat");
+      emit_solver_warning("picosat");
 #endif
-  }
-  else if(solver_option == "lingeling")
-  {
+    }
+    else if(solver_option == "lingeling")
+    {
 #if defined SATCHECK_LINGELING
-    solver->set_prop(
-      make_satcheck_prop<satcheck_lingelingt>(message_handler, options));
-    solver_set = true;
+      solver->set_prop(
+        make_satcheck_prop<satcheck_lingelingt>(message_handler, options));
+      solver_set = true;
 #else
-    emit_solver_warning("lingeling");
+      emit_solver_warning("lingeling");
 #endif
-  }
-  else if(solver_option == "glucose")
-  {
-#if defined SATCHECK_GLUCOSE
-    if(
-      options.get_bool_option("beautify") ||
-      !options.get_bool_option("sat-preprocessor")) // no simplifier
-    {
-      // simplifier won't work with beautification
-      solver->set_prop(make_satcheck_prop<satcheck_glucose_no_simplifiert>(
-        message_handler, options));
     }
-    else // with simplifier
+    else if(solver_option == "glucose")
     {
-      solver->set_prop(make_satcheck_prop<satcheck_glucose_simplifiert>(
-        message_handler, options));
-    }
-    solver_set = true;
+#if defined SATCHECK_GLUCOSE
+      if(
+        options.get_bool_option("beautify") ||
+        !options.get_bool_option("sat-preprocessor")) // no simplifier
+      {
+        // simplifier won't work with beautification
+        solver->set_prop(make_satcheck_prop<satcheck_glucose_no_simplifiert>(
+          message_handler, options));
+      }
+      else // with simplifier
+      {
+        solver->set_prop(make_satcheck_prop<satcheck_glucose_simplifiert>(
+          message_handler, options));
+      }
+      solver_set = true;
 #else
-    emit_solver_warning("glucose");
+      emit_solver_warning("glucose");
 #endif
-  }
-  else if(solver_option == "cadical")
-  {
+    }
+    else if(solver_option == "cadical")
+    {
 #if defined SATCHECK_CADICAL
-    solver->set_prop(
-      make_satcheck_prop<satcheck_cadicalt>(message_handler, options));
-    solver_set = true;
+      solver->set_prop(
+        make_satcheck_prop<satcheck_cadicalt>(message_handler, options));
+      solver_set = true;
 #else
-    emit_solver_warning("cadical");
+      emit_solver_warning("cadical");
 #endif
-  }
-  else
-  {
-    messaget log(message_handler);
-    log.error() << "unknown solver '" << solver_option << "'" << messaget::eom;
-    exit(CPROVER_EXIT_USAGE_ERROR);
+    }
+    else
+    {
+      messaget log(message_handler);
+      log.error() << "unknown solver '" << solver_option << "'" << messaget::eom;
+      exit(CPROVER_EXIT_USAGE_ERROR);
+    }
   }
   if(!solver_set)
   {