diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
index bdd8c10c8e7..ae7ec1bfe89 100644
--- a/src/cbmc/cbmc_parse_options.cpp
+++ b/src/cbmc/cbmc_parse_options.cpp
@@ -635,6 +635,7 @@ 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(),
+        cmdline,
         goto_model.symbol_table,
         goto_model.goto_functions);
 
diff --git a/src/goto-programs/initialize_goto_model.cpp b/src/goto-programs/initialize_goto_model.cpp
index 1c434cfef8e..bc3c0f732ea 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..099292eba20 100644
--- a/src/goto-programs/rebuild_goto_start_function.cpp
+++ b/src/goto-programs/rebuild_goto_start_function.cpp
@@ -25,9 +25,11 @@
 ///   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),
+  cmdline(cmdline),
   symbol_table(symbol_table),
   goto_functions(goto_functions)
 {
@@ -50,6 +52,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..64d75372e25 100644
--- a/src/goto-programs/rebuild_goto_start_function.h
+++ b/src/goto-programs/rebuild_goto_start_function.h
@@ -9,6 +9,7 @@
 #ifndef CPROVER_GOTO_PROGRAMS_REBUILD_GOTO_START_FUNCTION_H
 #define CPROVER_GOTO_PROGRAMS_REBUILD_GOTO_START_FUNCTION_H
 
+#include <util/cmdline.h>
 #include <util/message.h>
 
 class symbol_tablet;
@@ -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;
 };