diff --git a/jbmc/regression/jbmc/output-options/Main.class b/jbmc/regression/jbmc/output-options/Main.class
new file mode 100644
index 00000000000..bd67b76274f
Binary files /dev/null and b/jbmc/regression/jbmc/output-options/Main.class differ
diff --git a/jbmc/regression/jbmc/output-options/Main.java b/jbmc/regression/jbmc/output-options/Main.java
new file mode 100644
index 00000000000..20c6646fb75
--- /dev/null
+++ b/jbmc/regression/jbmc/output-options/Main.java
@@ -0,0 +1,6 @@
+public class Main {
+  public static void main(String[] args) {
+    for(String arg : args) {
+    }
+  }
+}
diff --git a/jbmc/regression/jbmc/output-options/test.desc b/jbmc/regression/jbmc/output-options/test.desc
new file mode 100644
index 00000000000..df330695097
--- /dev/null
+++ b/jbmc/regression/jbmc/output-options/test.desc
@@ -0,0 +1,23 @@
+CORE symex-driven-lazy-loading-expected-failure
+Main.class
+--verbosity 10 --unwind 2 --disable-uncaught-exception-check --throw-assertion-error
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+assertions: "1"
+assumptions: "1"
+java-threading: "0"
+lazy-methods: "1"
+propagation: "1"
+refine-strings: "1"
+sat-preprocessor: "1"
+simplify: "1"
+simplify-if: "1"
+symex-driven-lazy-loading: "0"
+throw-assertion-error: "1"
+throw-runtime-exceptions: "0"
+uncaught-exception-check: "0"
+unwind: "2"
+--
+--
+Symex-driven lazy loading would expect symex-driven-lazy-loading: "1".
diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp
index 5a2a499eb07..60467ff66de 100644
--- a/jbmc/src/jbmc/jbmc_parse_options.cpp
+++ b/jbmc/src/jbmc/jbmc_parse_options.cpp
@@ -20,6 +20,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/exit_codes.h>
 #include <util/invariant.h>
 #include <util/unicode.h>
+#include <util/xml.h>
 #include <util/version.h>
 
 #include <langapi/language.h>
@@ -390,6 +391,9 @@ int jbmc_parse_optionst::doit()
     return 0; // should contemplate EX_OK from sysexits.h
   }
 
+  eval_verbosity(
+    cmdline.get_value("verbosity"), messaget::M_STATISTICS, ui_message_handler);
+
   //
   // command line options
   //
@@ -412,9 +416,6 @@ int jbmc_parse_optionst::doit()
     return 6; // should contemplate EX_SOFTWARE from sysexits.h
   }
 
-  eval_verbosity(
-    cmdline.get_value("verbosity"), messaget::M_STATISTICS, ui_message_handler);
-
   //
   // Print a banner
   //
@@ -422,6 +423,28 @@ int jbmc_parse_optionst::doit()
            << "-bit " << config.this_architecture() << " "
            << config.this_operating_system() << eom;
 
+  // output the options
+  switch(ui_message_handler.get_ui())
+  {
+    case ui_message_handlert::uit::PLAIN:
+      conditional_output(debug(), [&options](messaget::mstreamt &mstream) {
+        mstream << "\nOptions: \n";
+        options.output(mstream);
+        mstream << messaget::eom;
+      });
+      break;
+    case ui_message_handlert::uit::JSON_UI:
+    {
+      json_objectt json_options;
+      json_options["options"] = options.to_json();
+      debug() << json_options;
+      break;
+    }
+    case ui_message_handlert::uit::XML_UI:
+      debug() << options.to_xml();
+      break;
+  }
+
   register_language(new_ansi_c_language);
   register_language(new_java_bytecode_language);
 
diff --git a/src/util/options.cpp b/src/util/options.cpp
index 65c805a8b65..c75a02182c1 100644
--- a/src/util/options.cpp
+++ b/src/util/options.cpp
@@ -11,7 +11,9 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "options.h"
 
+#include "json.h"
 #include "string2int.h"
+#include "xml.h"
 
 void optionst::set_option(const std::string &option,
                           const std::string &value)
@@ -84,3 +86,52 @@ const optionst::value_listt &optionst::get_list_option(
   else
     return it->second;
 }
+
+/// Returns the options as JSON key value pairs
+json_objectt optionst::to_json() const
+{
+  json_objectt json_options;
+  for(const auto &option_pair : option_map)
+  {
+    json_arrayt &values = json_options[option_pair.first].make_array();
+    for(const auto &value : option_pair.second)
+      values.push_back(json_stringt(value));
+  }
+  return json_options;
+}
+
+/// Returns the options in XML format
+xmlt optionst::to_xml() const
+{
+  xmlt xml_options("options");
+  for(const auto &option_pair : option_map)
+  {
+    xmlt &xml_option = xml_options.new_element("option");
+    xml_option.set_attribute("name", option_pair.first);
+    for(const auto &value : option_pair.second)
+    {
+      xmlt &xml_value = xml_option.new_element("value");
+      xml_value.data = value;
+    }
+  }
+  return xml_options;
+}
+
+/// Outputs the options to `out`
+void optionst::output(std::ostream &out) const
+{
+  for(const auto &option_pair : option_map)
+  {
+    out << option_pair.first << ": ";
+    bool first = true;
+    for(const auto &value : option_pair.second)
+    {
+      if(first)
+        first = false;
+      else
+        out << ", ";
+      out << '"' << value << '"';
+    }
+    out << "\n";
+  }
+}
diff --git a/src/util/options.h b/src/util/options.h
index 741157740e6..d2e35c8c11c 100644
--- a/src/util/options.h
+++ b/src/util/options.h
@@ -16,6 +16,9 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <map>
 #include <list>
 
+class json_objectt;
+class xmlt;
+
 class optionst
 {
 public:
@@ -55,6 +58,10 @@ class optionst
     return *this;
   }
 
+  json_objectt to_json() const;
+  xmlt to_xml() const;
+  void output(std::ostream &out) const;
+
 protected:
   option_mapt option_map;
   const value_listt empty_list;