diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp
index d7cadc121f1..8a1a8b7e938 100644
--- a/src/goto-instrument/goto_instrument_parse_options.cpp
+++ b/src/goto-instrument/goto_instrument_parse_options.cpp
@@ -897,6 +897,8 @@ void goto_instrument_parse_optionst::get_goto_program()
 {
   status() << "Reading GOTO program from `" << cmdline.args[0] << "'" << eom;
 
+  config.set(cmdline);
+
   auto result = read_goto_binary(cmdline.args[0], get_message_handler());
 
   if(!result.has_value())
@@ -904,7 +906,7 @@ void goto_instrument_parse_optionst::get_goto_program()
 
   goto_model = std::move(result.value());
 
-  config.set(cmdline);
+  config.set_from_symbol_table(goto_model.symbol_table);
 }
 
 void goto_instrument_parse_optionst::instrument_goto_program()
diff --git a/src/goto-programs/read_goto_binary.cpp b/src/goto-programs/read_goto_binary.cpp
index bc28f789493..d4333852dc6 100644
--- a/src/goto-programs/read_goto_binary.cpp
+++ b/src/goto-programs/read_goto_binary.cpp
@@ -27,6 +27,12 @@ Module: Read Goto Programs
 #include "elf_reader.h"
 #include "osx_fat_reader.h"
 
+/// \brief Read a goto binary from a file, but do not update \ref config
+/// \param filename the file name of the goto binary
+/// \param dest the goto model returned
+/// \param message_handler for diagnostics
+/// \deprecated Use read_goto_binary(file, message_handler) instead
+/// \return true on failure, false on success
 bool read_goto_binary(
   const std::string &filename,
   goto_modelt &dest,
@@ -36,6 +42,10 @@ bool read_goto_binary(
     filename, dest.symbol_table, dest.goto_functions, message_handler);
 }
 
+/// \brief Read a goto binary from a file, but do not update \ref config
+/// \param filename the file name of the goto binary
+/// \param message_handler for diagnostics
+/// \return goto model on success, {} on failure
 optionalt<goto_modelt>
 read_goto_binary(const std::string &filename, message_handlert &message_handler)
 {
@@ -50,6 +60,12 @@ read_goto_binary(const std::string &filename, message_handlert &message_handler)
     return std::move(dest);
 }
 
+/// \brief Read a goto binary from a file, but do not update \ref config
+/// \param filename the file name of the goto binary
+/// \param symbol_table the symbol table from the goto binary
+/// \param goto_functions the goto functions from the goto binary
+/// \param message_handler for diagnostics
+/// \return true on failure, false on success
 bool read_goto_binary(
   const std::string &filename,
   symbol_tablet &symbol_table,
@@ -206,8 +222,10 @@ bool is_goto_binary(const std::string &filename)
   return false;
 }
 
-/// reads an object file
-/// \par parameters: a file_name
+/// \brief reads an object file, and also updates config
+/// \param file_name file name of the goto binary
+/// \param dest the goto model returned
+/// \param message_handler for diagnostics
 /// \return true on error, false otherwise
 bool read_object_and_link(
   const std::string &file_name,
@@ -241,8 +259,9 @@ bool read_object_and_link(
   return false;
 }
 
-/// reads an object file
-/// \par parameters: a file_name
+/// \brief reads an object file, and also updates the config
+/// \param file_name file name of the goto binary
+/// \param message_handler for diagnostics
 /// \return true on error, false otherwise
 bool read_object_and_link(
   const std::string &file_name,