diff --git a/src/goto-symex/auto_objects.cpp b/src/goto-symex/auto_objects.cpp
index bf3c2b4a02c..d0f7e300727 100644
--- a/src/goto-symex/auto_objects.cpp
+++ b/src/goto-symex/auto_objects.cpp
@@ -34,9 +34,7 @@ exprt goto_symext::make_auto_object(const typet &type, statet &state)
   return symbol_exprt(symbol.name, symbol.type);
 }
 
-void goto_symext::initialize_auto_object(
-  const exprt &expr,
-  statet &state)
+void goto_symext::initialize_auto_object(const exprt &expr, statet &state)
 {
   const typet &type=ns.follow(expr.type());
 
@@ -77,9 +75,7 @@ void goto_symext::initialize_auto_object(
   }
 }
 
-void goto_symext::trigger_auto_object(
-  const exprt &expr,
-  statet &state)
+void goto_symext::trigger_auto_object(const exprt &expr, statet &state)
 {
   if(expr.id()==ID_symbol &&
      expr.get_bool(ID_C_SSA_symbol))
diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h
index 5ae5a79321f..c1d0ee5b382 100644
--- a/src/goto-symex/goto_symex.h
+++ b/src/goto-symex/goto_symex.h
@@ -36,38 +36,59 @@ class namespacet;
 class side_effect_exprt;
 class typecast_exprt;
 
-/// Configuration of the symbolic execution
+/// Configuration used for a symbolic execution
 struct symex_configt final
 {
+  /// \brief The maximum depth to take the execution to.
+  /// Depth is a count of the instructions that have been executed on any
+  /// single path.
   unsigned max_depth;
+
   bool doing_path_exploration;
+
   bool allow_pointer_unsoundness;
+
   bool constant_propagation;
+
   bool self_loops_to_assumptions;
+
   bool simplify_opt;
+
   bool unwinding_assertions;
+
   bool partial_loops;
+
   mp_integer debug_level;
 
   /// \brief Should the additional validation checks be run?
-  ///
   /// If this flag is set the checks for renaming (both level1 and level2) are
   /// executed in the goto_symex_statet (in the assignment method).
   bool run_validation_checks;
 
+  /// \brief Construct a symex_configt using options specified in an
+  /// \ref optionst
   explicit symex_configt(const optionst &options);
 };
 
 /// \brief The main class for the forward symbolic simulator
-///
+/// \remarks
 /// Higher-level architectural information on symbolic execution is
 /// documented in the \ref symex-overview
 /// "Symbolic execution module page".
 class goto_symext
 {
 public:
+  /// A type abbreviation for \ref goto_symex_statet
   typedef goto_symex_statet statet;
 
+  /// Construct a goto_symext to execute a particular program
+  /// \param mh: The message handler to use for log messages
+  /// \param outer_symbol_table: The symbol table for the program to be
+  ///   executed, excluding any symbols added during the symbolic execution
+  /// \param _target: Where to store the equation built up by this execution
+  /// \param options: The options to use to configure this execution
+  /// \param path_storage: Place to storage symbolic execution paths that have
+  /// been halted and can be resumed later
   goto_symext(
     message_handlert &mh,
     const symbol_tablet &outer_symbol_table,
@@ -76,7 +97,6 @@ class goto_symext
     path_storaget &path_storage)
     : should_pause_symex(false),
       symex_config(options),
-      language_mode(),
       outer_symbol_table(outer_symbol_table),
       ns(outer_symbol_table),
       target(_target),
@@ -89,21 +109,37 @@ class goto_symext
   {
   }
 
+  /// A virtual destructor allowing derived classes to be cleaned up correctly
   virtual ~goto_symext() = default;
 
+  /// The type of delegate functions that retrieve a goto_functiont for a
+  /// particular function identifier
+  /// \remarks
+  /// This allows goto_symext to be divorced from the particular type of
+  /// goto_modelt that provides the function bodies
   typedef
     std::function<const goto_functionst::goto_functiont &(const irep_idt &)>
     get_goto_functiont;
 
   /// Return a function to get/load a goto function from the given goto model
-  static get_goto_functiont get_goto_function(abstract_goto_modelt &);
-
-  /// \brief symex entire program starting from entry point
-  ///
-  /// The state that goto_symext maintains has a large memory footprint.
-  /// This method deallocates the state as soon as symbolic execution
-  /// has completed, so use it if you don't care about having the state
-  /// around afterwards.
+  /// Create a default delegate to retrieve function bodies from a
+  /// goto_functionst
+  /// \param goto_model: The goto model holding the function map from which to
+  ///   retrieve function bodies
+  /// \return A delegate to retrieve function bodies from the given
+  ///   goto_functionst
+  static get_goto_functiont get_goto_function(abstract_goto_modelt &goto_model);
+
+  /// \brief Symbolically execute the entire program starting from entry point
+  /// \remarks
+  /// The state that goto_symext maintains uses a lot of memory.
+  /// This method therefore deallocates the state as soon as symbolic execution
+  /// has completed. This function is useful to callers that don't care about
+  /// having the state around afterwards.
+  /// \param get_goto_function: The delegate to retrieve function bodies (see
+  ///   \ref get_goto_functiont)
+  /// \param new_symbol_table: A symbol table to store the symbols added during
+  /// symbolic execution
   virtual void symex_from_entry_point_of(
     const get_goto_functiont &get_goto_function,
     symbol_tablet &new_symbol_table);
@@ -114,37 +150,49 @@ class goto_symext
     symbol_tablet &new_symbol_table);
 
   /// Performs symbolic execution using a state and equation that have
-  /// already been used to symex part of the program. The state is not
-  /// re-initialized; instead, symbolic execution resumes from the program
-  /// counter of the saved state.
+  /// already been used to symbolically execute part of the program. The state
+  /// is not re-initialized; instead, symbolic execution resumes from the
+  /// program counter of the saved state.
+  /// \param get_goto_function: The delegate to retrieve function bodies (see
+  ///   \ref get_goto_functiont)
+  /// \param saved_state: The symbolic execution state to resume from
+  /// \param saved_equation: The equation as previously built up
+  /// \param new_symbol_table: A symbol table to store the symbols added during
+  ///   symbolic execution
   virtual void resume_symex_from_saved_state(
     const get_goto_functiont &get_goto_function,
     const statet &saved_state,
     symex_target_equationt *saved_equation,
     symbol_tablet &new_symbol_table);
 
-  //// \brief symex entire program starting from entry point
+  //// \brief Symbolically execute the entire program starting from entry point
   ///
   /// This method uses the `state` argument as the symbolic execution
   /// state, which is useful for examining the state after this method
   /// returns. The state that goto_symext maintains has a large memory
   /// footprint, so if keeping the state around is not necessary,
   /// clients should instead call goto_symext::symex_from_entry_point_of().
+  /// \param state: The symbolic execution state to use for the execution
+  /// \param get_goto_functions: A functor to retrieve function bodies to
+  ///   execute
+  /// \param new_symbol_table: A symbol table to store the symbols added during
+  ///   symbolic execution
   virtual void symex_with_state(
-    statet &,
-    const get_goto_functiont &,
-    symbol_tablet &);
+    statet &state,
+    const get_goto_functiont &get_goto_functions,
+    symbol_tablet &new_symbol_table);
 
-  /// \brief Have states been pushed onto the workqueue?
-  ///
+  /// \brief Set when states are pushed onto the workqueue
   /// If this flag is set at the end of a symbolic execution run, it means that
-  /// symex has been paused because we encountered a GOTO instruction while
-  /// doing path exploration, and thus pushed the successor states of the GOTO
-  /// onto path_storage. The symbolic execution caller should now choose which
-  /// successor state to continue executing, and resume symex from that state.
+  /// symbolic execution has been paused because we encountered a GOTO
+  /// instruction while doing path exploration, and thus pushed the successor
+  /// states of the GOTO onto path_storage. The symbolic execution caller
+  /// should now choose which successor state to continue executing, and resume
+  /// symbolic execution from that state.
   bool should_pause_symex;
 
 protected:
+  /// The configuration to use for this symbolic execution
   const symex_configt symex_config;
 
   /// Initialize the symbolic execution and the given state with
@@ -156,14 +204,23 @@ class goto_symext
 
   /// Invokes symex_step and verifies whether additional threads can be
   /// executed.
-  /// \param state: Current GOTO symex step.
-  /// \param get_goto_function: function that retrieves function bodies
+  /// \param state: Symbolic execution state for current instruction
+  /// \param get_goto_function: The delegate to retrieve function bodies (see
+  ///   \ref get_goto_functiont)
   void symex_threaded_step(
-    statet &, const get_goto_functiont &);
-
-  virtual void symex_step(
-    const get_goto_functiont &,
-    statet &);
+    statet &state,
+    const get_goto_functiont &get_goto_function);
+
+  /// \brief Called for each step in the symbolic execution
+  /// Case-switches over the type of the instruction being executed and calls
+  /// another function appropriate to the instruction type, for example
+  /// \ref symex_function_call if the current instruction is a function call,
+  /// \ref symex_goto if the current instruction is a goto, etc.
+  /// \param get_goto_function: The delegate to retrieve function bodies (see
+  ///   \ref get_goto_functiont)
+  /// \param state: Symbolic execution state for current instruction
+  virtual void
+  symex_step(const get_goto_functiont &get_goto_function, statet &state);
 
 public:
 
@@ -172,12 +229,11 @@ class goto_symext
   irep_idt language_mode;
 
 protected:
-
-  /// The symbol table associated with the goto-program that we're
-  /// executing. This symbol table will not additionally contain objects
-  /// that are dynamically created as part of symbolic execution; the
-  /// names of those object are stored in the symbol table passed as the
-  /// `new_symbol_table` argument to the `symex_*` methods.
+  /// The symbol table associated with the goto-program being executed.
+  /// This symbol table will not have objects that are dynamically created as
+  /// part of symbolic execution added to it; those object are stored in the
+  /// symbol table passed as the `new_symbol_table` argument to the `symex_*`
+  /// methods.
   const symbol_tablet &outer_symbol_table;
 
   /// Initialized just before symbolic execution begins, to point to
@@ -188,19 +244,29 @@ class goto_symext
   /// used during symbolic execution to look up names from the original
   /// goto-program, and the names of dynamically-created objects.
   namespacet ns;
+
+  /// The equation that this execution is building up
   symex_target_equationt &target;
+
+  /// A monotonically increasing index for each encountered ATOMIC_BEGIN
+  /// instruction
   unsigned atomic_section_counter;
 
+  /// The messaget to write log messages to
   mutable messaget log;
 
   friend class symex_dereference_statet;
 
-  // this does the following:
-  // a) rename non-det choices
-  // b) remove pointer dereferencing
-  // c) clean up byte_extract on the lhs of an assignment
-  void clean_expr(
-    exprt &, statet &, bool write);
+  /// Clean up an expression
+  /// \remarks
+  /// this does the following:
+  ///   a) rename non-det choices
+  ///   b) remove pointer dereferencing
+  ///   c) clean up byte_extract on the lhs of an assignment
+  /// \param expr: The expression to clean up
+  /// \param state
+  /// \param write
+  void clean_expr(exprt &expr, statet &state, bool write);
 
   void trigger_auto_object(const exprt &, statet &);
   void initialize_auto_object(const exprt &, statet &);
@@ -214,14 +280,32 @@ class goto_symext
     statet &,
     bool keep_array);
 
-  virtual void symex_goto(statet &);
-  virtual void symex_start_thread(statet &);
-  virtual void symex_atomic_begin(statet &);
-  virtual void symex_atomic_end(statet &);
-  virtual void symex_decl(statet &);
-  virtual void symex_decl(statet &, const symbol_exprt &expr);
-  virtual void symex_dead(statet &);
-  virtual void symex_other(statet &);
+  /// Symbolically execute a GOTO instruction
+  /// \param state: Symbolic execution state for current instruction
+  virtual void symex_goto(statet &state);
+  /// Symbolically execute a START_THREAD instruction
+  /// \param state: Symbolic execution state for current instruction
+  virtual void symex_start_thread(statet &state);
+  /// Symbolically execute an ATOMIC_BEGIN instruction
+  /// \param state: Symbolic execution state for current instruction
+  virtual void symex_atomic_begin(statet &state);
+  /// Symbolically execute an ATOMIC_END instruction
+  /// \param state: Symbolic execution state for current instruction
+  virtual void symex_atomic_end(statet &state);
+  /// Symbolically execute a DECL instruction
+  /// \param state: Symbolic execution state for current instruction
+  virtual void symex_decl(statet &state);
+  /// Symbolically execute a DECL instruction for the given symbol or simulate
+  /// such an execution for a synthetic symbol
+  /// \param state: Symbolic execution state for current instruction
+  /// \param expr: The symbol being declared
+  virtual void symex_decl(statet &state, const symbol_exprt &expr);
+  /// Symbolically execute a DEAD instruction
+  /// \param state: Symbolic execution state for current instruction
+  virtual void symex_dead(statet &state);
+  /// Symbolically execute an OTHER instruction
+  /// \param state: Symbolic execution state for current instruction
+  virtual void symex_other(statet &state);
 
   void symex_assert(const goto_programt::instructiont &, statet &);
   virtual void vcc(
@@ -229,42 +313,63 @@ class goto_symext
     const std::string &msg,
     statet &);
 
-  virtual void symex_assume(statet &, const exprt &cond);
+  /// Symbolically execute an ASSUME instruction or simulate such an execution
+  /// for a synthetic assumption
+  /// \param state: Symbolic execution state for current instruction
+  /// \param cond: The guard of the assumption
+  virtual void symex_assume(statet &state, const exprt &cond);
   void symex_assume_l2(statet &, const exprt &cond);
 
   /// Merge all branches joining at the current program point. Applies
   /// \ref merge_goto for each goto state (each of which corresponds to previous
   /// branch).
-  void merge_gotos(statet &);
+  /// \param state: Symbolic execution state to be updated
+  void merge_gotos(statet &state);
 
   /// Merge a single branch, the symbolic state of which is held in \p
   /// goto_state, into the current overall symbolic state. \p goto_state is no
   /// longer expected to be valid afterwards.
-  virtual void merge_goto(goto_statet &&goto_state, statet &);
-
-  void phi_function(const goto_statet &goto_state, statet &);
-
-  // determine whether to unwind a loop -- true indicates abort,
-  // with false we continue.
+  /// \param goto_state: A state to be merged into this location
+  /// \param state: Symbolic execution state to be updated
+  virtual void merge_goto(goto_statet &&goto_state, statet &state);
+
+  /// Merge the SSA assignments from goto_state into dest_state
+  /// \param goto_state: A state to be merged into this location
+  /// \param dest_state: Symbolic execution state to be updated
+  void phi_function(const goto_statet &goto_state, statet &dest_state);
+
+  /// Determine whether to unwind a loop
+  /// \param source
+  /// \param context
+  /// \param unwind
+  /// \return true indicates abort, with false we continue
   virtual bool should_stop_unwind(
     const symex_targett::sourcet &source,
     const goto_symex_statet::call_stackt &context,
     unsigned unwind);
 
-  virtual void loop_bound_exceeded(statet &, const exprt &guard);
+  virtual void loop_bound_exceeded(statet &state, const exprt &guard);
 
-  virtual void no_body(const irep_idt &)
+  /// Log a warning that a function has no body
+  /// \param identifier: The name of the function with no body
+  virtual void no_body(const irep_idt &identifier)
   {
   }
 
-  /// Symbolic execution of a function call.
+  /// Symbolically execute a FUNCTION_CALL instruction.
   /// Only functions that are symbols are supported, see
-  /// \ref goto_symext::symex_function_call_symbol
+  /// \ref goto_symext::symex_function_call_symbol.
+  /// \param get_goto_function: The delegate to retrieve function bodies (see
+  ///   \ref get_goto_functiont)
+  /// \param state: Symbolic execution state for current instruction
+  /// \param code: The function call instruction
   virtual void symex_function_call(
-    const get_goto_functiont &,
-    statet &,
-    const code_function_callt &);
+    const get_goto_functiont &get_goto_function,
+    statet &state,
+    const code_function_callt &code);
 
+  /// Symbolically execute a END_FUNCTION instruction.
+  /// \param state: Symbolic execution state for current instruction
   virtual void symex_end_of_function(statet &);
 
   /// Symbolic execution of a call to a function call.
@@ -273,10 +378,14 @@ class goto_symext
   /// \ref goto_symext::symex_fkt
   /// For non-special functions see
   /// \ref goto_symext::symex_function_call_code
+  /// \param get_goto_function: The delegate to retrieve function bodies (see
+  ///   \ref get_goto_functiont)
+  /// \param state: Symbolic execution state for current instruction
+  /// \param code: The function call instruction
   virtual void symex_function_call_symbol(
-    const get_goto_functiont &,
-    statet &,
-    const code_function_callt &);
+    const get_goto_functiont &get_goto_function,
+    statet &state,
+    const code_function_callt &code);
 
   /// Symbolic execution of a function call by inlining.
   /// Records the call in \p target by appending a function call step and:
@@ -284,10 +393,14 @@ class goto_symext
   ///    and proceed to executing the code of the function.
   ///   - otherwise assign a nondetministic value to the left-hand-side of the
   ///     call when there is one
+  /// \param get_goto_function: The delegate to retrieve function bodies (see
+  ///   \ref get_goto_functiont)
+  /// \param state: Symbolic execution state for current instruction
+  /// \param call: The function call instruction
   virtual void symex_function_call_code(
-    const get_goto_functiont &,
-    statet &,
-    const code_function_callt &);
+    const get_goto_functiont &get_goto_function,
+    statet &state,
+    const code_function_callt &call);
 
   virtual bool get_unwind_recursion(
     const irep_idt &identifier,
@@ -302,20 +415,28 @@ class goto_symext
   /// \param arguments: arguments that are passed to the function
   void parameter_assignments(
     const irep_idt &function_identifier,
-    const goto_functionst::goto_functiont &,
-    statet &,
+    const goto_functionst::goto_functiont &goto_function,
+    statet &state,
     const exprt::operandst &arguments);
 
   // exceptions
-  void symex_throw(statet &);
-  void symex_catch(statet &);
+  /// Symbolically execute a THROW instruction
+  /// \param state: Symbolic execution state for current instruction
+  void symex_throw(statet &state);
+  /// Symbolically execute a CATCH instruction
+  /// \param state: Symbolic execution state for current instruction
+  void symex_catch(statet &state);
 
-  virtual void do_simplify(exprt &);
+  virtual void do_simplify(exprt &expr);
 
-  void symex_assign(statet &, const code_assignt &);
+  /// Symbolically execute an ASSIGN instruction or simulate such an execution
+  /// for a synthetic assignment
+  /// \param state: Symbolic execution state for current instruction
+  /// \param code: The assignment to execute
+  void symex_assign(statet &state, const code_assignt &code);
 
   // havocs the given object
-  void havoc_rec(statet &, const guardt &, const exprt &);
+  void havoc_rec(statet &state, const guardt &guard, const exprt &dest);
 
   typedef symex_targett::assignment_typet assignment_typet;
 
@@ -378,22 +499,66 @@ class goto_symext
   static exprt add_to_lhs(const exprt &lhs, const exprt &what);
 
   virtual void symex_gcc_builtin_va_arg_next(
-    statet &, const exprt &lhs, const side_effect_exprt &);
+    statet &state,
+    const exprt &lhs,
+    const side_effect_exprt &code);
+  /// Symbolically execute an assignment instruction that has an `allocate` on
+  /// the right hand side
+  /// \param state: Symbolic execution state for current instruction
+  /// \param lhs: The expression to assign to
+  /// \param code: The `allocate` expression
   virtual void symex_allocate(
-    statet &, const exprt &lhs, const side_effect_exprt &);
-  virtual void symex_cpp_delete(statet &, const codet &);
-  virtual void symex_cpp_new(
-    statet &, const exprt &lhs, const side_effect_exprt &);
-  virtual void symex_fkt(statet &, const code_function_callt &);
-  virtual void symex_trace(statet &, const code_function_callt &);
-  virtual void symex_printf(statet &, const exprt &rhs);
-  virtual void symex_input(statet &, const codet &);
-  virtual void symex_output(statet &, const codet &);
-
+    statet &state,
+    const exprt &lhs,
+    const side_effect_exprt &code);
+  /// Symbolically execute an OTHER instruction that does a CPP `delete`
+  /// \param state: Symbolic execution state for current instruction
+  /// \param code: The cleaned up CPP `delete` instruction
+  virtual void symex_cpp_delete(statet &state, const codet &code);
+  /// Symbolically execute an assignment instruction that has a CPP `new` or
+  /// `new array` or a Java `new array` on the right hand side
+  /// \param state: Symbolic execution state for current instruction
+  /// \param lhs: The expression to assign to
+  /// \param code: The `new` expression
+  virtual void
+  symex_cpp_new(statet &state, const exprt &lhs, const side_effect_exprt &code);
+  /// Symbolically execute a FUNCTION_CALL instruction for a function whose
+  /// name starts with CPROVER_FKT_PREFIX
+  /// \remarks
+  /// While the name seems to imply that this would be called when symbolic
+  /// execution doesn't know what to do, it may actually be derived from a
+  /// German abbreviation for function.
+  /// This should not be called as these functions should already be removed
+  /// \param state: Symbolic execution state for current instruction
+  /// \param code: The function call instruction
+  virtual void symex_fkt(statet &state, const code_function_callt &code);
+  /// Symbolically execute a FUNCTION_CALL instruction for the `CBMC_trace`
+  /// function
+  /// \param state: Symbolic execution state for current instruction
+  /// \param code: The function call instruction
+  virtual void symex_trace(statet &state, const code_function_callt &code);
+  /// Symbolically execute an OTHER instruction that does a CPP `printf`
+  /// \param state: Symbolic execution state for current instruction
+  /// \param rhs: The cleaned up CPP `printf` instruction
+  virtual void symex_printf(statet &state, const exprt &rhs);
+  /// Symbolically execute an OTHER instruction that does a CPP input
+  /// \param state: Symbolic execution state for current instruction
+  /// \param code: The cleaned up input instruction
+  virtual void symex_input(statet &state, const codet &code);
+  /// Symbolically execute an OTHER instruction that does a CPP output
+  /// \param state: Symbolic execution state for current instruction
+  /// \param code: The cleaned up output instruction
+  virtual void symex_output(statet &state, const codet &code);
+
+  /// A monotonically increasing index for each created dynamic object
   static unsigned dynamic_counter;
 
   void rewrite_quantifiers(exprt &, statet &);
 
+  /// \brief Symbolic execution paths to be resumed later
+  /// \remarks
+  /// Partially-executed symbolic execution \ref path_storaget::patht "paths"
+  /// whose execution can be resumed later
   path_storaget &path_storage;
 
 public:
@@ -413,8 +578,9 @@ class goto_symext
   ///
   /// The actual number of total and remaining VCCs should be assigned to
   /// the relevant members of goto_symex_statet. The members below are used to
-  /// cache the values from goto_symex_statet after symex has ended, so that
-  /// \ref bmct can read those values even after the state has been deallocated.
+  /// cache the values from goto_symex_statet after symbolic execution has
+  /// ended, so that \ref bmct can read those values even after the state has
+  /// been deallocated.
 
   unsigned _total_vccs, _remaining_vccs;
   ///@}
@@ -449,6 +615,7 @@ class goto_symext
 /// recursion) being entered. 'Next instruction' in this situation refers
 /// to the next one in program order, so it ignores things like unconditional
 /// GOTOs, and only goes until the end of the current function.
+/// \param state: Symbolic execution state to be transformed
 void symex_transition(goto_symext::statet &state);
 
 void symex_transition(
diff --git a/src/goto-symex/goto_symex_state.h b/src/goto-symex/goto_symex_state.h
index 3462ed85000..a21b3eac445 100644
--- a/src/goto-symex/goto_symex_state.h
+++ b/src/goto-symex/goto_symex_state.h
@@ -114,8 +114,8 @@ struct framet
   }
 };
 
-/// Central data structure: state.
-
+/// \brief Central data structure: state.
+///
 /// The state is a persistent data structure that symex maintains as it
 /// executes. As we walk over each instruction, state will be updated reflecting
 /// their effects until a branch occurs (such as an if), where parts of the
diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp
index 32f93d89a50..d078c2502f0 100644
--- a/src/goto-symex/symex_assign.cpp
+++ b/src/goto-symex/symex_assign.cpp
@@ -21,9 +21,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 // #define USE_UPDATE
 
-void goto_symext::symex_assign(
-  statet &state,
-  const code_assignt &code)
+void goto_symext::symex_assign(statet &state, const code_assignt &code)
 {
   exprt lhs=code.lhs();
   exprt rhs=code.rhs();
diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp
index 87c6b1d7bb6..1c80b87c141 100644
--- a/src/goto-symex/symex_main.cpp
+++ b/src/goto-symex/symex_main.cpp
@@ -237,7 +237,10 @@ void goto_symext::symex_with_state(
 
     ~reset_namespacet()
     {
+      // Get symbol table 1, the outer symbol table from the GOTO program
       const symbol_tablet &st = ns.get_symbol_table();
+      // Move a new namespace containing this symbol table over the top of the
+      // current one
       ns = namespacet(st);
     }