diff --git a/src/ebmc/Makefile b/src/ebmc/Makefile
index 2901d837c..aab061feb 100644
--- a/src/ebmc/Makefile
+++ b/src/ebmc/Makefile
@@ -1,6 +1,7 @@
 SRC = \
       bdd_engine.cpp \
       bmc.cpp \
+      build_transition_system.cpp \
       cegar/abstract.cpp \
       cegar/bmc_cegar.cpp \
       cegar/latch_ordering.cpp \
diff --git a/src/ebmc/build_transition_system.cpp b/src/ebmc/build_transition_system.cpp
new file mode 100644
index 000000000..dc9af380f
--- /dev/null
+++ b/src/ebmc/build_transition_system.cpp
@@ -0,0 +1,351 @@
+/*******************************************************************\
+
+Module: Transition Systems for EBMC
+
+Author: Daniel Kroening, dkr@amazon.com
+
+\*******************************************************************/
+
+#include "build_transition_system.h"
+
+#include <util/cmdline.h>
+#include <util/get_module.h>
+#include <util/message.h>
+#include <util/namespace.h>
+#include <util/options.h>
+#include <util/unicode.h>
+
+#include <langapi/language.h>
+#include <langapi/language_util.h>
+#include <langapi/mode.h>
+#include <trans-word-level/show_module_hierarchy.h>
+#include <trans-word-level/show_modules.h>
+
+#include "ebmc_error.h"
+#include "ebmc_language_file.h"
+#include "ebmc_version.h"
+#include "output_file.h"
+#include "transition_system.h"
+
+#include <fstream>
+#include <iostream>
+
+int 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;
+  }
+
+  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;
+  }
+
+  auto language = get_language_from_filename(filename);
+
+  if(language == nullptr)
+  {
+    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;
+  }
+
+  optionst options;
+
+  // do -I
+  if(cmdline.isset('I'))
+    options.set_option("I", cmdline.get_values('I'));
+
+  options.set_option("force-systemverilog", cmdline.isset("systemverilog"));
+
+  // do -D
+  if(cmdline.isset('D'))
+    options.set_option("defines", cmdline.get_values('D'));
+
+  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;
+}
+
+static bool parse(
+  const cmdlinet &cmdline,
+  const std::string &filename,
+  ebmc_language_filest &language_files,
+  message_handlert &message_handler)
+{
+  messaget message(message_handler);
+
+  std::ifstream infile(widen_if_needed(filename));
+
+  if(!infile)
+  {
+    message.error() << "failed to open input file `" << filename << "'"
+                    << messaget::eom;
+    return true;
+  }
+
+  auto &lf = language_files.add_file(filename);
+  lf.filename = filename;
+  lf.language = get_language_from_filename(filename);
+
+  if(lf.language == nullptr)
+  {
+    source_locationt location;
+    location.set_file(filename);
+    message.error().source_location = location;
+    message.error() << "failed to figure out type of file" << messaget::eom;
+    return true;
+  }
+
+  languaget &language = *lf.language;
+
+  optionst options;
+
+  // do -I
+  if(cmdline.isset('I'))
+    options.set_option("I", cmdline.get_values('I'));
+
+  options.set_option("force-systemverilog", cmdline.isset("systemverilog"));
+  options.set_option("vl2smv-extensions", cmdline.isset("vl2smv-extensions"));
+  options.set_option("warn-implicit-nets", cmdline.isset("warn-implicit-nets"));
+
+  // do -D
+  if(cmdline.isset('D'))
+    options.set_option("defines", cmdline.get_values('D'));
+
+  // do --ignore-initial
+  if(cmdline.isset("ignore-initial"))
+    options.set_option("ignore-initial", true);
+
+  // do --initial-zero
+  if(cmdline.isset("initial-zero"))
+    options.set_option("initial-zero", true);
+
+  language.set_language_options(options, message_handler);
+
+  message.status() << "Parsing " << filename << messaget::eom;
+
+  if(language.parse(infile, filename, message_handler))
+  {
+    message.error() << "PARSING ERROR\n";
+    return true;
+  }
+
+  lf.get_modules();
+
+  return false;
+}
+
+bool parse(
+  const cmdlinet &cmdline,
+  ebmc_language_filest &language_files,
+  message_handlert &message_handler)
+{
+  for(unsigned i = 0; i < cmdline.args.size(); i++)
+  {
+    if(parse(cmdline, cmdline.args[i], language_files, message_handler))
+      return true;
+  }
+  return false;
+}
+
+bool get_main(
+  const cmdlinet &cmdline,
+  message_handlert &message_handler,
+  transition_systemt &transition_system)
+{
+  std::string top_module;
+
+  if(cmdline.isset("module"))
+    top_module = cmdline.get_value("module");
+  else if(cmdline.isset("top"))
+    top_module = cmdline.get_value("top");
+
+  try
+  {
+    transition_system.main_symbol =
+      &get_module(transition_system.symbol_table, top_module, message_handler);
+    transition_system.trans_expr =
+      to_trans_expr(transition_system.main_symbol->value);
+  }
+
+  catch(int e)
+  {
+    return true;
+  }
+
+  return false;
+}
+
+void make_next_state(exprt &expr)
+{
+  for(auto &sub_expression : expr.operands())
+    make_next_state(sub_expression);
+
+  if(expr.id() == ID_symbol)
+    expr.id(ID_next_symbol);
+}
+
+int get_transition_system(
+  const cmdlinet &cmdline,
+  message_handlert &message_handler,
+  transition_systemt &transition_system)
+{
+  messaget message(message_handler);
+
+  if(cmdline.isset("preprocess"))
+    return preprocess(cmdline, message_handler);
+
+  //
+  // parsing
+  //
+  ebmc_language_filest language_files;
+
+  if(parse(cmdline, language_files, message_handler))
+    return 1;
+
+  if(cmdline.isset("show-parse"))
+  {
+    language_files.show_parse(std::cout, message_handler);
+    return 0;
+  }
+
+  //
+  // type checking
+  //
+
+  message.status() << "Converting" << messaget::eom;
+
+  if(language_files.typecheck(transition_system.symbol_table, message_handler))
+  {
+    message.error() << "CONVERSION ERROR" << messaget::eom;
+    return 2;
+  }
+
+  if(cmdline.isset("show-modules"))
+  {
+    show_modules(transition_system.symbol_table, std::cout);
+    return 0;
+  }
+
+  if(cmdline.isset("modules-xml"))
+  {
+    auto filename = cmdline.get_value("modules-xml");
+    auto outfile = output_filet{filename};
+    show_modules_xml(transition_system.symbol_table, outfile.stream());
+    return 0;
+  }
+
+  if(cmdline.isset("json-modules"))
+  {
+    auto out_file = output_filet{cmdline.get_value("json-modules")};
+    json_modules(transition_system.symbol_table, out_file.stream());
+    return 0;
+  }
+
+  if(cmdline.isset("show-symbol-table"))
+  {
+    std::cout << transition_system.symbol_table;
+    return 0;
+  }
+
+  // get module name
+
+  if(get_main(cmdline, message_handler, transition_system))
+    return 1;
+
+  if(cmdline.isset("show-module-hierarchy"))
+  {
+    DATA_INVARIANT(
+      transition_system.main_symbol != nullptr, "must have main_symbol");
+    show_module_hierarchy(
+      transition_system.symbol_table,
+      *transition_system.main_symbol,
+      std::cout);
+    return 0;
+  }
+
+  // --reset given?
+  if(cmdline.isset("reset"))
+  {
+    namespacet ns(transition_system.symbol_table);
+    exprt reset_constraint = to_expr(
+      ns, transition_system.main_symbol->name, cmdline.get_value("reset"));
+
+    // true in initial state
+    transt new_trans_expr = transition_system.trans_expr;
+    new_trans_expr.init() = and_exprt(new_trans_expr.init(), reset_constraint);
+
+    // and not anymore afterwards
+    exprt reset_next_state = reset_constraint;
+    make_next_state(reset_next_state);
+
+    new_trans_expr.trans() =
+      and_exprt(new_trans_expr.trans(), not_exprt(reset_next_state));
+    transition_system.trans_expr = new_trans_expr;
+  }
+
+  return -1; // done with the transition system
+}
+
+transition_systemt get_transition_system(
+  const cmdlinet &cmdline,
+  message_handlert &message_handler)
+{
+  transition_systemt transition_system;
+  auto exit_code =
+    get_transition_system(cmdline, message_handler, transition_system);
+  if(exit_code != -1)
+    throw ebmc_errort().with_exit_code(exit_code);
+  return transition_system;
+}
+
+int show_parse(const cmdlinet &cmdline, message_handlert &message_handler)
+{
+  transition_systemt dummy_transition_system;
+  return get_transition_system(
+    cmdline, message_handler, dummy_transition_system);
+}
+
+int show_modules(const cmdlinet &cmdline, message_handlert &message_handler)
+{
+  transition_systemt dummy_transition_system;
+  return get_transition_system(
+    cmdline, message_handler, dummy_transition_system);
+}
+
+int show_module_hierarchy(
+  const cmdlinet &cmdline,
+  message_handlert &message_handler)
+{
+  transition_systemt dummy_transition_system;
+  return get_transition_system(
+    cmdline, message_handler, dummy_transition_system);
+}
+
+int show_symbol_table(
+  const cmdlinet &cmdline,
+  message_handlert &message_handler)
+{
+  transition_systemt dummy_transition_system;
+  return get_transition_system(
+    cmdline, message_handler, dummy_transition_system);
+}
diff --git a/src/ebmc/build_transition_system.h b/src/ebmc/build_transition_system.h
new file mode 100644
index 000000000..e75622385
--- /dev/null
+++ b/src/ebmc/build_transition_system.h
@@ -0,0 +1,24 @@
+/*******************************************************************\
+
+Module: Transition Systems for EBMC
+
+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;
+
+transition_systemt get_transition_system(const cmdlinet &, message_handlert &);
+
+int 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 &);
+
+#endif // CPROVER_EBMC_BUILD_TRANSITION_SYSTEM_H
diff --git a/src/ebmc/ebmc_parse_options.cpp b/src/ebmc/ebmc_parse_options.cpp
index a39fbc3cb..3d9733130 100644
--- a/src/ebmc/ebmc_parse_options.cpp
+++ b/src/ebmc/ebmc_parse_options.cpp
@@ -15,6 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <trans-netlist/smv_netlist.h>
 
+#include "build_transition_system.h"
 #include "diatest.h"
 #include "ebmc_base.h"
 #include "ebmc_error.h"
diff --git a/src/ebmc/neural_liveness.cpp b/src/ebmc/neural_liveness.cpp
index 13aac05a3..b55db6aff 100644
--- a/src/ebmc/neural_liveness.cpp
+++ b/src/ebmc/neural_liveness.cpp
@@ -17,6 +17,7 @@ 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"
diff --git a/src/ebmc/random_traces.cpp b/src/ebmc/random_traces.cpp
index 68ef7b420..b761c6244 100644
--- a/src/ebmc/random_traces.cpp
+++ b/src/ebmc/random_traces.cpp
@@ -20,6 +20,7 @@ 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"
diff --git a/src/ebmc/ranking_function.cpp b/src/ebmc/ranking_function.cpp
index 2e7ad5ed3..770939e6c 100644
--- a/src/ebmc/ranking_function.cpp
+++ b/src/ebmc/ranking_function.cpp
@@ -21,6 +21,7 @@ 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"
diff --git a/src/ebmc/transition_system.cpp b/src/ebmc/transition_system.cpp
index 53dd70c21..56a5fa911 100644
--- a/src/ebmc/transition_system.cpp
+++ b/src/ebmc/transition_system.cpp
@@ -74,326 +74,6 @@ void transition_systemt::output(std::ostream &out) const
   ::output(trans_expr.trans(), out, *language, ns);
 }
 
-int 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;
-  }
-
-  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;
-  }
-
-  auto language = get_language_from_filename(filename);
-
-  if(language == nullptr)
-  {
-    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;
-  }
-
-  optionst options;
-
-  // do -I
-  if(cmdline.isset('I'))
-    options.set_option("I", cmdline.get_values('I'));
-
-  options.set_option("force-systemverilog", cmdline.isset("systemverilog"));
-
-  // do -D
-  if(cmdline.isset('D'))
-    options.set_option("defines", cmdline.get_values('D'));
-
-  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;
-}
-
-static bool parse(
-  const cmdlinet &cmdline,
-  const std::string &filename,
-  ebmc_language_filest &language_files,
-  message_handlert &message_handler)
-{
-  messaget message(message_handler);
-
-  std::ifstream infile(widen_if_needed(filename));
-
-  if(!infile)
-  {
-    message.error() << "failed to open input file `" << filename << "'"
-                    << messaget::eom;
-    return true;
-  }
-
-  auto &lf = language_files.add_file(filename);
-  lf.filename = filename;
-  lf.language = get_language_from_filename(filename);
-
-  if(lf.language == nullptr)
-  {
-    source_locationt location;
-    location.set_file(filename);
-    message.error().source_location = location;
-    message.error() << "failed to figure out type of file" << messaget::eom;
-    return true;
-  }
-
-  languaget &language = *lf.language;
-
-  optionst options;
-
-  // do -I
-  if(cmdline.isset('I'))
-    options.set_option("I", cmdline.get_values('I'));
-
-  options.set_option("force-systemverilog", cmdline.isset("systemverilog"));
-  options.set_option("vl2smv-extensions", cmdline.isset("vl2smv-extensions"));
-  options.set_option("warn-implicit-nets", cmdline.isset("warn-implicit-nets"));
-
-  // do -D
-  if(cmdline.isset('D'))
-    options.set_option("defines", cmdline.get_values('D'));
-
-  // do --ignore-initial
-  if(cmdline.isset("ignore-initial"))
-    options.set_option("ignore-initial", true);
-
-  // do --initial-zero
-  if(cmdline.isset("initial-zero"))
-    options.set_option("initial-zero", true);
-
-  language.set_language_options(options, message_handler);
-
-  message.status() << "Parsing " << filename << messaget::eom;
-
-  if(language.parse(infile, filename, message_handler))
-  {
-    message.error() << "PARSING ERROR\n";
-    return true;
-  }
-
-  lf.get_modules();
-
-  return false;
-}
-
-bool parse(
-  const cmdlinet &cmdline,
-  ebmc_language_filest &language_files,
-  message_handlert &message_handler)
-{
-  for(unsigned i = 0; i < cmdline.args.size(); i++)
-  {
-    if(parse(cmdline, cmdline.args[i], language_files, message_handler))
-      return true;
-  }
-  return false;
-}
-
-bool get_main(
-  const cmdlinet &cmdline,
-  message_handlert &message_handler,
-  transition_systemt &transition_system)
-{
-  std::string top_module;
-
-  if(cmdline.isset("module"))
-    top_module = cmdline.get_value("module");
-  else if(cmdline.isset("top"))
-    top_module = cmdline.get_value("top");
-
-  try
-  {
-    transition_system.main_symbol =
-      &get_module(transition_system.symbol_table, top_module, message_handler);
-    transition_system.trans_expr =
-      to_trans_expr(transition_system.main_symbol->value);
-  }
-
-  catch(int e)
-  {
-    return true;
-  }
-
-  return false;
-}
-
-void make_next_state(exprt &expr)
-{
-  for(auto &sub_expression : expr.operands())
-    make_next_state(sub_expression);
-
-  if(expr.id() == ID_symbol)
-    expr.id(ID_next_symbol);
-}
-
-int get_transition_system(
-  const cmdlinet &cmdline,
-  message_handlert &message_handler,
-  transition_systemt &transition_system)
-{
-  messaget message(message_handler);
-
-  if(cmdline.isset("preprocess"))
-    return preprocess(cmdline, message_handler);
-
-  //
-  // parsing
-  //
-  ebmc_language_filest language_files;
-
-  if(parse(cmdline, language_files, message_handler))
-    return 1;
-
-  if(cmdline.isset("show-parse"))
-  {
-    language_files.show_parse(std::cout, message_handler);
-    return 0;
-  }
-
-  //
-  // type checking
-  //
-
-  message.status() << "Converting" << messaget::eom;
-
-  if(language_files.typecheck(transition_system.symbol_table, message_handler))
-  {
-    message.error() << "CONVERSION ERROR" << messaget::eom;
-    return 2;
-  }
-
-  if(cmdline.isset("show-modules"))
-  {
-    show_modules(transition_system.symbol_table, std::cout);
-    return 0;
-  }
-
-  if(cmdline.isset("modules-xml"))
-  {
-    auto filename = cmdline.get_value("modules-xml");
-    auto outfile = output_filet{filename};
-    show_modules_xml(transition_system.symbol_table, outfile.stream());
-    return 0;
-  }
-
-  if(cmdline.isset("json-modules"))
-  {
-    auto out_file = output_filet{cmdline.get_value("json-modules")};
-    json_modules(transition_system.symbol_table, out_file.stream());
-    return 0;
-  }
-
-  if(cmdline.isset("show-symbol-table"))
-  {
-    std::cout << transition_system.symbol_table;
-    return 0;
-  }
-
-  // get module name
-
-  if(get_main(cmdline, message_handler, transition_system))
-    return 1;
-
-  if(cmdline.isset("show-module-hierarchy"))
-  {
-    DATA_INVARIANT(
-      transition_system.main_symbol != nullptr, "must have main_symbol");
-    show_module_hierarchy(
-      transition_system.symbol_table,
-      *transition_system.main_symbol,
-      std::cout);
-    return 0;
-  }
-
-  // --reset given?
-  if(cmdline.isset("reset"))
-  {
-    namespacet ns(transition_system.symbol_table);
-    exprt reset_constraint = to_expr(
-      ns, transition_system.main_symbol->name, cmdline.get_value("reset"));
-
-    // true in initial state
-    transt new_trans_expr = transition_system.trans_expr;
-    new_trans_expr.init() = and_exprt(new_trans_expr.init(), reset_constraint);
-
-    // and not anymore afterwards
-    exprt reset_next_state = reset_constraint;
-    make_next_state(reset_next_state);
-
-    new_trans_expr.trans() =
-      and_exprt(new_trans_expr.trans(), not_exprt(reset_next_state));
-    transition_system.trans_expr = new_trans_expr;
-  }
-
-  return -1; // done with the transition system
-}
-
-transition_systemt get_transition_system(
-  const cmdlinet &cmdline,
-  message_handlert &message_handler)
-{
-  transition_systemt transition_system;
-  auto exit_code =
-    get_transition_system(cmdline, message_handler, transition_system);
-  if(exit_code != -1)
-    throw ebmc_errort().with_exit_code(exit_code);
-  return transition_system;
-}
-
-int show_parse(const cmdlinet &cmdline, message_handlert &message_handler)
-{
-  transition_systemt dummy_transition_system;
-  return get_transition_system(
-    cmdline, message_handler, dummy_transition_system);
-}
-
-int show_modules(const cmdlinet &cmdline, message_handlert &message_handler)
-{
-  transition_systemt dummy_transition_system;
-  return get_transition_system(
-    cmdline, message_handler, dummy_transition_system);
-}
-
-int show_module_hierarchy(
-  const cmdlinet &cmdline,
-  message_handlert &message_handler)
-{
-  transition_systemt dummy_transition_system;
-  return get_transition_system(
-    cmdline, message_handler, dummy_transition_system);
-}
-
-int show_symbol_table(
-  const cmdlinet &cmdline,
-  message_handlert &message_handler)
-{
-  transition_systemt dummy_transition_system;
-  return get_transition_system(
-    cmdline, message_handler, dummy_transition_system);
-}
-
 std::vector<symbol_exprt> transition_systemt::state_variables() const
 {
   std::vector<symbol_exprt> state_variables;
diff --git a/src/ebmc/transition_system.h b/src/ebmc/transition_system.h
index a2451632e..7056dccb9 100644
--- a/src/ebmc/transition_system.h
+++ b/src/ebmc/transition_system.h
@@ -13,9 +13,6 @@ Author: Daniel Kroening, dkr@amazon.com
 #include <util/std_expr.h>
 #include <util/symbol_table.h>
 
-class cmdlinet;
-class message_handlert;
-
 class transition_systemt
 {
 public:
@@ -34,12 +31,4 @@ class transition_systemt
   std::vector<symbol_exprt> inputs() const;
 };
 
-transition_systemt get_transition_system(const cmdlinet &, message_handlert &);
-
-int 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 &);
-
 #endif // CPROVER_EBMC_TRANSITION_SYSTEM_H