diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
index 265759fc698..886298304f6 100644
--- a/src/cbmc/cbmc_parse_options.cpp
+++ b/src/cbmc/cbmc_parse_options.cpp
@@ -633,9 +633,10 @@ int cbmc_parse_optionst::get_goto_program(
     {
       const std::string &function_id=cmdline.get_value("function");
       rebuild_goto_start_functiont start_function_rebuilder(
-        get_message_handler(),
-        goto_model.symbol_table,
-        goto_model.goto_functions);
+          get_message_handler(),
+          cmdline,
+          goto_model.symbol_table,
+          goto_model.goto_functions);
 
       if(start_function_rebuilder(function_id))
       {
diff --git a/src/goto-programs/initialize_goto_model.cpp b/src/goto-programs/initialize_goto_model.cpp
index 753dff36edb..41e9bce9371 100644
--- a/src/goto-programs/initialize_goto_model.cpp
+++ b/src/goto-programs/initialize_goto_model.cpp
@@ -138,6 +138,7 @@ bool initialize_goto_model(
       const std::string &function_id=cmdline.get_value("function");
       rebuild_goto_start_functiont start_function_rebuilder(
         msg.get_message_handler(),
+        cmdline,
         goto_model.symbol_table,
         goto_model.goto_functions);
 
diff --git a/src/goto-programs/rebuild_goto_start_function.cpp b/src/goto-programs/rebuild_goto_start_function.cpp
index 0949c1da73f..cb4d9e01f3d 100644
--- a/src/goto-programs/rebuild_goto_start_function.cpp
+++ b/src/goto-programs/rebuild_goto_start_function.cpp
@@ -13,6 +13,7 @@
 #include <util/symbol.h>
 #include <util/symbol_table.h>
 #include <util/prefix.h>
+#include <util/cmdline.h>
 #include <langapi/mode.h>
 #include <memory>
 
@@ -25,11 +26,13 @@
 ///   body of the _start function).
 rebuild_goto_start_functiont::rebuild_goto_start_functiont(
   message_handlert &_message_handler,
+  const cmdlinet &cmdline,
   symbol_tablet &symbol_table,
   goto_functionst &goto_functions):
-  messaget(_message_handler),
-  symbol_table(symbol_table),
-  goto_functions(goto_functions)
+    messaget(_message_handler),
+    cmdline(cmdline),
+    symbol_table(symbol_table),
+    goto_functions(goto_functions)
 {
 }
 
@@ -50,6 +53,7 @@ bool rebuild_goto_start_functiont::operator()(
   std::unique_ptr<languaget> language=get_language_from_mode(mode);
   INVARIANT(language, "No language found for mode: "+id2string(mode));
   language->set_message_handler(get_message_handler());
+  language->get_language_options(cmdline);
 
   // To create a new entry point we must first remove the old one
   remove_existing_entry_point();
diff --git a/src/goto-programs/rebuild_goto_start_function.h b/src/goto-programs/rebuild_goto_start_function.h
index 870e05a61f6..79086aac570 100644
--- a/src/goto-programs/rebuild_goto_start_function.h
+++ b/src/goto-programs/rebuild_goto_start_function.h
@@ -10,6 +10,7 @@
 #define CPROVER_GOTO_PROGRAMS_REBUILD_GOTO_START_FUNCTION_H
 
 #include <util/message.h>
+class cmdlinet;
 
 class symbol_tablet;
 class goto_functionst;
@@ -25,6 +26,7 @@ class rebuild_goto_start_functiont: public messaget
 public:
   rebuild_goto_start_functiont(
     message_handlert &_message_handler,
+    const cmdlinet &cmdline,
     symbol_tablet &symbol_table,
     goto_functionst &goto_functions);
 
@@ -35,6 +37,7 @@ class rebuild_goto_start_functiont: public messaget
 
   void remove_existing_entry_point();
 
+  const cmdlinet &cmdline;
   symbol_tablet &symbol_table;
   goto_functionst &goto_functions;
 };
diff --git a/src/java_bytecode/java_bytecode_language.cpp b/src/java_bytecode/java_bytecode_language.cpp
index 8ea79aafa6d..6d71390627b 100644
--- a/src/java_bytecode/java_bytecode_language.cpp
+++ b/src/java_bytecode/java_bytecode_language.cpp
@@ -116,6 +116,7 @@ bool java_bytecode_languaget::generate_start_function(
   const irep_idt &entry_function_symbol_id,
   symbol_tablet &symbol_table)
 {
+  PRECONDITION(language_options_initialized);
   const auto res=
     get_main_symbol(
       symbol_table, entry_function_symbol_id, get_message_handler());
@@ -200,6 +201,8 @@ bool java_bytecode_languaget::typecheck(
   symbol_tablet &symbol_table,
   const std::string &module)
 {
+  PRECONDITION(language_options_initialized);
+
   if(string_refinement_enabled)
     string_preprocess.initialize_conversion_table();
 
@@ -385,6 +388,7 @@ void java_bytecode_languaget::replace_string_methods(
 
 bool java_bytecode_languaget::final(symbol_tablet &symbol_table)
 {
+  PRECONDITION(language_options_initialized);
   java_internal_additions(symbol_table);
 
   // replace code of String methods calls by code we generate