diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp
index 60e1adc98a5..4509e641a53 100644
--- a/jbmc/src/jbmc/jbmc_parse_options.cpp
+++ b/jbmc/src/jbmc/jbmc_parse_options.cpp
@@ -105,7 +105,6 @@ void jbmc_parse_optionst::set_default_options(optionst &options)
   options.set_option("pretty-names", true);
   options.set_option("propagation", true);
   options.set_option("refine-strings", true);
-  options.set_option("sat-preprocessor", true);
   options.set_option("simple-slice", true);
   options.set_option("simplify", true);
   options.set_option("simplify-if", true);
@@ -274,28 +273,6 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options)
   else if(cmdline.isset("arrays-uf-never"))
     options.set_option("arrays-uf", "never");
 
-  if(cmdline.isset("dimacs"))
-    options.set_option("dimacs", true);
-
-  if(cmdline.isset("refine-arrays"))
-  {
-    options.set_option("refine", true);
-    options.set_option("refine-arrays", true);
-  }
-
-  if(cmdline.isset("refine-arithmetic"))
-  {
-    options.set_option("refine", true);
-    options.set_option("refine-arithmetic", true);
-  }
-
-  if(cmdline.isset("refine"))
-  {
-    options.set_option("refine", true);
-    options.set_option("refine-arrays", true);
-    options.set_option("refine-arithmetic", true);
-  }
-
   if(cmdline.isset("no-refine-strings"))
     options.set_option("refine-strings", false);
 
@@ -322,84 +299,10 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options)
       "--max-nondet-string-length");
   }
 
-  if(cmdline.isset("max-node-refinement"))
-    options.set_option(
-      "max-node-refinement",
-      cmdline.get_value("max-node-refinement"));
-
-  // SMT Options
-
-  if(cmdline.isset("smt1"))
-  {
-    log.error() << "--smt1 is no longer supported" << messaget::eom;
-    exit(CPROVER_EXIT_USAGE_ERROR);
-  }
-
-  if(cmdline.isset("smt2"))
-    options.set_option("smt2", true);
-
-  if(cmdline.isset("fpa"))
-    options.set_option("fpa", true);
-
-  bool solver_set=false;
-
-  if(cmdline.isset("boolector"))
-  {
-    options.set_option("boolector", true), solver_set=true;
-    options.set_option("smt2", true);
-  }
-
-  if(cmdline.isset("mathsat"))
-  {
-    options.set_option("mathsat", true), solver_set=true;
-    options.set_option("smt2", true);
-  }
-
-  if(cmdline.isset("cvc4"))
-  {
-    options.set_option("cvc4", true), solver_set=true;
-    options.set_option("smt2", true);
-  }
-
-  if(cmdline.isset("yices"))
-  {
-    options.set_option("yices", true), solver_set=true;
-    options.set_option("smt2", true);
-  }
-
-  if(cmdline.isset("z3"))
-  {
-    options.set_option("z3", true), solver_set=true;
-    options.set_option("smt2", true);
-  }
-
-  if(cmdline.isset("smt2") && !solver_set)
-  {
-    if(cmdline.isset("outfile"))
-    {
-      // outfile and no solver should give standard compliant SMT-LIB
-      options.set_option("generic", true);
-    }
-    else
-    {
-      // the default smt2 solver
-      options.set_option("z3", true);
-    }
-  }
-
-  if(cmdline.isset("beautify"))
-    options.set_option("beautify", true);
-
-  if(cmdline.isset("no-sat-preprocessor"))
-    options.set_option("sat-preprocessor", false);
-
   options.set_option(
     "pretty-names",
     !cmdline.isset("no-pretty-names"));
 
-  if(cmdline.isset("outfile"))
-    options.set_option("outfile", cmdline.get_value("outfile"));
-
   if(cmdline.isset("graphml-witness"))
   {
     options.set_option("graphml-witness", cmdline.get_value("graphml-witness"));
@@ -457,6 +360,14 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options)
 
   if(cmdline.isset("show-goto-symex-steps"))
     options.set_option("show-goto-symex-steps", true);
+
+  if(cmdline.isset("smt1"))
+  {
+    log.error() << "--smt1 is no longer supported" << messaget::eom;
+    exit(CPROVER_EXIT_USAGE_ERROR);
+  }
+
+  parse_solver_options(cmdline, options);
 }
 
 /// invoke main modules
@@ -1108,20 +1019,9 @@ void jbmc_parse_optionst::help()
     HELP_BMC
     "\n"
     "Backend options:\n"
-    " --object-bits n              number of bits used for object addresses\n"
-    " --dimacs                     generate CNF in DIMACS format\n"
-    " --beautify                   beautify the counterexample (greedy heuristic)\n" // NOLINT(*)
-    " --localize-faults            localize faults (experimental)\n"
-    " --smt1                       use default SMT1 solver (obsolete)\n"
-    " --smt2                       use default SMT2 solver (Z3)\n"
-    " --boolector                  use Boolector\n"
-    " --mathsat                    use MathSAT\n"
-    " --cvc4                       use CVC4\n"
-    " --yices                      use Yices\n"
-    " --z3                         use Z3\n"
-    " --refine                     use refinement procedure (experimental)\n"
+    HELP_CONFIG_BACKEND
+    HELP_SOLVER
     HELP_STRING_REFINEMENT
-    " --outfile filename           output formula to given file\n"
     " --arrays-uf-never            never turn arrays into uninterpreted functions\n" // NOLINT(*)
     " --arrays-uf-always           always turn arrays into uninterpreted functions\n" // NOLINT(*)
     "\n"
diff --git a/jbmc/src/jbmc/jbmc_parse_options.h b/jbmc/src/jbmc/jbmc_parse_options.h
index ea55144dcbc..0e381c409bf 100644
--- a/jbmc/src/jbmc/jbmc_parse_options.h
+++ b/jbmc/src/jbmc/jbmc_parse_options.h
@@ -46,7 +46,7 @@ class optionst;
   "(no-simplify)(full-slice)" \
   OPT_REACHABILITY_SLICER \
   "(debug-level):(no-propagation)(no-simplify-if)" \
-  "(document-subgoals)(outfile):" \
+  "(document-subgoals)" \
   "(object-bits):" \
   "(classpath):(cp):" \
   OPT_JAVA_JAR \
@@ -55,10 +55,8 @@ class optionst;
   "(no-assertions)(no-assumptions)" \
   OPT_XML_INTERFACE \
   OPT_JSON_INTERFACE \
-  "(smt1)(smt2)(fpa)(cvc3)(cvc4)(boolector)(yices)(z3)(mathsat)" \
-  "(no-sat-preprocessor)" \
-  "(beautify)" \
-  "(dimacs)(refine)(max-node-refinement):(refine-arrays)(refine-arithmetic)"\
+  "(smt1)" /* rejected, will eventually disappear */ \
+  OPT_SOLVER \
   OPT_STRING_REFINEMENT \
   "(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \
   OPT_SHOW_GOTO_FUNCTIONS \
diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
index ba9d672de8a..59c4cc0ba7b 100644
--- a/src/cbmc/cbmc_parse_options.cpp
+++ b/src/cbmc/cbmc_parse_options.cpp
@@ -106,7 +106,6 @@ void cbmc_parse_optionst::set_default_options(optionst &options)
   options.set_option("built-in-assertions", true);
   options.set_option("pretty-names", true);
   options.set_option("propagation", true);
-  options.set_option("sat-preprocessor", true);
   options.set_option("simple-slice", true);
   options.set_option("simplify", true);
   options.set_option("simplify-if", true);
@@ -306,42 +305,15 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
   else if(cmdline.isset("arrays-uf-never"))
     options.set_option("arrays-uf", "never");
 
-  if(cmdline.isset("dimacs"))
-    options.set_option("dimacs", true);
-
   if(cmdline.isset("show-array-constraints"))
     options.set_option("show-array-constraints", true);
 
-  if(cmdline.isset("refine-arrays"))
-  {
-    options.set_option("refine", true);
-    options.set_option("refine-arrays", true);
-  }
-
-  if(cmdline.isset("refine-arithmetic"))
-  {
-    options.set_option("refine", true);
-    options.set_option("refine-arithmetic", true);
-  }
-
-  if(cmdline.isset("refine"))
-  {
-    options.set_option("refine", true);
-    options.set_option("refine-arrays", true);
-    options.set_option("refine-arithmetic", true);
-  }
-
   if(cmdline.isset("refine-strings"))
   {
     options.set_option("refine-strings", true);
     options.set_option("string-printable", cmdline.isset("string-printable"));
   }
 
-  if(cmdline.isset("max-node-refinement"))
-    options.set_option(
-      "max-node-refinement",
-      cmdline.get_value("max-node-refinement"));
-
   options.set_option(
     "symex-cache-dereferences", cmdline.isset("symex-cache-dereferences"));
 
@@ -369,104 +341,9 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
     }
   }
 
-  // SMT Options
-
-  if(cmdline.isset("smt1"))
-  {
-    log.error() << "--smt1 is no longer supported" << messaget::eom;
-    exit(CPROVER_EXIT_USAGE_ERROR);
-  }
-
-  if(cmdline.isset("smt2"))
-    options.set_option("smt2", true);
-
-  if(cmdline.isset("fpa"))
-    options.set_option("fpa", true);
-
-  bool solver_set=false;
-
-  if(cmdline.isset("boolector"))
-  {
-    options.set_option("boolector", true), solver_set=true;
-    options.set_option("smt2", true);
-  }
-
-  if(cmdline.isset("cprover-smt2"))
-  {
-    options.set_option("cprover-smt2", true), solver_set = true;
-    options.set_option("smt2", true);
-  }
-
-  if(cmdline.isset("mathsat"))
-  {
-    options.set_option("mathsat", true), solver_set=true;
-    options.set_option("smt2", true);
-  }
-
-  if(cmdline.isset("cvc4"))
-  {
-    options.set_option("cvc4", true), solver_set=true;
-    options.set_option("smt2", true);
-  }
-
-  if(cmdline.isset("incremental-smt2-solver"))
-  {
-    options.set_option(
-      "incremental-smt2-solver", cmdline.get_value("incremental-smt2-solver")),
-      solver_set = true;
-  }
-
-  if(cmdline.isset("external-sat-solver"))
-  {
-    options.set_option(
-      "external-sat-solver", cmdline.get_value("external-sat-solver")),
-      solver_set = true;
-  }
-
-  if(cmdline.isset("yices"))
-  {
-    options.set_option("yices", true), solver_set=true;
-    options.set_option("smt2", true);
-  }
-
-  if(cmdline.isset("z3"))
-  {
-    options.set_option("z3", true), solver_set=true;
-    options.set_option("smt2", true);
-  }
-
-  if(cmdline.isset("smt2") && !solver_set)
-  {
-    if(cmdline.isset("outfile"))
-    {
-      // outfile and no solver should give standard compliant SMT-LIB
-      options.set_option("generic", true);
-    }
-    else
-    {
-      // the default smt2 solver
-      options.set_option("z3", true);
-    }
-  }
-
-  if(cmdline.isset("write-solver-stats-to"))
-  {
-    options.set_option(
-      "write-solver-stats-to", cmdline.get_value("write-solver-stats-to"));
-  }
-
-  if(cmdline.isset("beautify"))
-    options.set_option("beautify", true);
-
-  if(cmdline.isset("no-sat-preprocessor"))
-    options.set_option("sat-preprocessor", false);
-
   if(cmdline.isset("no-pretty-names"))
     options.set_option("pretty-names", false);
 
-  if(cmdline.isset("outfile"))
-    options.set_option("outfile", cmdline.get_value("outfile"));
-
   if(cmdline.isset("graphml-witness"))
   {
     options.set_option("graphml-witness", cmdline.get_value("graphml-witness"));
@@ -502,6 +379,14 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
 
   // Options for process_goto_program
   options.set_option("rewrite-union", true);
+
+  if(cmdline.isset("smt1"))
+  {
+    log.error() << "--smt1 is no longer supported" << messaget::eom;
+    exit(CPROVER_EXIT_USAGE_ERROR);
+  }
+
+  parse_solver_options(cmdline, options);
 }
 
 /// invoke main modules
@@ -999,6 +884,7 @@ void cbmc_parse_optionst::help()
     " --trace                      give a counterexample trace for failed properties\n" //NOLINT(*)
     " --stop-on-fail               stop analysis once a failed property is detected\n" // NOLINT(*)
     "                              (implies --trace)\n"
+    " --localize-faults            localize faults (experimental)\n"
     "\n"
     "C/C++ frontend options:\n"
     " --preprocess                 stop after preprocessing\n"
@@ -1036,23 +922,8 @@ void cbmc_parse_optionst::help()
     "\n"
     "Backend options:\n"
     HELP_CONFIG_BACKEND
-    " --dimacs                     generate CNF in DIMACS format\n"
-    " --beautify                   beautify the counterexample (greedy heuristic)\n" // NOLINT(*)
-    " --localize-faults            localize faults (experimental)\n"
-    " --smt2                       use default SMT2 solver (Z3)\n"
-    " --boolector                  use Boolector\n"
-    " --cprover-smt2               use CPROVER SMT2 solver\n"
-    " --cvc4                       use CVC4\n"
-    " --mathsat                    use MathSAT\n"
-    " --yices                      use Yices\n"
-    " --z3                         use Z3\n"
-    " --refine                     use refinement procedure (experimental)\n"
-    " --incremental-smt2-solver cmd\n"
-    "                              command to invoke external SMT solver for\n"
-    "                              incremental solving (experimental)\n"
-    " --external-sat-solver cmd    command to invoke SAT solver process\n"
+    HELP_SOLVER
     HELP_STRING_REFINEMENT_CBMC
-    " --outfile filename           output formula to given file\n"
     " --arrays-uf-never            never turn arrays into uninterpreted functions\n" // NOLINT(*)
     " --arrays-uf-always           always turn arrays into uninterpreted functions\n" // NOLINT(*)
     "\n"
@@ -1065,8 +936,6 @@ void cbmc_parse_optionst::help()
     HELP_FLUSH
     " --verbosity #                verbosity level\n"
     HELP_TIMESTAMP
-    " --write-solver-stats-to json-file\n"
-    "                              collect the solver query complexity\n"
     " --show-array-constraints     show array theory constraints added\n"
     "                              during post processing.\n"
     "                              Requires --json-ui.\n"
diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h
index d69c0c0ee65..3b4d0e3cbb7 100644
--- a/src/cbmc/cbmc_parse_options.h
+++ b/src/cbmc/cbmc_parse_options.h
@@ -45,8 +45,7 @@ class optionst;
   "(no-simplify)(full-slice)" \
   OPT_REACHABILITY_SLICER \
   "(debug-level):(no-propagation)(no-simplify-if)" \
-  "(document-subgoals)(outfile):(test-preprocessor)" \
-  "(write-solver-stats-to):"  \
+  "(document-subgoals)(test-preprocessor)" \
   "(show-array-constraints)"  \
   OPT_CONFIG_C_CPP \
   OPT_CONFIG_PLATFORM \
@@ -55,13 +54,7 @@ class optionst;
   OPT_GOTO_CHECK \
   OPT_XML_INTERFACE \
   OPT_JSON_INTERFACE \
-  "(smt1)(smt2)(fpa)(cvc3)(cvc4)(boolector)(yices)(z3)(mathsat)" \
-  "(cprover-smt2)" \
-  "(incremental-smt2-solver):" \
-  "(external-sat-solver):" \
-  "(no-sat-preprocessor)" \
-  "(beautify)" \
-  "(dimacs)(refine)(max-node-refinement):(refine-arrays)(refine-arithmetic)"\
+  OPT_SOLVER \
   OPT_STRING_REFINEMENT_CBMC \
   OPT_SHOW_GOTO_FUNCTIONS \
   OPT_SHOW_PROPERTIES \
diff --git a/src/goto-checker/solver_factory.cpp b/src/goto-checker/solver_factory.cpp
index df47f425c74..8bbcd97ffb2 100644
--- a/src/goto-checker/solver_factory.cpp
+++ b/src/goto-checker/solver_factory.cpp
@@ -11,14 +11,15 @@ Author: Daniel Kroening, Peter Schrammel
 
 #include "solver_factory.h"
 
-#include <iostream>
-
+#include <util/cmdline.h>
 #include <util/exception_utils.h>
 #include <util/make_unique.h>
 #include <util/message.h>
 #include <util/options.h>
 #include <util/version.h>
 
+#include <iostream>
+
 #ifdef _MSC_VER
 #include <util/unicode.h>
 #endif
@@ -450,3 +451,128 @@ void solver_factoryt::no_incremental_check()
       "--incremental-loop");
   }
 }
+
+static void parse_sat_options(const cmdlinet &cmdline, optionst &options)
+{
+  if(cmdline.isset("external-sat-solver"))
+  {
+    options.set_option(
+      "external-sat-solver", cmdline.get_value("external-sat-solver"));
+  }
+
+  options.set_option("sat-preprocessor", !cmdline.isset("no-sat-preprocessor"));
+
+  if(cmdline.isset("dimacs"))
+    options.set_option("dimacs", true);
+}
+
+static void parse_smt2_options(const cmdlinet &cmdline, optionst &options)
+{
+  if(cmdline.isset("smt2"))
+    options.set_option("smt2", true);
+
+  if(cmdline.isset("fpa"))
+    options.set_option("fpa", true);
+
+  bool solver_set = false;
+
+  if(cmdline.isset("boolector"))
+  {
+    options.set_option("boolector", true), solver_set = true;
+    options.set_option("smt2", true);
+  }
+
+  if(cmdline.isset("cprover-smt2"))
+  {
+    options.set_option("cprover-smt2", true), solver_set = true;
+    options.set_option("smt2", true);
+  }
+
+  if(cmdline.isset("mathsat"))
+  {
+    options.set_option("mathsat", true), solver_set = true;
+    options.set_option("smt2", true);
+  }
+
+  if(cmdline.isset("cvc4"))
+  {
+    options.set_option("cvc4", true), solver_set = true;
+    options.set_option("smt2", true);
+  }
+
+  if(cmdline.isset("incremental-smt2-solver"))
+  {
+    options.set_option(
+      "incremental-smt2-solver", cmdline.get_value("incremental-smt2-solver")),
+      solver_set = true;
+  }
+
+  if(cmdline.isset("yices"))
+  {
+    options.set_option("yices", true), solver_set = true;
+    options.set_option("smt2", true);
+  }
+
+  if(cmdline.isset("z3"))
+  {
+    options.set_option("z3", true), solver_set = true;
+    options.set_option("smt2", true);
+  }
+
+  if(cmdline.isset("smt2") && !solver_set)
+  {
+    if(cmdline.isset("outfile"))
+    {
+      // outfile and no solver should give standard compliant SMT-LIB
+      options.set_option("generic", true);
+    }
+    else
+    {
+      // the default smt2 solver
+      options.set_option("z3", true);
+    }
+  }
+}
+
+void parse_solver_options(const cmdlinet &cmdline, optionst &options)
+{
+  parse_sat_options(cmdline, options);
+  parse_smt2_options(cmdline, options);
+
+  if(cmdline.isset("outfile"))
+    options.set_option("outfile", cmdline.get_value("outfile"));
+
+  if(cmdline.isset("write-solver-stats-to"))
+  {
+    options.set_option(
+      "write-solver-stats-to", cmdline.get_value("write-solver-stats-to"));
+  }
+
+  if(cmdline.isset("beautify"))
+    options.set_option("beautify", true);
+
+  if(cmdline.isset("refine-arrays"))
+  {
+    options.set_option("refine", true);
+    options.set_option("refine-arrays", true);
+  }
+
+  if(cmdline.isset("refine-arithmetic"))
+  {
+    options.set_option("refine", true);
+    options.set_option("refine-arithmetic", true);
+  }
+
+  if(cmdline.isset("refine"))
+  {
+    options.set_option("refine", true);
+    options.set_option("refine-arrays", true);
+    options.set_option("refine-arithmetic", true);
+  }
+
+  if(cmdline.isset("max-node-refinement"))
+  {
+    options.set_option(
+      "max-node-refinement", cmdline.get_value("max-node-refinement"));
+  }
+}
diff --git a/src/goto-checker/solver_factory.h b/src/goto-checker/solver_factory.h
index 348ef242c06..48180d5d369 100644
--- a/src/goto-checker/solver_factory.h
+++ b/src/goto-checker/solver_factory.h
@@ -16,6 +16,7 @@ Author: Daniel Kroening, Peter Schrammel
 
 #include <solvers/smt2/smt2_dec.h>
 
+class cmdlinet;
 class message_handlert;
 class namespacet;
 class optionst;
@@ -91,4 +92,50 @@ class solver_factoryt final
   void no_incremental_check();
 };
 
+/// Parse solver-related command-line parameters in \p cmdline and set
+/// corresponding values in \p options.
+void parse_solver_options(const cmdlinet &cmdline, optionst &options);
+
+#define OPT_SOLVER                                                             \
+  "(smt1)" /* rejected, will eventually disappear */                           \
+  "(smt2)"                                                                     \
+  "(fpa)" /* undocumented */                                                   \
+  "(cvc3)"                                                                     \
+  "(cvc4)(boolector)(yices)(z3)"                                               \
+  "(mathsat)"                                                                  \
+  "(cprover-smt2)"                                                             \
+  "(incremental-smt2-solver):"                                                 \
+  "(external-sat-solver):"                                                     \
+  "(no-sat-preprocessor)" /* undocumented */                                   \
+  "(beautify)"                                                                 \
+  "(dimacs)"                                                                   \
+  "(refine)"                                                                   \
+  "(max-node-refinement):" /* undocumented */                                  \
+  "(refine-arrays)"        /* undocumented */                                  \
+  "(refine-arithmetic)"    /* undocumented */                                  \
+  "(outfile):"                                                                 \
+  "(write-solver-stats-to):"
+
+#define HELP_SOLVER                                                            \
+  " --external-sat-solver cmd    command to invoke SAT solver process\n"       \
+  " --dimacs                     generate CNF in DIMACS format\n"              \
+  " --beautify                   beautify the counterexample\n"                \
+  "                              (greedy heuristic)\n"                         \
+  " --smt1                       use default SMT1 solver (obsolete)\n"         \
+  " --smt2                       use default SMT2 solver (Z3)\n"               \
+  " --boolector                  use Boolector\n"                              \
+  " --cprover-smt2               use CPROVER SMT2 solver\n"                    \
+  " --cvc3                       use CVC3\n"                                   \
+  " --cvc4                       use CVC4\n"                                   \
+  " --mathsat                    use MathSAT\n"                                \
+  " --yices                      use Yices\n"                                  \
+  " --z3                         use Z3\n"                                     \
+  " --refine                     use refinement procedure (experimental)\n"    \
+  " --incremental-smt2-solver cmd\n"                                           \
+  "                              command to invoke external SMT solver for\n"  \
+  "                              incremental solving (experimental)\n"         \
+  " --outfile filename           output formula to given file\n"               \
+  " --write-solver-stats-to json-file\n"                                       \
+  "                              collect the solver query complexity\n"
+
 #endif // CPROVER_GOTO_CHECKER_SOLVER_FACTORY_H