diff --git a/src/cbmc/bmc.h b/src/cbmc/bmc.h
index 4c69fab527c..f03a94e02ab 100644
--- a/src/cbmc/bmc.h
+++ b/src/cbmc/bmc.h
@@ -15,6 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <list>
 #include <map>
 
+#include <util/ui_message.h>
 #include <util/options.h>
 
 #include <solvers/prop/prop.h>
@@ -23,7 +24,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <solvers/sat/satcheck.h>
 #include <solvers/smt1/smt1_dec.h>
 #include <solvers/smt2/smt2_dec.h>
-#include <langapi/language_ui.h>
 #include <goto-symex/symex_target_equation.h>
 #include <goto-programs/safety_checker.h>
 
@@ -56,7 +56,7 @@ class bmct:public safety_checkert
   // additional stuff
   expr_listt bmc_constraints;
 
-  void set_ui(language_uit::uit _ui) { ui=_ui; }
+  void set_ui(ui_message_handlert::uit _ui) { ui=_ui; }
 
   // the safety_checkert interface
   virtual resultt operator()(
@@ -74,7 +74,7 @@ class bmct:public safety_checkert
   prop_convt &prop_conv;
 
   // use gui format
-  language_uit::uit ui;
+  ui_message_handlert::uit ui;
 
   virtual decision_proceduret::resultt
     run_decision_procedure(prop_convt &prop_conv);
diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
index ed6f3f081a2..15561cadf2e 100644
--- a/src/cbmc/cbmc_parse_options.cpp
+++ b/src/cbmc/cbmc_parse_options.cpp
@@ -25,7 +25,14 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <ansi-c/c_preprocess.h>
 
+#include <goto-programs/convert_nondet.h>
+#include <goto-programs/get_goto_model.h>
 #include <goto-programs/goto_convert_functions.h>
+#include <goto-programs/goto_inline.h>
+#include <goto-programs/link_to_library.h>
+#include <goto-programs/loop_ids.h>
+#include <goto-programs/mm_io.h>
+#include <goto-programs/read_goto_binary.h>
 #include <goto-programs/remove_function_pointers.h>
 #include <goto-programs/remove_virtual_functions.h>
 #include <goto-programs/remove_instanceof.h>
@@ -35,20 +42,15 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <goto-programs/remove_complex.h>
 #include <goto-programs/remove_asm.h>
 #include <goto-programs/remove_unused_functions.h>
+#include <goto-programs/remove_skip.h>
 #include <goto-programs/remove_static_init_loops.h>
-#include <goto-programs/mm_io.h>
-#include <goto-programs/goto_inline.h>
-#include <goto-programs/show_properties.h>
+#include <goto-programs/replace_java_nondet.h>
 #include <goto-programs/set_properties.h>
-#include <goto-programs/read_goto_binary.h>
+#include <goto-programs/show_goto_functions.h>
+#include <goto-programs/show_symbol_table.h>
+#include <goto-programs/show_properties.h>
 #include <goto-programs/string_abstraction.h>
 #include <goto-programs/string_instrumentation.h>
-#include <goto-programs/loop_ids.h>
-#include <goto-programs/link_to_library.h>
-#include <goto-programs/remove_skip.h>
-#include <goto-programs/show_goto_functions.h>
-#include <goto-programs/replace_java_nondet.h>
-#include <goto-programs/convert_nondet.h>
 
 #include <goto-symex/rewrite_union.h>
 #include <goto-symex/adjust_float_expressions.h>
@@ -71,7 +73,7 @@ Author: Daniel Kroening, kroening@kroening.com
 cbmc_parse_optionst::cbmc_parse_optionst(int argc, const char **argv):
   parse_options_baset(CBMC_OPTIONS, argc, argv),
   xml_interfacet(cmdline),
-  language_uit(cmdline, ui_message_handler),
+  messaget(ui_message_handler),
   ui_message_handler(cmdline, "CBMC " CBMC_VERSION)
 {
 }
@@ -82,7 +84,7 @@ ::cbmc_parse_optionst::cbmc_parse_optionst(
   const std::string &extra_options):
   parse_options_baset(CBMC_OPTIONS+extra_options, argc, argv),
   xml_interfacet(cmdline),
-  language_uit(cmdline, ui_message_handler),
+  messaget(ui_message_handler),
   ui_message_handler(cmdline, "CBMC " CBMC_VERSION)
 {
 }
@@ -470,7 +472,7 @@ int cbmc_parse_optionst::doit()
   register_languages();
 
   if(cmdline.isset("test-preprocessor"))
-    return test_c_preprocessor(ui_message_handler)?8:0;
+    return test_c_preprocessor(get_message_handler())?8:0;
 
   if(cmdline.isset("preprocess"))
   {
@@ -478,12 +480,56 @@ int cbmc_parse_optionst::doit()
     return 0; // should contemplate EX_OK from sysexits.h
   }
 
-  goto_functionst goto_functions;
+  if(cmdline.isset("show-parse-tree"))
+  {
+    if(cmdline.args.size()!=1 ||
+       is_goto_binary(cmdline.args[0]))
+    {
+      error() << "Please give exactly one source file" << eom;
+      return 6;
+    }
+
+    std::string filename=cmdline.args[0];
+
+    #ifdef _MSC_VER
+    std::ifstream infile(widen(filename));
+    #else
+    std::ifstream infile(filename);
+    #endif
+
+    if(!infile)
+    {
+      error() << "failed to open input file `"
+              << filename << "'" << eom;
+      return 6;
+    }
 
-  expr_listt bmc_constraints;
+    std::unique_ptr<languaget> language=
+      get_language_from_filename(filename);
 
-  int get_goto_program_ret=
-    get_goto_program(options, bmc_constraints, goto_functions);
+    if(language==nullptr)
+    {
+      error() << "failed to figure out type of file `"
+              <<  filename << "'" << eom;
+      return 6;
+    }
+
+    language->get_language_options(cmdline);
+    language->set_message_handler(get_message_handler());
+
+    status() << "Parsing " << filename << eom;
+
+    if(language->parse(infile, filename))
+    {
+      error() << "PARSING ERROR" << eom;
+      return 6;
+    }
+
+    language->show_parse(std::cout);
+    return 0;
+  }
+
+  int get_goto_program_ret=get_goto_program(options);
 
   if(get_goto_program_ret!=-1)
     return get_goto_program_ret;
@@ -491,26 +537,28 @@ int cbmc_parse_optionst::doit()
   if(cmdline.isset("show-claims") || // will go away
      cmdline.isset("show-properties")) // use this one
   {
-    const namespacet ns(symbol_table);
-    show_properties(ns, get_ui(), goto_functions);
+    show_properties(goto_model, ui_message_handler.get_ui());
     return 0; // should contemplate EX_OK from sysexits.h
   }
 
-  if(set_properties(goto_functions))
+  if(set_properties())
     return 7; // should contemplate EX_USAGE from sysexits.h
 
   // unwinds <clinit> loops to number of enum elements
   // side effect: add this as explicit unwind to unwind set
   if(options.get_bool_option("java-unwind-enum-static"))
     remove_static_init_loops(
-      symbol_table,
-      goto_functions,
+      goto_model.symbol_table,
+      goto_model.goto_functions,
       options,
-      ui_message_handler);
+      get_message_handler());
 
   // get solver
-  cbmc_solverst cbmc_solvers(options, symbol_table, ui_message_handler);
-  cbmc_solvers.set_ui(get_ui());
+  cbmc_solverst cbmc_solvers(
+    options,
+    goto_model.symbol_table,
+    get_message_handler());
+  cbmc_solvers.set_ui(ui_message_handler.get_ui());
 
   std::unique_ptr<cbmc_solverst::solvert> cbmc_solver;
 
@@ -527,21 +575,25 @@ int cbmc_parse_optionst::doit()
 
   prop_convt &prop_conv=cbmc_solver->prop_conv();
 
-  bmct bmc(options, symbol_table, ui_message_handler, prop_conv);
+  bmct bmc(
+    options,
+    goto_model.symbol_table,
+    get_message_handler(),
+    prop_conv);
 
   // do actual BMC
-  return do_bmc(bmc, goto_functions);
+  return do_bmc(bmc);
 }
 
-bool cbmc_parse_optionst::set_properties(goto_functionst &goto_functions)
+bool cbmc_parse_optionst::set_properties()
 {
   try
   {
     if(cmdline.isset("claim")) // will go away
-      ::set_properties(goto_functions, cmdline.get_values("claim"));
+      ::set_properties(goto_model, cmdline.get_values("claim"));
 
     if(cmdline.isset("property")) // use this one
-      ::set_properties(goto_functions, cmdline.get_values("property"));
+      ::set_properties(goto_model, cmdline.get_values("property"));
   }
 
   catch(const char *e)
@@ -565,9 +617,7 @@ bool cbmc_parse_optionst::set_properties(goto_functionst &goto_functions)
 }
 
 int cbmc_parse_optionst::get_goto_program(
-  const optionst &options,
-  expr_listt &bmc_constraints, // for get_modules
-  goto_functionst &goto_functions)
+  const optionst &options)
 {
   if(cmdline.args.empty())
   {
@@ -577,127 +627,28 @@ int cbmc_parse_optionst::get_goto_program(
 
   try
   {
-    if(cmdline.isset("show-parse-tree"))
-    {
-      if(cmdline.args.size()!=1 ||
-         is_goto_binary(cmdline.args[0]))
-      {
-        error() << "Please give exactly one source file" << eom;
-        return 6;
-      }
-
-      std::string filename=cmdline.args[0];
-
-      #ifdef _MSC_VER
-      std::ifstream infile(widen(filename));
-      #else
-      std::ifstream infile(filename);
-      #endif
-
-      if(!infile)
-      {
-        error() << "failed to open input file `"
-                << filename << "'" << eom;
-        return 6;
-      }
-
-      std::unique_ptr<languaget> language=get_language_from_filename(filename);
-      language->get_language_options(cmdline);
-
-      if(language==nullptr)
-      {
-        error() << "failed to figure out type of file `"
-                <<  filename << "'" << eom;
-        return 6;
-      }
-
-      language->set_message_handler(get_message_handler());
-
-      status() << "Parsing " << filename << eom;
-
-      if(language->parse(infile, filename))
-      {
-        error() << "PARSING ERROR" << eom;
-        return 6;
-      }
-
-      language->show_parse(std::cout);
-      return 0;
-    }
-
-    cmdlinet::argst binaries;
-    binaries.reserve(cmdline.args.size());
-
-    for(cmdlinet::argst::iterator
-        it=cmdline.args.begin();
-        it!=cmdline.args.end();
-        ) // no ++it
-    {
-      if(is_goto_binary(*it))
-      {
-        binaries.push_back(*it);
-        it=cmdline.args.erase(it);
-        continue;
-      }
-
-      ++it;
-    }
-
-    if(!cmdline.args.empty())
-    {
-      if(parse())
-        return 6;
-      if(typecheck())
-        return 6;
-      int get_modules_ret=get_modules(bmc_constraints);
-      if(get_modules_ret!=-1)
-        return get_modules_ret;
-      if(binaries.empty() && final())
-        return 6;
-
-      // we no longer need any parse trees or language files
-      clear_parse();
-    }
-
-    for(const auto &bin : binaries)
-    {
-      status() << "Reading GOTO program from file " << eom;
-
-      if(read_object_and_link(
-        bin,
-        symbol_table,
-        goto_functions,
-        get_message_handler()))
-      {
-        return 6;
-      }
-    }
+    goto_model=get_goto_model(cmdline, get_message_handler());
 
     if(cmdline.isset("show-symbol-table"))
     {
-      show_symbol_table();
+      show_symbol_table(goto_model, ui_message_handler.get_ui());
       return 0;
     }
 
-    status() << "Generating GOTO Program" << eom;
-
-    goto_convert(symbol_table, goto_functions, ui_message_handler);
-
-    if(process_goto_program(options, goto_functions))
+    if(process_goto_program(options))
       return 6;
 
     // show it?
     if(cmdline.isset("show-loops"))
     {
-      show_loop_ids(get_ui(), goto_functions);
+      show_loop_ids(ui_message_handler.get_ui(), goto_model);
       return 0;
     }
 
     // show it?
     if(cmdline.isset("show-goto-functions"))
     {
-      namespacet ns(symbol_table);
-      show_goto_functions(ns, get_ui(), goto_functions);
+      show_goto_functions(goto_model, ui_message_handler.get_ui());
       return 0;
     }
 
@@ -786,49 +737,44 @@ void cbmc_parse_optionst::preprocessing()
 }
 
 bool cbmc_parse_optionst::process_goto_program(
-  const optionst &options,
-  goto_functionst &goto_functions)
+  const optionst &options)
 {
   try
   {
-    namespacet ns(symbol_table);
-
     // Remove inline assembler; this needs to happen before
     // adding the library.
-    remove_asm(symbol_table, goto_functions);
+    remove_asm(goto_model);
 
     // add the library
-    link_to_library(symbol_table, goto_functions, ui_message_handler);
+    link_to_library(goto_model, get_message_handler());
 
     if(cmdline.isset("string-abstraction"))
-      string_instrumentation(
-        symbol_table, get_message_handler(), goto_functions);
+      string_instrumentation(goto_model, get_message_handler());
 
     // remove function pointers
     status() << "Removal of function pointers and virtual functions" << eom;
     remove_function_pointers(
       get_message_handler(),
-      symbol_table,
-      goto_functions,
+      goto_model,
       cmdline.isset("pointer-check"));
     // Java virtual functions -> explicit dispatch tables:
-    remove_virtual_functions(symbol_table, goto_functions);
+    remove_virtual_functions(goto_model);
     // remove catch and throw (introduces instanceof)
-    remove_exceptions(symbol_table, goto_functions);
+    remove_exceptions(goto_model);
     // Similar removal of RTTI inspection:
-    remove_instanceof(symbol_table, goto_functions);
+    remove_instanceof(goto_model);
 
-    mm_io(symbol_table, goto_functions);
+    mm_io(goto_model);
 
     // do partial inlining
     status() << "Partial Inlining" << eom;
-    goto_partial_inline(goto_functions, ns, ui_message_handler);
+    goto_partial_inline(goto_model, get_message_handler());
 
     // remove returns, gcc vectors, complex
-    remove_returns(symbol_table, goto_functions);
-    remove_vector(symbol_table, goto_functions);
-    remove_complex(symbol_table, goto_functions);
-    rewrite_union(goto_functions, ns);
+    remove_returns(goto_model);
+    remove_vector(goto_model);
+    remove_complex(goto_model);
+    rewrite_union(goto_model);
 
     // Similar removal of java nondet statements:
     // TODO Should really get this from java_bytecode_language somehow, but we
@@ -841,20 +787,21 @@ bool cbmc_parse_optionst::process_goto_program(
       cmdline.isset("java-max-input-tree-depth")
         ? std::stoul(cmdline.get_value("java-max-input-tree-depth"))
         : MAX_NONDET_TREE_DEPTH;
-    replace_java_nondet(goto_functions);
+
+    replace_java_nondet(goto_model);
+
     convert_nondet(
-      goto_functions,
-      symbol_table,
-      ui_message_handler,
+      goto_model,
+      get_message_handler(),
       max_nondet_array_length,
       max_nondet_tree_depth);
 
     // add generic checks
     status() << "Generic Property Instrumentation" << eom;
-    goto_check(ns, options, goto_functions);
+    goto_check(options, goto_model);
 
     // checks don't know about adjusted float expressions
-    adjust_float_expressions(goto_functions, ns);
+    adjust_float_expressions(goto_model);
 
     // ignore default/user-specified initialization
     // of variables with static lifetime
@@ -862,46 +809,44 @@ bool cbmc_parse_optionst::process_goto_program(
     {
       status() << "Adding nondeterministic initialization "
                   "of static/global variables" << eom;
-      nondet_static(ns, goto_functions);
+      nondet_static(goto_model);
     }
 
     if(cmdline.isset("string-abstraction"))
     {
       status() << "String Abstraction" << eom;
       string_abstraction(
-        symbol_table,
-        get_message_handler(),
-        goto_functions);
+        goto_model,
+        get_message_handler());
     }
 
     // add failed symbols
     // needs to be done before pointer analysis
-    add_failed_symbols(symbol_table);
+    add_failed_symbols(goto_model.symbol_table);
 
     // recalculate numbers, etc.
-    goto_functions.update();
+    goto_model.goto_functions.update();
 
     // add loop ids
-    goto_functions.compute_loop_numbers();
+    goto_model.goto_functions.compute_loop_numbers();
 
     if(cmdline.isset("drop-unused-functions"))
     {
       // Entry point will have been set before and function pointers removed
       status() << "Removing unused functions" << eom;
-      remove_unused_functions(goto_functions, ui_message_handler);
+      remove_unused_functions(goto_model, get_message_handler());
     }
 
     // remove skips such that trivial GOTOs are deleted and not considered
     // for coverage annotation:
-    remove_skip(goto_functions);
+    remove_skip(goto_model);
 
     // instrument cover goals
     if(cmdline.isset("cover"))
     {
       if(instrument_cover_goals(
            cmdline,
-           symbol_table,
-           goto_functions,
+           goto_model,
            get_message_handler()))
         return true;
     }
@@ -911,21 +856,21 @@ bool cbmc_parse_optionst::process_goto_program(
     // before using the argument of the "property" option.
     // Do not re-label after using the property slicer because
     // this would cause the property identifiers to change.
-    label_properties(goto_functions);
+    label_properties(goto_model);
 
     // full slice?
     if(cmdline.isset("full-slice"))
     {
       status() << "Performing a full slice" << eom;
       if(cmdline.isset("property"))
-        property_slicer(goto_functions, ns, cmdline.get_values("property"));
+        property_slicer(goto_model, cmdline.get_values("property"));
       else
-        full_slicer(goto_functions, ns);
+        full_slicer(goto_model);
     }
 
     // remove any skips introduced since coverage instrumentation
-    remove_skip(goto_functions);
-    goto_functions.update();
+    remove_skip(goto_model);
+    goto_model.goto_functions.update();
   }
 
   catch(const char *e)
@@ -955,16 +900,14 @@ bool cbmc_parse_optionst::process_goto_program(
 }
 
 /// invoke main modules
-int cbmc_parse_optionst::do_bmc(
-  bmct &bmc,
-  const goto_functionst &goto_functions)
+int cbmc_parse_optionst::do_bmc(bmct &bmc)
 {
-  bmc.set_ui(get_ui());
+  bmc.set_ui(ui_message_handler.get_ui());
 
   int result=6;
 
   // do actual BMC
-  switch(bmc.run(goto_functions))
+  switch(bmc.run(goto_model.goto_functions))
   {
     case safety_checkert::resultt::SAFE:
       result=0;
diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h
index ef91683ee0e..8360951dc54 100644
--- a/src/cbmc/cbmc_parse_options.h
+++ b/src/cbmc/cbmc_parse_options.h
@@ -15,8 +15,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/ui_message.h>
 #include <util/parse_options.h>
 
-#include <langapi/language_ui.h>
-
 #include <analyses/goto_check.h>
 
 #include <java_bytecode/java_bytecode_language.h>
@@ -74,7 +72,7 @@ class optionst;
 class cbmc_parse_optionst:
   public parse_options_baset,
   public xml_interfacet,
-  public language_uit
+  public messaget
 {
 public:
   virtual int doit() override;
@@ -87,35 +85,17 @@ class cbmc_parse_optionst:
     const std::string &extra_options);
 
 protected:
+  goto_modelt goto_model;
   ui_message_handlert ui_message_handler;
-  virtual void register_languages();
-
-  virtual void get_command_line_options(optionst &options);
-
-  virtual int do_bmc(
-    bmct &bmc,
-    const goto_functionst &goto_functions);
-
-  virtual int get_goto_program(
-    const optionst &options,
-    expr_listt &bmc_constraints,
-    goto_functionst &goto_functions);
-
-  virtual bool process_goto_program(
-    const optionst &options,
-    goto_functionst &goto_functions);
-
-  bool set_properties(goto_functionst &goto_functions);
 
   void eval_verbosity();
-
-  // get any additional stuff before finalizing the goto program
-  virtual int get_modules(expr_listt &bmc_constraints)
-  {
-    return -1; // continue
-  }
-
+  void register_languages();
+  void get_command_line_options(optionst &options);
   void preprocessing();
+  int get_goto_program(const optionst &);
+  bool process_goto_program(const optionst &);
+  bool set_properties();
+  int do_bmc(bmct &);
 };
 
 #endif // CPROVER_CBMC_CBMC_PARSE_OPTIONS_H
diff --git a/src/cbmc/cbmc_solvers.h b/src/cbmc/cbmc_solvers.h
index 02bbb8b5db9..2245ff59b70 100644
--- a/src/cbmc/cbmc_solvers.h
+++ b/src/cbmc/cbmc_solvers.h
@@ -17,6 +17,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <memory>
 
 #include <util/options.h>
+#include <util/ui_message.h>
 
 #include <solvers/prop/prop.h>
 #include <solvers/prop/prop_conv.h>
@@ -25,7 +26,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <solvers/prop/aig_prop.h>
 #include <solvers/smt1/smt1_dec.h>
 #include <solvers/smt2/smt2_dec.h>
-#include <langapi/language_ui.h>
 #include <goto-symex/symex_target_equation.h>
 
 #include "bv_cbmc.h"
@@ -123,7 +123,7 @@ class cbmc_solverst:public messaget
   {
   }
 
-  void set_ui(language_uit::uit _ui) { ui=_ui; }
+  void set_ui(ui_message_handlert::uit _ui) { ui=_ui; }
 
 protected:
   const optionst &options;
@@ -131,7 +131,7 @@ class cbmc_solverst:public messaget
   namespacet ns;
 
   // use gui format
-  language_uit::uit ui;
+  ui_message_handlert::uit ui;
 
   std::unique_ptr<solvert> get_default();
   std::unique_ptr<solvert> get_dimacs();
diff --git a/src/cbmc/fault_localization.h b/src/cbmc/fault_localization.h
index 008bb819b1e..dd0227327e6 100644
--- a/src/cbmc/fault_localization.h
+++ b/src/cbmc/fault_localization.h
@@ -15,7 +15,6 @@ Author: Peter Schrammel
 #include <util/namespace.h>
 #include <util/options.h>
 #include <util/threeval.h>
-#include <langapi/language_ui.h>
 
 #include <goto-symex/symex_target_equation.h>
 
diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp
index 66d31053220..6bb726bfaef 100644
--- a/src/goto-analyzer/goto_analyzer_parse_options.cpp
+++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp
@@ -21,7 +21,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <java_bytecode/java_bytecode_language.h>
 #include <jsil/jsil_language.h>
 
-#include <goto-programs/initialize_goto_model.h>
+#include <goto-programs/get_goto_model.h>
 #include <goto-programs/set_properties.h>
 #include <goto-programs/remove_function_pointers.h>
 #include <goto-programs/remove_virtual_functions.h>
@@ -58,7 +58,7 @@ goto_analyzer_parse_optionst::goto_analyzer_parse_optionst(
   int argc,
   const char **argv):
   parse_options_baset(GOTO_ANALYSER_OPTIONS, argc, argv),
-  language_uit(cmdline, ui_message_handler),
+  messaget(ui_message_handler),
   ui_message_handler(cmdline, "GOTO-ANALYZER " CBMC_VERSION)
 {
 }
@@ -160,8 +160,14 @@ int goto_analyzer_parse_optionst::doit()
 
   register_languages();
 
-  if(initialize_goto_model(goto_model, cmdline, get_message_handler()))
+  try
+  {
+    goto_model=get_goto_model(cmdline, get_message_handler());
+  }
+  catch(...)
+  {
     return 6;
+  }
 
   if(process_goto_program(options))
     return 6;
diff --git a/src/goto-analyzer/goto_analyzer_parse_options.h b/src/goto-analyzer/goto_analyzer_parse_options.h
index 5d61256b1f2..3fbaab18b1b 100644
--- a/src/goto-analyzer/goto_analyzer_parse_options.h
+++ b/src/goto-analyzer/goto_analyzer_parse_options.h
@@ -15,8 +15,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/ui_message.h>
 #include <util/parse_options.h>
 
-#include <langapi/language_ui.h>
-
 #include <goto-programs/goto_model.h>
 #include <goto-programs/show_goto_functions.h>
 
@@ -52,7 +50,7 @@ class optionst;
 
 class goto_analyzer_parse_optionst:
   public parse_options_baset,
-  public language_uit
+  public messaget
 {
 public:
   virtual int doit() override;
@@ -72,6 +70,11 @@ class goto_analyzer_parse_optionst:
   bool set_properties();
 
   void eval_verbosity();
+
+  ui_message_handlert::uit get_ui()
+  {
+    return ui_message_handler.get_ui();
+  }
 };
 
 #endif // CPROVER_GOTO_ANALYZER_GOTO_ANALYZER_PARSE_OPTIONS_H
diff --git a/src/goto-cc/gcc_mode.h b/src/goto-cc/gcc_mode.h
index cd4f1cb1a56..d5b1e9627cd 100644
--- a/src/goto-cc/gcc_mode.h
+++ b/src/goto-cc/gcc_mode.h
@@ -18,6 +18,8 @@ Date: June 2006
 
 #include "goto_cc_mode.h"
 
+#include <set>
+
 class gcc_modet:public goto_cc_modet
 {
 public:
diff --git a/src/goto-cc/goto_cc_mode.h b/src/goto-cc/goto_cc_mode.h
index a0b6ea47a96..6dbad84d3ce 100644
--- a/src/goto-cc/goto_cc_mode.h
+++ b/src/goto-cc/goto_cc_mode.h
@@ -14,10 +14,10 @@ Date: June 2006
 #ifndef CPROVER_GOTO_CC_GOTO_CC_MODE_H
 #define CPROVER_GOTO_CC_GOTO_CC_MODE_H
 
-#include <langapi/language_ui.h>
-
 #include "goto_cc_cmdline.h"
 
+#include <util/message.h>
+
 class goto_cc_modet:public messaget
 {
 public:
diff --git a/src/goto-diff/goto_diff.h b/src/goto-diff/goto_diff.h
index 2b6a9ac923d..23a65221358 100644
--- a/src/goto-diff/goto_diff.h
+++ b/src/goto-diff/goto_diff.h
@@ -13,9 +13,9 @@ Author: Peter Schrammel
 #define CPROVER_GOTO_DIFF_GOTO_DIFF_H
 
 #include <goto-programs/goto_model.h>
-#include <langapi/language_ui.h>
-#include <util/message.h>
+
 #include <util/json.h>
+#include <util/ui_message.h>
 
 #include <ostream>
 
@@ -37,14 +37,14 @@ class goto_difft:public messaget
 
   virtual bool operator()()=0;
 
-  void set_ui(language_uit::uit _ui) { ui=_ui; }
+  void set_ui(ui_message_handlert::uit _ui) { ui=_ui; }
 
   virtual std::ostream &output_functions(std::ostream &out) const;
 
 protected:
   const goto_modelt &goto_model1;
   const goto_modelt &goto_model2;
-  language_uit::uit ui;
+  ui_message_handlert::uit ui;
 
   unsigned total_functions_count;
   typedef std::set<irep_idt> irep_id_sett;
diff --git a/src/goto-diff/goto_diff_parse_options.h b/src/goto-diff/goto_diff_parse_options.h
index 505de8410f4..a79cd064706 100644
--- a/src/goto-diff/goto_diff_parse_options.h
+++ b/src/goto-diff/goto_diff_parse_options.h
@@ -15,8 +15,6 @@ Author: Peter Schrammel
 #include <util/ui_message.h>
 #include <util/parse_options.h>
 
-#include <langapi/language_ui.h>
-
 #include <goto-programs/goto_model.h>
 #include <goto-programs/show_goto_functions.h>
 
diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp
index 8991ab985d3..ae8a339cdbb 100644
--- a/src/goto-instrument/goto_instrument_parse_options.cpp
+++ b/src/goto-instrument/goto_instrument_parse_options.cpp
@@ -41,6 +41,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <goto-programs/remove_unused_functions.h>
 #include <goto-programs/parameter_assignments.h>
 #include <goto-programs/slice_global_inits.h>
+#include <goto-programs/show_symbol_table.h>
 
 #include <pointer-analysis/value_set_analysis.h>
 #include <pointer-analysis/goto_program_dereference.h>
@@ -476,7 +477,7 @@ int goto_instrument_parse_optionst::doit()
 
     if(cmdline.isset("show-symbol-table"))
     {
-      show_symbol_table();
+      show_symbol_table(symbol_table, get_ui());
       return 0;
     }
 
@@ -527,7 +528,7 @@ int goto_instrument_parse_optionst::doit()
 
     if(cmdline.isset("list-symbols"))
     {
-      show_symbol_table(true);
+      show_symbol_table(symbol_table, get_ui());
       return 0;
     }
 
diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h
index e2c4bf4fbc0..daee4657647 100644
--- a/src/goto-instrument/goto_instrument_parse_options.h
+++ b/src/goto-instrument/goto_instrument_parse_options.h
@@ -15,7 +15,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/ui_message.h>
 #include <util/parse_options.h>
 
-#include <langapi/language_ui.h>
 #include <goto-programs/goto_functions.h>
 #include <goto-programs/show_goto_functions.h>
 #include <goto-programs/remove_const_function_pointers.h>
@@ -81,7 +80,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 class goto_instrument_parse_optionst:
   public parse_options_baset,
-  public language_uit
+  public messaget
 {
 public:
   virtual int doit();
@@ -89,7 +88,7 @@ class goto_instrument_parse_optionst:
 
   goto_instrument_parse_optionst(int argc, const char **argv):
     parse_options_baset(GOTO_INSTRUMENT_OPTIONS, argc, argv),
-    language_uit(cmdline, ui_message_handler),
+    messaget(ui_message_handler),
     ui_message_handler(cmdline, "goto-instrument"),
     function_pointer_removal_done(false),
     partial_inlining_done(false),
@@ -115,7 +114,13 @@ class goto_instrument_parse_optionst:
   bool partial_inlining_done;
   bool remove_returns_done;
 
+  symbol_tablet symbol_table;
   goto_functionst goto_functions;
+
+  ui_message_handlert::uit get_ui()
+  {
+    return ui_message_handler.get_ui();
+  }
 };
 
 #endif // CPROVER_GOTO_INSTRUMENT_GOTO_INSTRUMENT_PARSE_OPTIONS_H
diff --git a/src/goto-programs/Makefile b/src/goto-programs/Makefile
index b164beef079..2166838dbe9 100644
--- a/src/goto-programs/Makefile
+++ b/src/goto-programs/Makefile
@@ -7,7 +7,7 @@ SRC = basic_blocks.cpp \
       destructor.cpp \
       elf_reader.cpp \
       format_strings.cpp \
-      initialize_goto_model.cpp \
+      get_goto_model.cpp \
       goto_asm.cpp \
       goto_clean_expr.cpp \
       goto_convert.cpp \
diff --git a/src/goto-programs/get_goto_model.cpp b/src/goto-programs/get_goto_model.cpp
new file mode 100644
index 00000000000..21946d2f6b8
--- /dev/null
+++ b/src/goto-programs/get_goto_model.cpp
@@ -0,0 +1,150 @@
+/*******************************************************************\
+
+Module:
+
+Author: Daniel Kroening, kroening@cs.cmu.edu
+
+\*******************************************************************/
+
+#include "get_goto_model.h"
+
+#include <fstream>
+
+#include <util/message.h>
+#include <util/cmdline.h>
+#include <util/language_file.h>
+#include <util/language.h>
+
+#include <langapi/mode.h>
+
+#include "read_goto_binary.h"
+#include "goto_model.h"
+#include "link_goto_model.h"
+#include "goto_convert_functions.h"
+
+static symbol_tablet get_source(
+  const cmdlinet &cmdline,
+  const std::string &filename,
+  message_handlert &message_handler)
+{
+  messaget message(message_handler);
+
+  std::unique_ptr<languaget> 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;
+    throw 0;
+  }
+
+  language->set_message_handler(message_handler);
+  language->get_language_options(cmdline);
+
+  #ifdef _MSC_VER
+  std::ifstream infile(widen(filename));
+  #else
+  std::ifstream infile(filename);
+  #endif
+
+  if(!infile)
+  {
+    message.error() << "failed to open input file `"
+                    << filename << "'" << messaget::eom;
+    throw 0;
+  }
+
+  message.status() << "Parsing " << filename << messaget::eom;
+
+  if(language->parse(infile, filename))
+  {
+    message.error() << "PARSING ERROR" << messaget::eom;
+    throw 0;
+  }
+
+  message.status() << "Converting" << messaget::eom;
+
+  symbol_tablet symbol_table;
+  if(language->typecheck(symbol_table, ""))
+  {
+    message.error() << "CONVERSION ERROR" << messaget::eom;
+    throw 0;
+  }
+
+  return symbol_table;
+}
+
+void add_entry_point(
+  const cmdlinet &cmdline,
+  goto_modelt &goto_model,
+  message_handlert &message_handler)
+{
+  std::set<irep_idt> modes;
+
+  for(const auto &it : goto_model.symbol_table.symbols)
+    if(!it.second.mode.empty())
+      modes.insert(it.second.mode);
+
+  if(modes.empty())
+    return;
+
+  irep_idt final_mode=*modes.begin();
+
+  std::unique_ptr<languaget> language(
+    get_language_from_mode(final_mode));
+
+  if(language==nullptr)
+    return;
+
+  language->set_message_handler(message_handler);
+  language->get_language_options(cmdline);
+  language->final(goto_model.symbol_table);
+
+  // The above may have generated further function bodies,
+  // which need to be converted.
+  goto_convert(goto_model, message_handler);
+}
+
+goto_modelt get_goto_model(
+  const cmdlinet &cmdline,
+  message_handlert &message_handler)
+{
+  messaget message(message_handler);
+
+  if(cmdline.args.empty())
+  {
+    message.error() << "Please provide a program" << messaget::eom;
+    throw 0;
+  }
+
+  goto_modelt goto_model;
+
+  // categorize
+  for(const auto &filename : cmdline.args)
+  {
+    goto_modelt tmp_model;
+
+    if(is_goto_binary(filename))
+    {
+      if(read_goto_binary(filename, tmp_model, message_handler))
+        throw 0;
+    }
+    else
+    {
+      tmp_model.symbol_table=
+        get_source(cmdline, filename, message_handler);
+      goto_convert(tmp_model, message_handler);
+    }
+
+    // now link together
+    link_goto_model(goto_model, tmp_model, message_handler);
+  }
+
+  // generate entry point
+  add_entry_point(cmdline, goto_model, message_handler);
+
+  return goto_model;
+}
diff --git a/src/goto-programs/get_goto_model.h b/src/goto-programs/get_goto_model.h
new file mode 100644
index 00000000000..93526f051fa
--- /dev/null
+++ b/src/goto-programs/get_goto_model.h
@@ -0,0 +1,20 @@
+/*******************************************************************\
+
+Module:
+
+Author: Daniel Kroening, kroening@cs.cmu.edu
+
+\*******************************************************************/
+
+#ifndef CPROVER_GOTO_PROGRAMS_GET_GOTO_MODEL_H
+#define CPROVER_GOTO_PROGRAMS_GET_GOTO_MODEL_H
+
+class cmdlinet;
+class message_handlert;
+class goto_modelt;
+
+goto_modelt get_goto_model(
+  const cmdlinet &,
+  message_handlert &);
+
+#endif
diff --git a/src/goto-programs/goto_convert_functions.cpp b/src/goto-programs/goto_convert_functions.cpp
index 5a35d5e2ef7..58d03a16cef 100644
--- a/src/goto-programs/goto_convert_functions.cpp
+++ b/src/goto-programs/goto_convert_functions.cpp
@@ -221,15 +221,6 @@ void goto_convert_functionst::convert_function(const irep_idt &identifier)
     f.make_hidden();
 }
 
-void goto_convert(
-  symbol_tablet &symbol_table,
-  goto_modelt &goto_model,
-  message_handlert &message_handler)
-{
-  goto_convert(symbol_table, goto_model.goto_functions, message_handler);
-  goto_model.symbol_table.swap(symbol_table);
-}
-
 void goto_convert(
   goto_modelt &goto_model,
   message_handlert &message_handler)
diff --git a/src/goto-programs/goto_convert_functions.h b/src/goto-programs/goto_convert_functions.h
index 85de9a67b97..3162b453d0f 100644
--- a/src/goto-programs/goto_convert_functions.h
+++ b/src/goto-programs/goto_convert_functions.h
@@ -23,12 +23,6 @@ void goto_convert(
   goto_functionst &functions,
   message_handlert &);
 
-// confusing, will go away
-void goto_convert(
-  symbol_tablet &symbol_table,
-  goto_modelt &dest,
-  message_handlert &);
-
 // convert it all!
 void goto_convert(
   goto_modelt &,
diff --git a/src/goto-programs/initialize_goto_model.cpp b/src/goto-programs/initialize_goto_model.cpp
deleted file mode 100644
index 34a2a46a895..00000000000
--- a/src/goto-programs/initialize_goto_model.cpp
+++ /dev/null
@@ -1,162 +0,0 @@
-/*******************************************************************\
-
-Module: Get a Goto Program
-
-Author: Daniel Kroening, kroening@kroening.com
-
-\*******************************************************************/
-
-/// \file
-/// Get a Goto Program
-
-#include "initialize_goto_model.h"
-
-#include <fstream>
-#include <iostream>
-
-#include <util/language.h>
-#include <util/config.h>
-#include <util/unicode.h>
-
-#include <langapi/mode.h>
-#include <langapi/language_ui.h>
-
-#include "goto_convert_functions.h"
-#include "read_goto_binary.h"
-
-bool initialize_goto_model(
-  goto_modelt &goto_model,
-  const cmdlinet &cmdline,
-  message_handlert &message_handler)
-{
-  messaget msg(message_handler);
-  const std::vector<std::string> &files=cmdline.args;
-  if(files.empty())
-  {
-    msg.error() << "Please provide a program" << messaget::eom;
-    return true;
-  }
-
-  try
-  {
-    std::vector<std::string> binaries, sources;
-    binaries.reserve(files.size());
-    sources.reserve(files.size());
-
-    for(const auto &file : files)
-    {
-      if(is_goto_binary(file))
-        binaries.push_back(file);
-      else
-        sources.push_back(file);
-    }
-
-    if(!sources.empty())
-    {
-      language_filest language_files;
-
-      language_files.set_message_handler(message_handler);
-
-      for(const auto &filename : sources)
-      {
-        #ifdef _MSC_VER
-        std::ifstream infile(widen(filename));
-        #else
-        std::ifstream infile(filename);
-        #endif
-
-        if(!infile)
-        {
-          msg.error() << "failed to open input file `" << filename
-            << '\'' << messaget::eom;
-          return true;
-        }
-
-        std::pair<language_filest::file_mapt::iterator, bool>
-          result=language_files.file_map.insert(
-            std::pair<std::string, language_filet>(filename, language_filet()));
-
-        language_filet &lf=result.first->second;
-
-        lf.filename=filename;
-        lf.language=get_language_from_filename(filename);
-
-        if(lf.language==nullptr)
-        {
-          source_locationt location;
-          location.set_file(filename);
-          msg.error().source_location=location;
-          msg.error() << "failed to figure out type of file" << messaget::eom;
-          return true;
-        }
-
-        languaget &language=*lf.language;
-        language.set_message_handler(message_handler);
-        language.get_language_options(cmdline);
-
-        msg.status() << "Parsing " << filename << messaget::eom;
-
-        if(language.parse(infile, filename))
-        {
-          msg.error() << "PARSING ERROR" << messaget::eom;
-          return true;
-        }
-
-        lf.get_modules();
-      }
-
-      msg.status() << "Converting" << messaget::eom;
-
-      if(language_files.typecheck(goto_model.symbol_table))
-      {
-        msg.error() << "CONVERSION ERROR" << messaget::eom;
-        return true;
-      }
-
-      if(binaries.empty())
-      {
-        if(language_files.final(goto_model.symbol_table))
-        {
-          msg.error() << "CONVERSION ERROR" << messaget::eom;
-          return true;
-        }
-      }
-    }
-
-    for(const auto &file : binaries)
-    {
-      msg.status() << "Reading GOTO program from file" << messaget::eom;
-
-      if(read_object_and_link(file, goto_model, message_handler))
-        return true;
-    }
-
-    msg.status() << "Generating GOTO Program" << messaget::eom;
-
-    goto_convert(
-      goto_model.symbol_table,
-      goto_model.goto_functions,
-      message_handler);
-  }
-  catch(const char *e)
-  {
-    msg.error() << e << messaget::eom;
-    return true;
-  }
-  catch(const std::string e)
-  {
-    msg.error() << e << messaget::eom;
-    return true;
-  }
-  catch(int)
-  {
-    return true;
-  }
-  catch(std::bad_alloc)
-  {
-    msg.error() << "Out of memory" << messaget::eom;
-    return true;
-  }
-
-  return false; // no error
-}
diff --git a/src/goto-programs/initialize_goto_model.h b/src/goto-programs/initialize_goto_model.h
deleted file mode 100644
index 9aa1c8ef126..00000000000
--- a/src/goto-programs/initialize_goto_model.h
+++ /dev/null
@@ -1,25 +0,0 @@
-/*******************************************************************\
-
-Module: Initialize a Goto Program
-
-Author: Daniel Kroening, kroening@kroening.com
-
-\*******************************************************************/
-
-/// \file
-/// Initialize a Goto Program
-
-#ifndef CPROVER_GOTO_PROGRAMS_INITIALIZE_GOTO_MODEL_H
-#define CPROVER_GOTO_PROGRAMS_INITIALIZE_GOTO_MODEL_H
-
-#include <util/message.h>
-#include <util/cmdline.h>
-
-#include "goto_model.h"
-
-bool initialize_goto_model(
-  goto_modelt &goto_model,
-  const cmdlinet &cmdline,
-  message_handlert &message_handler);
-
-#endif // CPROVER_GOTO_PROGRAMS_INITIALIZE_GOTO_MODEL_H
diff --git a/src/goto-programs/read_goto_binary.cpp b/src/goto-programs/read_goto_binary.cpp
index 2b4a3805401..9e7a1968ccc 100644
--- a/src/goto-programs/read_goto_binary.cpp
+++ b/src/goto-programs/read_goto_binary.cpp
@@ -30,8 +30,6 @@ Module: Read Goto Programs
 #include <util/base_type.h>
 #include <util/config.h>
 
-#include <langapi/language_ui.h>
-
 #include "goto_model.h"
 #include "link_goto_model.h"
 #include "read_bin_goto_object.h"
diff --git a/src/goto-programs/show_symbol_table.cpp b/src/goto-programs/show_symbol_table.cpp
index eebb63dcfcd..b4230f9086b 100644
--- a/src/goto-programs/show_symbol_table.cpp
+++ b/src/goto-programs/show_symbol_table.cpp
@@ -23,8 +23,44 @@ void show_symbol_table_xml_ui()
 {
 }
 
+void show_symbol_table_brief_plain(
+  const symbol_tablet &symbol_table,
+  std::ostream &out)
+{
+  // we want to sort alphabetically
+  std::set<std::string> symbols;
+
+  forall_symbols(it, symbol_table.symbols)
+    symbols.insert(id2string(it->first));
+
+  const namespacet ns(symbol_table);
+
+  for(const std::string &id : symbols)
+  {
+    const symbolt &symbol=ns.lookup(id);
+
+    std::unique_ptr<languaget> ptr;
+
+    if(symbol.mode=="")
+      ptr=get_default_language();
+    else
+    {
+      ptr=get_language_from_mode(symbol.mode);
+      if(ptr==nullptr)
+        throw "symbol "+id2string(symbol.name)+" has unknown mode";
+    }
+
+    std::string type_str;
+
+    if(symbol.type.is_not_nil())
+      ptr->from_type(symbol.type, type_str, ns);
+
+    out << symbol.name << " " << type_str << '\n';
+  }
+}
+
 void show_symbol_table_plain(
-  const goto_modelt &goto_model,
+  const symbol_tablet &symbol_table,
   std::ostream &out)
 {
   out << '\n' << "Symbols:" << '\n' << '\n';
@@ -32,10 +68,10 @@ void show_symbol_table_plain(
   // we want to sort alphabetically
   std::set<std::string> symbols;
 
-  forall_symbols(it, goto_model.symbol_table.symbols)
+  forall_symbols(it, symbol_table.symbols)
     symbols.insert(id2string(it->first));
 
-  const namespacet ns(goto_model.symbol_table);
+  const namespacet ns(symbol_table);
 
   for(const std::string &id : symbols)
   {
@@ -112,14 +148,40 @@ void show_symbol_table_plain(
   }
 }
 
+void show_symbol_table(
+  const symbol_tablet &symbol_table,
+  ui_message_handlert::uit ui)
+{
+  switch(ui)
+  {
+  case ui_message_handlert::uit::PLAIN:
+    show_symbol_table_plain(symbol_table, std::cout);
+    break;
+
+  case ui_message_handlert::uit::XML_UI:
+    show_symbol_table_xml_ui();
+    break;
+
+  default:
+    break;
+  }
+}
+
 void show_symbol_table(
   const goto_modelt &goto_model,
   ui_message_handlert::uit ui)
+{
+  show_symbol_table(goto_model.symbol_table, ui);
+}
+
+void show_symbol_table_brief(
+  const symbol_tablet &symbol_table,
+  ui_message_handlert::uit ui)
 {
   switch(ui)
   {
   case ui_message_handlert::uit::PLAIN:
-    show_symbol_table_plain(goto_model, std::cout);
+    show_symbol_table_brief_plain(symbol_table, std::cout);
     break;
 
   case ui_message_handlert::uit::XML_UI:
@@ -130,3 +192,10 @@ void show_symbol_table(
     break;
   }
 }
+
+void show_symbol_table_brief(
+  const goto_modelt &goto_model,
+  ui_message_handlert::uit ui)
+{
+  show_symbol_table_brief(goto_model.symbol_table, ui);
+}
diff --git a/src/goto-programs/show_symbol_table.h b/src/goto-programs/show_symbol_table.h
index 5ad717e7049..82e49128967 100644
--- a/src/goto-programs/show_symbol_table.h
+++ b/src/goto-programs/show_symbol_table.h
@@ -14,9 +14,22 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/ui_message.h>
 
+class symbol_tablet;
 class goto_modelt;
 
 void show_symbol_table(
+  const symbol_tablet &,
+  ui_message_handlert::uit ui);
+
+void show_symbol_table_brief(
+  const symbol_tablet &,
+  ui_message_handlert::uit ui);
+
+void show_symbol_table(
+  const goto_modelt &,
+  ui_message_handlert::uit ui);
+
+void show_symbol_table_brief(
   const goto_modelt &,
   ui_message_handlert::uit ui);
 
diff --git a/src/java_bytecode/ci_lazy_methods.cpp b/src/java_bytecode/ci_lazy_methods.cpp
index 41eab823e42..1365c14bbb8 100644
--- a/src/java_bytecode/ci_lazy_methods.cpp
+++ b/src/java_bytecode/ci_lazy_methods.cpp
@@ -61,7 +61,8 @@ bool ci_lazy_methodst::operator()(
   std::vector<irep_idt> method_worklist2;
 
   auto main_function=
-    get_main_symbol(symbol_table, main_class, get_message_handler(), true);
+    get_main_symbol(symbol_table, get_message_handler(), true);
+
   if(main_function.stop_convert)
   {
     // Failed, mark all functions in the given main class(es)
diff --git a/src/java_bytecode/java_bytecode_language.cpp b/src/java_bytecode/java_bytecode_language.cpp
index f966600b38b..74f63ca7787 100644
--- a/src/java_bytecode/java_bytecode_language.cpp
+++ b/src/java_bytecode/java_bytecode_language.cpp
@@ -236,6 +236,18 @@ bool java_bytecode_languaget::typecheck(
        symbol_table, get_message_handler(), string_refinement_enabled))
     return true;
 
+  // remember the main class, if any
+  if(!main_class.empty())
+  {
+    symbolt main_class_symbol;
+    main_class_symbol.name="java_main_class";
+    main_class_symbol.base_name=main_class_symbol.name;
+    main_class_symbol.value.id(ID_string_constant);
+    main_class_symbol.value.set(ID_value, main_class);
+    main_class_symbol.mode=ID_java;
+    symbol_table.move(main_class_symbol);
+  }
+
   return false;
 }
 
@@ -368,7 +380,7 @@ bool java_bytecode_languaget::final(symbol_tablet &symbol_table)
   replace_string_methods(symbol_table);
 
   main_function_resultt res=
-    get_main_symbol(symbol_table, main_class, get_message_handler());
+    get_main_symbol(symbol_table, get_message_handler());
   if(res.stop_convert)
     return res.error_found;
 
@@ -376,7 +388,6 @@ bool java_bytecode_languaget::final(symbol_tablet &symbol_table)
   return
     java_entry_point(
       symbol_table,
-      main_class,
       get_message_handler(),
       assume_inputs_non_null,
       max_nondet_array_length,
diff --git a/src/java_bytecode/java_entry_point.cpp b/src/java_bytecode/java_entry_point.cpp
index c142f37ddf5..5d6516f10f2 100644
--- a/src/java_bytecode/java_entry_point.cpp
+++ b/src/java_bytecode/java_entry_point.cpp
@@ -322,7 +322,6 @@ void java_record_outputs(
 
 main_function_resultt get_main_symbol(
   symbol_tablet &symbol_table,
-  const irep_idt &main_class,
   message_handlert &message_handler,
   bool allow_no_body)
 {
@@ -362,7 +361,7 @@ main_function_resultt get_main_symbol(
     // check if it has a body
     if(symbol.value.is_nil() && !allow_no_body)
     {
-      message.error() << "main method `" << main_class
+      message.error() << "main method `" << symbol.display_name()
                       << "' has no body" << messaget::eom;
       res.main_function=symbol;
       res.error_found=true;
@@ -375,8 +374,11 @@ main_function_resultt get_main_symbol(
     // no function given, we look for the main class
     assert(config.main=="");
 
+    symbol_tablet::symbolst::const_iterator s_it=
+      symbol_table.symbols.find("java_main_class");
+
     // are we given a main class?
-    if(main_class.empty())
+    if(s_it==symbol_table.symbols.end())
     {
       res.main_function=symbol;
       res.error_found=false;
@@ -384,6 +386,8 @@ main_function_resultt get_main_symbol(
       return res; // silently ignore
     }
 
+    irep_idt main_class=s_it->second.value.get(ID_value);
+
     std::string entry_method=
       id2string(main_class)+".main";
 
@@ -478,7 +482,6 @@ main_function_resultt get_main_symbol(
 /// \returns true if error occurred on entry point search
 bool java_entry_point(
   symbol_tablet &symbol_table,
-  const irep_idt &main_class,
   message_handlert &message_handler,
   bool assume_init_pointers_not_null,
   size_t max_nondet_array_length,
@@ -492,7 +495,7 @@ bool java_entry_point(
 
   messaget message(message_handler);
   main_function_resultt res=
-    get_main_symbol(symbol_table, main_class, message_handler);
+    get_main_symbol(symbol_table, message_handler);
   if(res.stop_convert)
     return res.stop_convert;
   symbolt symbol=res.main_function;
diff --git a/src/java_bytecode/java_entry_point.h b/src/java_bytecode/java_entry_point.h
index 18e42aafc65..f9757c3f689 100644
--- a/src/java_bytecode/java_entry_point.h
+++ b/src/java_bytecode/java_entry_point.h
@@ -19,7 +19,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 bool java_entry_point(
   class symbol_tablet &symbol_table,
-  const irep_idt &main_class,
   class message_handlert &message_handler,
   bool assume_init_pointers_not_null,
   size_t max_nondet_array_length,
@@ -36,7 +35,6 @@ typedef struct
 /// Figures out the entry point of the code to verify
 main_function_resultt get_main_symbol(
   symbol_tablet &symbol_table,
-  const irep_idt &main_class,
   message_handlert &,
   bool allow_no_body=false);
 
diff --git a/src/solvers/refinement/bv_refinement.h b/src/solvers/refinement/bv_refinement.h
index d1e72e227b3..a3f6207f5dc 100644
--- a/src/solvers/refinement/bv_refinement.h
+++ b/src/solvers/refinement/bv_refinement.h
@@ -12,7 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_SOLVERS_REFINEMENT_BV_REFINEMENT_H
 #define CPROVER_SOLVERS_REFINEMENT_BV_REFINEMENT_H
 
-#include <langapi/language_ui.h>
+#include <util/ui_message.h>
 
 #include <solvers/flattening/bv_pointers.h>
 
@@ -42,7 +42,7 @@ class bv_refinementt:public bv_pointerst
 
   using bv_pointerst::is_in_conflict;
 
-  void set_ui(language_uit::uit _ui) { ui=_ui; }
+  void set_ui(ui_message_handlert::uit _ui) { ui=_ui; }
 
 protected:
   resultt prop_solve();
@@ -113,7 +113,7 @@ class bv_refinementt:public bv_pointerst
   bvt parent_assumptions;
 
   // use gui format
-  language_uit::uit ui;
+  ui_message_handlert::uit ui;
 };
 
 #endif // CPROVER_SOLVERS_REFINEMENT_BV_REFINEMENT_H
diff --git a/src/solvers/refinement/string_constraint.h b/src/solvers/refinement/string_constraint.h
index 867284101e3..3d5121d472d 100644
--- a/src/solvers/refinement/string_constraint.h
+++ b/src/solvers/refinement/string_constraint.h
@@ -20,7 +20,6 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com
 #ifndef CPROVER_SOLVERS_REFINEMENT_STRING_CONSTRAINT_H
 #define CPROVER_SOLVERS_REFINEMENT_STRING_CONSTRAINT_H
 
-#include <langapi/language_ui.h>
 #include <solvers/refinement/bv_refinement.h>
 #include <solvers/refinement/string_refinement_invariant.h>
 #include <util/refined_string_type.h>
diff --git a/src/symex/symex_parse_options.cpp b/src/symex/symex_parse_options.cpp
index f2da45da76c..581771747fd 100644
--- a/src/symex/symex_parse_options.cpp
+++ b/src/symex/symex_parse_options.cpp
@@ -26,7 +26,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <cpp/cpp_language.h>
 #include <java_bytecode/java_bytecode_language.h>
 
-#include <goto-programs/initialize_goto_model.h>
+#include <goto-programs/get_goto_model.h>
 #include <goto-programs/goto_convert_functions.h>
 #include <goto-programs/show_properties.h>
 #include <goto-programs/set_properties.h>
@@ -59,7 +59,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 symex_parse_optionst::symex_parse_optionst(int argc, const char **argv):
   parse_options_baset(SYMEX_OPTIONS, argc, argv),
-  language_uit(cmdline, ui_message_handler),
+  messaget(ui_message_handler),
   ui_message_handler(cmdline, "Symex " CBMC_VERSION)
 {
 }
@@ -137,8 +137,14 @@ int symex_parse_optionst::doit()
 
   eval_verbosity();
 
-  if(initialize_goto_model(goto_model, cmdline, get_message_handler()))
+  try
+  {
+    goto_model=get_goto_model(cmdline, get_message_handler());
+  }
+  catch(...)
+  {
     return 6;
+  }
 
   if(process_goto_program(options))
     return 6;
@@ -341,41 +347,15 @@ bool symex_parse_optionst::process_goto_program(const optionst &options)
 
     if(cmdline.isset("cover"))
     {
-      std::string criterion=cmdline.get_value("cover");
-
-      coverage_criteriont c;
-
-      if(criterion=="assertion" || criterion=="assertions")
-        c=coverage_criteriont::ASSERTION;
-      else if(criterion=="path" || criterion=="paths")
-        c=coverage_criteriont::PATH;
-      else if(criterion=="branch" || criterion=="branches")
-        c=coverage_criteriont::BRANCH;
-      else if(criterion=="location" || criterion=="locations")
-        c=coverage_criteriont::LOCATION;
-      else if(criterion=="decision" || criterion=="decisions")
-        c=coverage_criteriont::DECISION;
-      else if(criterion=="condition" || criterion=="conditions")
-        c=coverage_criteriont::CONDITION;
-      else if(criterion=="mcdc")
-        c=coverage_criteriont::MCDC;
-      else if(criterion=="cover")
-        c=coverage_criteriont::COVER;
-      else
-      {
-        error() << "unknown coverage criterion" << eom;
-        return true;
-      }
-
       status() << "Instrumenting coverage goals" << eom;
-      instrument_cover_goals(symbol_table, goto_model.goto_functions, c);
-      goto_model.goto_functions.update();
+      if(instrument_cover_goals(cmdline, goto_model, get_message_handler()))
+        return true;
     }
 
     // show it?
     if(cmdline.isset("show-loops"))
     {
-      show_loop_ids(get_ui(), goto_model.goto_functions);
+      show_loop_ids(get_ui(), goto_model);
       return true;
     }
 
diff --git a/src/symex/symex_parse_options.h b/src/symex/symex_parse_options.h
index 7278cbf1261..a3fb841f20b 100644
--- a/src/symex/symex_parse_options.h
+++ b/src/symex/symex_parse_options.h
@@ -18,8 +18,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <goto-programs/goto_model.h>
 #include <goto-programs/show_goto_functions.h>
 
-#include <langapi/language_ui.h>
-
 #include <analyses/goto_check.h>
 
 #include <java_bytecode/java_bytecode_language.h>
@@ -55,7 +53,7 @@ class optionst;
 
 class symex_parse_optionst:
   public parse_options_baset,
-  public language_uit
+  public messaget
 {
 public:
   virtual int doit();
@@ -80,6 +78,11 @@ class symex_parse_optionst:
   void eval_verbosity();
 
   std::string get_test(const goto_tracet &goto_trace);
+
+  ui_message_handlert::uit get_ui() const
+  {
+    return ui_message_handler.get_ui();
+  }
 };
 
 #endif // CPROVER_SYMEX_SYMEX_PARSE_OPTIONS_H