diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp
index 8ea70017c47..b360286b7d0 100644
--- a/jbmc/src/jbmc/jbmc_parse_options.cpp
+++ b/jbmc/src/jbmc/jbmc_parse_options.cpp
@@ -53,6 +53,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <langapi/mode.h>
 
+#include <cbmc/bmc.h> // will go away
+
 #include <java_bytecode/convert_java_nondet.h>
 #include <java_bytecode/java_bytecode_language.h>
 #include <java_bytecode/java_enum_static_init_unwind_handler.h>
diff --git a/jbmc/src/jbmc/jbmc_parse_options.h b/jbmc/src/jbmc/jbmc_parse_options.h
index d5989a7a5fc..b8361afde61 100644
--- a/jbmc/src/jbmc/jbmc_parse_options.h
+++ b/jbmc/src/jbmc/jbmc_parse_options.h
@@ -20,7 +20,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <analyses/goto_check.h>
 
-#include <cbmc/bmc.h>
+#include <goto-checker/bmc_util.h>
 
 #include <goto-programs/class_hierarchy.h>
 #include <goto-programs/goto_trace.h>
@@ -33,7 +33,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <java_bytecode/java_bytecode_language.h>
 
-class bmct;
 class goto_functionst;
 class optionst;
 
diff --git a/src/cbmc/bmc.h b/src/cbmc/bmc.h
index 063d2fc6078..0fbfa2f0da3 100644
--- a/src/cbmc/bmc.h
+++ b/src/cbmc/bmc.h
@@ -264,42 +264,4 @@ class path_explorert : public bmct
     goto_symext::get_goto_functiont get_goto_function) override;
 };
 
-#define OPT_BMC                                                                \
-  "(program-only)"                                                             \
-  "(show-loops)"                                                               \
-  "(show-vcc)"                                                                 \
-  "(slice-formula)"                                                            \
-  "(unwinding-assertions)"                                                     \
-  "(no-unwinding-assertions)"                                                  \
-  "(no-pretty-names)"                                                          \
-  "(no-self-loops-to-assumptions)"                                             \
-  "(partial-loops)"                                                            \
-  "(paths):"                                                                   \
-  "(show-symex-strategies)"                                                    \
-  "(depth):"                                                                   \
-  "(unwind):"                                                                  \
-  "(unwindset):"                                                               \
-  "(graphml-witness):"                                                         \
-  "(unwindset):"
-
-#define HELP_BMC                                                               \
-  " --paths [strategy]           explore paths one at a time\n"                \
-  " --show-symex-strategies      list strategies for use with --paths\n"       \
-  " --program-only               only show program expression\n"               \
-  " --show-loops                 show the loops in the program\n"              \
-  " --depth nr                   limit search depth\n"                         \
-  " --unwind nr                  unwind nr times\n"                            \
-  " --unwindset L:B,...          unwind loop L with a bound of B\n"            \
-  "                              (use --show-loops to get the loop IDs)\n"     \
-  " --show-vcc                   show the verification conditions\n"           \
-  " --slice-formula              remove assignments unrelated to property\n"   \
-  " --unwinding-assertions       generate unwinding assertions (cannot be\n"   \
-  "                              used with --cover or --partial-loops)\n"      \
-  " --partial-loops              permit paths with partial loops\n"            \
-  " --no-self-loops-to-assumptions\n"                                          \
-  "                              do not simplify while(1){} to assume(0)\n"    \
-  " --no-pretty-names            do not simplify identifiers\n"                \
-  " --graphml-witness filename   write the witness in GraphML format to "      \
-  "filename\n" // NOLINT(*)
-
 #endif // CPROVER_CBMC_BMC_H
diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
index 8663179c435..31405e7c620 100644
--- a/src/cbmc/cbmc_parse_options.cpp
+++ b/src/cbmc/cbmc_parse_options.cpp
@@ -30,6 +30,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <cpp/cprover_library.h>
 
+#include <goto-checker/bmc_util.h>
+
 #include <goto-programs/adjust_float_expressions.h>
 #include <goto-programs/initialize_goto_model.h>
 #include <goto-programs/instrument_preconditions.h>
diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h
index 4e63f1837b4..e3aac2e4ed0 100644
--- a/src/cbmc/cbmc_parse_options.h
+++ b/src/cbmc/cbmc_parse_options.h
@@ -24,6 +24,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <analyses/goto_check.h>
 
+#include <goto-checker/bmc_util.h>
 #include <goto-checker/solver_factory.h>
 
 #include <goto-programs/goto_trace.h>
@@ -33,7 +34,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "bmc.h"
 #include "xml_interface.h"
 
-class bmct;
 class goto_functionst;
 class optionst;
 
diff --git a/src/goto-checker/bmc_util.h b/src/goto-checker/bmc_util.h
index 1aa7e74506b..7cb2c64a676 100644
--- a/src/goto-checker/bmc_util.h
+++ b/src/goto-checker/bmc_util.h
@@ -71,4 +71,43 @@ void slice(
   const optionst &,
   ui_message_handlert &);
 
+// clang-format off
+#define OPT_BMC \
+  "(program-only)" \
+  "(show-loops)" \
+  "(show-vcc)" \
+  "(slice-formula)" \
+  "(unwinding-assertions)" \
+  "(no-unwinding-assertions)" \
+  "(no-pretty-names)" \
+  "(no-self-loops-to-assumptions)" \
+  "(partial-loops)" \
+  "(paths):" \
+  "(show-symex-strategies)" \
+  "(depth):" \
+  "(unwind):" \
+  "(unwindset):" \
+  "(graphml-witness):" \
+  "(unwindset):"
+
+#define HELP_BMC \
+  " --paths [strategy]           explore paths one at a time\n" \
+  " --show-symex-strategies      list strategies for use with --paths\n" \
+  " --program-only               only show program expression\n" \
+  " --show-loops                 show the loops in the program\n" \
+  " --depth nr                   limit search depth\n" \
+  " --unwind nr                  unwind nr times\n" \
+  " --unwindset L:B,...          unwind loop L with a bound of B\n" \
+  "                              (use --show-loops to get the loop IDs)\n" \
+  " --show-vcc                   show the verification conditions\n" \
+  " --slice-formula              remove assignments unrelated to property\n" \
+  " --unwinding-assertions       generate unwinding assertions (cannot be\n" \
+  "                              used with --cover or --partial-loops)\n" \
+  " --partial-loops              permit paths with partial loops\n" \
+  " --no-self-loops-to-assumptions\n" \
+  "                              do not simplify while(1){} to assume(0)\n" \
+  " --no-pretty-names            do not simplify identifiers\n" \
+  " --graphml-witness filename   write the witness in GraphML format to filename\n" // NOLINT(*)
+// clang-format on
+
 #endif // CPROVER_GOTO_CHECKER_BMC_UTIL_H