diff --git a/regression/verilog/preprocessor/unknown_directive.desc b/regression/verilog/preprocessor/unknown_directive.desc
index 1f6ce9b32..e718de61f 100644
--- a/regression/verilog/preprocessor/unknown_directive.desc
+++ b/regression/verilog/preprocessor/unknown_directive.desc
@@ -2,7 +2,6 @@ CORE
 unknown_directive.v
 --preprocess
 ^file unknown_directive\.v line 1: unknown preprocessor directive "something"$
-^PREPROCESSING FAILED$
 ^EXIT=1$
 ^SIGNAL=0$
 --
diff --git a/src/ebmc/Makefile b/src/ebmc/Makefile
index aab061feb..793f05b53 100644
--- a/src/ebmc/Makefile
+++ b/src/ebmc/Makefile
@@ -13,6 +13,7 @@ SRC = \
       diatest.cpp \
       dimacs_writer.cpp \
       ebmc_base.cpp \
+      ebmc_language.cpp \
       ebmc_language_file.cpp \
       ebmc_languages.cpp \
       ebmc_parse_options.cpp \
diff --git a/src/ebmc/build_transition_system.cpp b/src/ebmc/build_transition_system.cpp
index dc9af380f..1471e2a1f 100644
--- a/src/ebmc/build_transition_system.cpp
+++ b/src/ebmc/build_transition_system.cpp
@@ -30,26 +30,20 @@ Author: Daniel Kroening, dkr@amazon.com
 #include <fstream>
 #include <iostream>
 
-int preprocess(const cmdlinet &cmdline, message_handlert &message_handler)
+void preprocess(const cmdlinet &cmdline, message_handlert &message_handler)
 {
   messaget message(message_handler);
 
   if(cmdline.args.size() != 1)
-  {
-    message.error() << "please give exactly one file to preprocess"
-                    << messaget::eom;
-    return 1;
-  }
+    throw ebmc_errort{}.with_exit_code(1)
+      << "please give exactly one file to preprocess";
 
   const auto &filename = cmdline.args.front();
   std::ifstream infile(widen_if_needed(filename));
 
   if(!infile)
-  {
-    message.error() << "failed to open input file `" << filename << "'"
-                    << messaget::eom;
-    return 1;
-  }
+    throw ebmc_errort{}.with_exit_code(1)
+      << "failed to open input file `" << filename << "'";
 
   auto language = get_language_from_filename(filename);
 
@@ -57,9 +51,8 @@ int preprocess(const cmdlinet &cmdline, message_handlert &message_handler)
   {
     source_locationt location;
     location.set_file(filename);
-    message.error().source_location = location;
-    message.error() << "failed to figure out type of file" << messaget::eom;
-    return 1;
+    throw ebmc_errort{}.with_location(location).with_exit_code(1)
+      << "failed to figure out type of file";
   }
 
   optionst options;
@@ -77,12 +70,7 @@ int preprocess(const cmdlinet &cmdline, message_handlert &message_handler)
   language->set_language_options(options, message_handler);
 
   if(language->preprocess(infile, filename, std::cout, message_handler))
-  {
-    message.error() << "PREPROCESSING FAILED" << messaget::eom;
-    return 1;
-  }
-
-  return 0;
+    throw ebmc_errort{}.with_exit_code(1);
 }
 
 static bool parse(
@@ -211,9 +199,6 @@ int get_transition_system(
 {
   messaget message(message_handler);
 
-  if(cmdline.isset("preprocess"))
-    return preprocess(cmdline, message_handler);
-
   //
   // parsing
   //
@@ -349,3 +334,40 @@ int show_symbol_table(
   return get_transition_system(
     cmdline, message_handler, dummy_transition_system);
 }
+
+std::optional<transition_systemt> ebmc_languagest::transition_system()
+{
+  if(cmdline.isset("preprocess"))
+  {
+    preprocess(cmdline, message_handler);
+    return {};
+  }
+
+  if(cmdline.isset("show-parse"))
+  {
+    show_parse(cmdline, message_handler);
+    return {};
+  }
+
+  if(
+    cmdline.isset("show-modules") || cmdline.isset("modules-xml") ||
+    cmdline.isset("json-modules"))
+  {
+    show_modules(cmdline, message_handler);
+    return {};
+  }
+
+  if(cmdline.isset("show-module-hierarchy"))
+  {
+    show_module_hierarchy(cmdline, message_handler);
+    return {};
+  }
+
+  if(cmdline.isset("show-symbol-table"))
+  {
+    show_symbol_table(cmdline, message_handler);
+    return {};
+  }
+
+  return get_transition_system(cmdline, message_handler);
+}
diff --git a/src/ebmc/build_transition_system.h b/src/ebmc/build_transition_system.h
index e75622385..35c345a2f 100644
--- a/src/ebmc/build_transition_system.h
+++ b/src/ebmc/build_transition_system.h
@@ -9,16 +9,25 @@ Author: Daniel Kroening, dkr@amazon.com
 #ifndef CPROVER_EBMC_BUILD_TRANSITION_SYSTEM_H
 #define CPROVER_EBMC_BUILD_TRANSITION_SYSTEM_H
 
-class cmdlinet;
-class message_handlert;
-class transition_systemt;
+#include "ebmc_language.h"
 
 transition_systemt get_transition_system(const cmdlinet &, message_handlert &);
 
-int preprocess(const cmdlinet &, message_handlert &);
+void preprocess(const cmdlinet &, message_handlert &);
 int show_parse(const cmdlinet &, message_handlert &);
 int show_modules(const cmdlinet &, message_handlert &);
 int show_module_hierarchy(const cmdlinet &, message_handlert &);
 int show_symbol_table(const cmdlinet &, message_handlert &);
 
+class ebmc_languagest : public ebmc_languaget
+{
+public:
+  ebmc_languagest(cmdlinet &_cmdline, message_handlert &_message_handler)
+    : ebmc_languaget{_cmdline, _message_handler}
+  {
+  }
+
+  std::optional<transition_systemt> transition_system() override;
+};
+
 #endif // CPROVER_EBMC_BUILD_TRANSITION_SYSTEM_H
diff --git a/src/ebmc/ebmc_language.cpp b/src/ebmc/ebmc_language.cpp
new file mode 100644
index 000000000..2eddf7e72
--- /dev/null
+++ b/src/ebmc/ebmc_language.cpp
@@ -0,0 +1,13 @@
+/*******************************************************************\
+
+Module: Abstract interface to support a modeling language
+
+Author: Daniel Kroening, dkr@amazon.com
+
+\*******************************************************************/
+
+#include "ebmc_language.h"
+
+ebmc_languaget::~ebmc_languaget()
+{
+}
diff --git a/src/ebmc/ebmc_language.h b/src/ebmc/ebmc_language.h
new file mode 100644
index 000000000..d49f80917
--- /dev/null
+++ b/src/ebmc/ebmc_language.h
@@ -0,0 +1,42 @@
+/*******************************************************************\
+
+Module: Abstract interface to support a modeling language
+
+Author: Daniel Kroening, dkr@amazon.com
+
+\*******************************************************************/
+
+/// \file
+/// Abstract interface to support a modeling language
+
+#ifndef EBMC_LANGUAGE_H
+#define EBMC_LANGUAGE_H
+
+#include <iosfwd>
+#include <optional>
+
+class cmdlinet;
+class message_handlert;
+class transition_systemt;
+
+class ebmc_languaget
+{
+public:
+  // constructor / destructor
+  ebmc_languaget(cmdlinet &_cmdline, message_handlert &_message_handler)
+    : cmdline(_cmdline), message_handler(_message_handler)
+  {
+  }
+
+  virtual ~ebmc_languaget();
+
+  /// Produce the transition system, and return it;
+  /// returns {} when diagnostic output was produced instead.
+  virtual std::optional<transition_systemt> transition_system() = 0;
+
+protected:
+  cmdlinet &cmdline;
+  message_handlert &message_handler;
+};
+
+#endif // EBMC_LANGUAGE_H
diff --git a/src/ebmc/ebmc_parse_options.cpp b/src/ebmc/ebmc_parse_options.cpp
index 3d9733130..478501507 100644
--- a/src/ebmc/ebmc_parse_options.cpp
+++ b/src/ebmc/ebmc_parse_options.cpp
@@ -19,6 +19,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "diatest.h"
 #include "ebmc_base.h"
 #include "ebmc_error.h"
+#include "ebmc_language.h"
 #include "ebmc_version.h"
 #include "format_hooks.h"
 #include "instrument_buechi.h"
@@ -108,23 +109,6 @@ int ebmc_parse_optionst::doit()
       return 0;
     }
 
-    if(cmdline.isset("preprocess"))
-      return preprocess(cmdline, ui_message_handler);
-
-    if(cmdline.isset("show-parse"))
-      return show_parse(cmdline, ui_message_handler);
-
-    if(
-      cmdline.isset("show-modules") || cmdline.isset("modules-xml") ||
-      cmdline.isset("json-modules"))
-      return show_modules(cmdline, ui_message_handler);
-
-    if(cmdline.isset("show-module-hierarchy"))
-      return show_module_hierarchy(cmdline, ui_message_handler);
-
-    if(cmdline.isset("show-symbol-table"))
-      return show_symbol_table(cmdline, ui_message_handler);
-
     if(cmdline.isset("coverage"))
     {
       throw ebmc_errort() << "This option is currently disabled";
@@ -140,18 +124,6 @@ int ebmc_parse_optionst::doit()
 #endif
     }
 
-    if(cmdline.isset("random-traces"))
-      return random_traces(cmdline, ui_message_handler);
-
-    if(cmdline.isset("random-trace") || cmdline.isset("random-waveform"))
-      return random_trace(cmdline, ui_message_handler);
-
-    if(cmdline.isset("neural-liveness"))
-      return do_neural_liveness(cmdline, ui_message_handler);
-
-    if(cmdline.isset("ranking-function"))
-      return do_ranking_function(cmdline, ui_message_handler);
-
     if(cmdline.isset("interpolation-word"))
     {
       throw ebmc_errort() << "This option is currently disabled";
@@ -208,7 +180,28 @@ int ebmc_parse_optionst::doit()
     }
 
     // get the transition system
-    auto transition_system = get_transition_system(cmdline, ui_message_handler);
+    ebmc_languagest ebmc_languages{cmdline, ui_message_handler};
+
+    auto transition_system_opt = ebmc_languages.transition_system();
+
+    // Did we produce diagnostics instead?
+    if(!transition_system_opt.has_value())
+      return 0;
+
+    auto &transition_system = transition_system_opt.value();
+
+    if(cmdline.isset("random-traces"))
+      return random_traces(transition_system, cmdline, ui_message_handler);
+
+    if(cmdline.isset("random-trace") || cmdline.isset("random-waveform"))
+      return random_trace(transition_system, cmdline, ui_message_handler);
+
+    if(cmdline.isset("neural-liveness"))
+      return do_neural_liveness(transition_system, cmdline, ui_message_handler);
+
+    if(cmdline.isset("ranking-function"))
+      return do_ranking_function(
+        transition_system, cmdline, ui_message_handler);
 
     // get the properties
     auto properties = ebmc_propertiest::from_command_line(
diff --git a/src/ebmc/neural_liveness.cpp b/src/ebmc/neural_liveness.cpp
index b55db6aff..5188f92cc 100644
--- a/src/ebmc/neural_liveness.cpp
+++ b/src/ebmc/neural_liveness.cpp
@@ -17,7 +17,6 @@ Author: Daniel Kroening, dkr@amazon.com
 #include <temporal-logic/temporal_expr.h>
 #include <verilog/sva_expr.h>
 
-#include "build_transition_system.h"
 #include "ebmc_error.h"
 #include "ebmc_solver_factory.h"
 #include "live_signal.h"
@@ -42,10 +41,14 @@ Author: Daniel Kroening, dkr@amazon.com
 class neural_livenesst
 {
 public:
-  neural_livenesst(const cmdlinet &_cmdline, message_handlert &_message_handler)
+  neural_livenesst(
+    transition_systemt &_transition_system,
+    const cmdlinet &_cmdline,
+    message_handlert &_message_handler)
     : cmdline(_cmdline),
       message(_message_handler),
-      solver_factory(ebmc_solver_factory(_cmdline))
+      solver_factory(ebmc_solver_factory(_cmdline)),
+      transition_system(_transition_system)
   {
   }
 
@@ -55,7 +58,7 @@ class neural_livenesst
   const cmdlinet &cmdline;
   messaget message;
   ebmc_solver_factoryt solver_factory;
-  transition_systemt transition_system;
+  transition_systemt &transition_system;
   ebmc_propertiest properties;
 
   int show_traces();
@@ -75,9 +78,6 @@ int neural_livenesst::operator()()
   if(!cmdline.isset("neural-engine"))
     throw ebmc_errort() << "give a neural engine";
 
-  transition_system =
-    get_transition_system(cmdline, message.get_message_handler());
-
   // Get the properties
   properties = ebmc_propertiest::from_command_line(
     cmdline, transition_system, message.get_message_handler());
@@ -127,9 +127,6 @@ int neural_livenesst::operator()()
 
 int neural_livenesst::show_traces()
 {
-  transition_system =
-    get_transition_system(cmdline, message.get_message_handler());
-
   properties = ebmc_propertiest::from_command_line(
     cmdline, transition_system, message.get_message_handler());
 
@@ -317,8 +314,9 @@ tvt neural_livenesst::verify(
 }
 
 int do_neural_liveness(
+  transition_systemt &transition_system,
   const cmdlinet &cmdline,
-  ui_message_handlert &ui_message_handler)
+  message_handlert &message_handler)
 {
-  return neural_livenesst(cmdline, ui_message_handler)();
+  return neural_livenesst{transition_system, cmdline, message_handler}();
 }
diff --git a/src/ebmc/neural_liveness.h b/src/ebmc/neural_liveness.h
index 159f38208..ed47bb555 100644
--- a/src/ebmc/neural_liveness.h
+++ b/src/ebmc/neural_liveness.h
@@ -9,9 +9,13 @@ Author: Daniel Kroening, dkr@amazon.com
 #ifndef EBMC_NEURAL_LIVENESS_H
 #define EBMC_NEURAL_LIVENESS_H
 
-#include <util/cmdline.h>
-#include <util/ui_message.h>
+class cmdlinet;
+class message_handlert;
+class transition_systemt;
 
-int do_neural_liveness(const cmdlinet &, ui_message_handlert &);
+int do_neural_liveness(
+  transition_systemt &,
+  const cmdlinet &,
+  message_handlert &);
 
 #endif // EBMC_NEURAL_LIVENESS_H
diff --git a/src/ebmc/random_traces.cpp b/src/ebmc/random_traces.cpp
index b761c6244..d9e102805 100644
--- a/src/ebmc/random_traces.cpp
+++ b/src/ebmc/random_traces.cpp
@@ -20,7 +20,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <trans-word-level/trans_trace_word_level.h>
 #include <trans-word-level/unwind.h>
 
-#include "build_transition_system.h"
 #include "ebmc_base.h"
 #include "ebmc_error.h"
 #include "output_file.h"
@@ -113,7 +112,10 @@ Function: random_traces
 
 \*******************************************************************/
 
-int random_traces(const cmdlinet &cmdline, message_handlert &message_handler)
+int random_traces(
+  const transition_systemt &transition_system,
+  const cmdlinet &cmdline,
+  message_handlert &message_handler)
 {
   const auto number_of_traces = [&cmdline]() -> std::size_t {
     if(cmdline.isset("traces"))
@@ -172,9 +174,6 @@ int random_traces(const cmdlinet &cmdline, message_handlert &message_handler)
       return {};
   }();
 
-  transition_systemt transition_system =
-    get_transition_system(cmdline, message_handler);
-
   if(cmdline.isset("waveform") && cmdline.isset("vcd"))
     throw ebmc_errort() << "cannot do VCD and ASCII waveform simultaneously";
 
@@ -232,7 +231,10 @@ Function: random_trace
 
 \*******************************************************************/
 
-int random_trace(const cmdlinet &cmdline, message_handlert &message_handler)
+int random_trace(
+  const transition_systemt &transition_system,
+  const cmdlinet &cmdline,
+  message_handlert &message_handler)
 {
   if(cmdline.isset("traces"))
     throw ebmc_errort() << "must not give number of traces";
@@ -276,9 +278,6 @@ int random_trace(const cmdlinet &cmdline, message_handlert &message_handler)
       return 10; // default
   }();
 
-  transition_systemt transition_system =
-    get_transition_system(cmdline, message_handler);
-
   auto consumer = [&](trans_tracet trace) -> void {
     namespacet ns(transition_system.symbol_table);
     if(cmdline.isset("random-waveform") || cmdline.isset("waveform"))
diff --git a/src/ebmc/random_traces.h b/src/ebmc/random_traces.h
index ccb03b584..92ba55645 100644
--- a/src/ebmc/random_traces.h
+++ b/src/ebmc/random_traces.h
@@ -16,14 +16,20 @@ Author: Daniel Kroening, kroening@kroening.com
 
 class cmdlinet;
 class message_handlert;
+class transition_systemt;
 
 // many traces
-int random_traces(const cmdlinet &, message_handlert &);
+int random_traces(
+  const transition_systemt &,
+  const cmdlinet &,
+  message_handlert &);
 
 // just one trace
-int random_trace(const cmdlinet &, message_handlert &);
+int random_trace(
+  const transition_systemt &,
+  const cmdlinet &,
+  message_handlert &);
 
-class transition_systemt;
 class trans_tracet;
 
 // many traces, VCD
diff --git a/src/ebmc/ranking_function.cpp b/src/ebmc/ranking_function.cpp
index 770939e6c..c35cc948a 100644
--- a/src/ebmc/ranking_function.cpp
+++ b/src/ebmc/ranking_function.cpp
@@ -21,7 +21,6 @@ Author: Daniel Kroening, dkr@amazon.com
 #include <trans-word-level/unwind.h>
 #include <verilog/sva_expr.h>
 
-#include "build_transition_system.h"
 #include "ebmc_base.h"
 #include "ebmc_error.h"
 #include "ebmc_solver_factory.h"
@@ -87,13 +86,10 @@ ebmc_propertiest::propertyt &find_property(ebmc_propertiest &properties)
 }
 
 int do_ranking_function(
+  const transition_systemt &transition_system,
   const cmdlinet &cmdline,
   message_handlert &message_handler)
 {
-  // get the transition system
-  transition_systemt transition_system =
-    get_transition_system(cmdline, message_handler);
-
   // parse the ranking function
   if(!cmdline.isset("ranking-function"))
     throw ebmc_errort() << "no candidate ranking function given";
diff --git a/src/ebmc/ranking_function.h b/src/ebmc/ranking_function.h
index d705705a0..bcd360efe 100644
--- a/src/ebmc/ranking_function.h
+++ b/src/ebmc/ranking_function.h
@@ -20,7 +20,10 @@ class exprt;
 class transition_systemt;
 class trans_tracet;
 
-int do_ranking_function(const cmdlinet &, message_handlert &);
+int do_ranking_function(
+  const transition_systemt &,
+  const cmdlinet &,
+  message_handlert &);
 
 exprt parse_ranking_function(
   const std::string &,