diff --git a/src/cbmc/symex_bmc.cpp b/src/cbmc/symex_bmc.cpp
index 438b5a0c73d..2cf88354f08 100644
--- a/src/cbmc/symex_bmc.cpp
+++ b/src/cbmc/symex_bmc.cpp
@@ -105,7 +105,7 @@ void symex_bmct::merge_goto(
     symex_coverage.covered(prev_pc, state.source.pc);
 }
 
-bool symex_bmct::get_unwind(
+bool symex_bmct::should_stop_unwind(
   const symex_targett::sourcet &source,
   const goto_symex_statet::call_stackt &context,
   unsigned unwind)
diff --git a/src/cbmc/symex_bmc.h b/src/cbmc/symex_bmc.h
index 9a0f7b50679..2e125241609 100644
--- a/src/cbmc/symex_bmc.h
+++ b/src/cbmc/symex_bmc.h
@@ -92,29 +92,23 @@ class symex_bmct: public goto_symext
   /// recursive call
   std::vector<recursion_unwind_handlert> recursion_unwind_handlers;
 
-  //
-  // overloaded from goto_symext
-  //
-  virtual void symex_step(
-    const get_goto_functiont &get_goto_function,
-    statet &state);
-
-  virtual void merge_goto(
-    const statet::goto_statet &goto_state,
-    statet &state);
-
-  // for loop unwinding
-  virtual bool get_unwind(
+  void symex_step(const get_goto_functiont &get_goto_function, statet &state)
+    override;
+
+  void
+  merge_goto(const statet::goto_statet &goto_state, statet &state) override;
+
+  bool should_stop_unwind(
     const symex_targett::sourcet &source,
     const goto_symex_statet::call_stackt &context,
-    unsigned unwind);
+    unsigned unwind) override;
 
-  virtual bool get_unwind_recursion(
+  bool get_unwind_recursion(
     const irep_idt &identifier,
     const unsigned thread_nr,
-    unsigned unwind);
+    unsigned unwind) override;
 
-  virtual void no_body(const irep_idt &identifier);
+  void no_body(const irep_idt &identifier) override;
 
   std::unordered_set<irep_idt> body_warnings;
 
diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h
index b59552f07af..882b8df257a 100644
--- a/src/goto-symex/goto_symex.h
+++ b/src/goto-symex/goto_symex.h
@@ -80,24 +80,12 @@ class goto_symext
   {
   }
 
-  virtual ~goto_symext()
-  {
-  }
+  virtual ~goto_symext() = default;
 
   typedef
     std::function<const goto_functionst::goto_functiont &(const irep_idt &)>
     get_goto_functiont;
 
-  /// \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.
-  virtual void symex_from_entry_point_of(
-    const goto_functionst &goto_functions,
-    symbol_tablet &new_symbol_table);
-
   /// \brief symex entire program starting from entry point
   ///
   /// The state that goto_symext maintains has a large memory footprint.
@@ -115,7 +103,7 @@ class goto_symext
   virtual void resume_symex_from_saved_state(
     const get_goto_functiont &get_goto_function,
     const statet &saved_state,
-    symex_target_equationt *const saved_equation,
+    symex_target_equationt *saved_equation,
     symbol_tablet &new_symbol_table);
 
   //// \brief symex entire program starting from entry point
@@ -142,38 +130,6 @@ class goto_symext
     const get_goto_functiont &,
     symbol_tablet &);
 
-  /// Symexes from the first instruction and the given state, terminating as
-  /// soon as the last instruction is reached.  This is useful to explicitly
-  /// symex certain ranges of a program, e.g. in an incremental decision
-  /// procedure.
-  /// \param state Symex state to start with.
-  /// \param goto_functions GOTO model to symex.
-  /// \param function_identifier The function with the instruction range
-  /// \param first Entry point in form of a first instruction.
-  /// \param limit Final instruction, which itself will not be symexed.
-  virtual void symex_instruction_range(
-    statet &,
-    const goto_functionst &,
-    const irep_idt &function_identifier,
-    goto_programt::const_targett first,
-    goto_programt::const_targett limit);
-
-  /// Symexes from the first instruction and the given state, terminating as
-  /// soon as the last instruction is reached.  This is useful to explicitly
-  /// symex certain ranges of a program, e.g. in an incremental decision
-  /// procedure.
-  /// \param state Symex state to start with.
-  /// \param get_goto_function retrieves a function body
-  /// \param function_identifier The function with the instruction range
-  /// \param first Entry point in form of a first instruction.
-  /// \param limit Final instruction, which itself will not be symexed.
-  virtual void symex_instruction_range(
-    statet &state,
-    const get_goto_functiont &get_goto_function,
-    const irep_idt &function_identifier,
-    goto_programt::const_targett first,
-    goto_programt::const_targett limit);
-
   /// \brief Have states been pushed onto the workqueue?
   ///
   /// If this flag is set at the end of a symbolic execution run, it means that
@@ -215,8 +171,6 @@ class goto_symext
   const bool allow_pointer_unsoundness;
 
 public:
-  // these bypass the target maps
-  virtual void symex_step_goto(statet &, bool taken);
 
   /// language_mode: ID_java, ID_C or another language identifier
   /// if we know the source language in use, irep_idt() otherwise.
@@ -263,13 +217,9 @@ class goto_symext
   void initialize_auto_object(const exprt &, statet &);
   void process_array_expr(exprt &);
   exprt make_auto_object(const typet &, statet &);
-  virtual void dereference(exprt &, statet &, const bool write);
+  virtual void dereference(exprt &, statet &, bool write);
 
-  void dereference_rec(
-    exprt &,
-    statet &,
-    guardt &,
-    const bool write);
+  void dereference_rec(exprt &, statet &, guardt &, bool write);
 
   void dereference_rec_address_of(
     exprt &,
@@ -292,13 +242,13 @@ class goto_symext
   virtual void symex_transition(
     statet &,
     goto_programt::const_targett to,
-    bool is_backwards_goto=false);
+    bool is_backwards_goto);
 
   virtual void symex_transition(statet &state)
   {
     goto_programt::const_targett next=state.source.pc;
     ++next;
-    symex_transition(state, next);
+    symex_transition(state, next, false);
   }
 
   virtual void symex_goto(statet &);
@@ -334,7 +284,7 @@ class goto_symext
 
   // determine whether to unwind a loop -- true indicates abort,
   // with false we continue.
-  virtual bool get_unwind(
+  virtual bool should_stop_unwind(
     const symex_targett::sourcet &source,
     const goto_symex_statet::call_stackt &context,
     unsigned unwind);
@@ -369,24 +319,20 @@ class goto_symext
 
   virtual bool get_unwind_recursion(
     const irep_idt &identifier,
-    const unsigned thread_nr,
+    unsigned thread_nr,
     unsigned unwind);
 
   void parameter_assignments(
-    const irep_idt function_identifier,
+    const irep_idt &function_identifier,
     const goto_functionst::goto_functiont &,
     statet &,
     const exprt::operandst &arguments);
 
   void locality(
-    const irep_idt function_identifier,
+    const irep_idt &function_identifier,
     statet &,
     const goto_functionst::goto_functiont &);
 
-  void add_end_of_function(
-    exprt &code,
-    const irep_idt &identifier);
-
   nondet_symbol_exprt build_symex_nondet(typet &type);
 
   // exceptions
@@ -471,7 +417,6 @@ class goto_symext
   static unsigned nondet_count;
   static unsigned dynamic_counter;
 
-  void read(exprt &);
   void replace_nondet(exprt &);
   void rewrite_quantifiers(exprt &, statet &);
 
diff --git a/src/goto-symex/symex_builtin_functions.cpp b/src/goto-symex/symex_builtin_functions.cpp
index f4e5e70ead1..43f9859c5c9 100644
--- a/src/goto-symex/symex_builtin_functions.cpp
+++ b/src/goto-symex/symex_builtin_functions.cpp
@@ -177,8 +177,8 @@ void goto_symext::symex_allocate(
   }
   else
   {
-    exprt nondet = build_symex_nondet(object_type);
-    code_assignt assignment(value_symbol.symbol_expr(), nondet);
+    const exprt nondet = build_symex_nondet(object_type);
+    const code_assignt assignment(value_symbol.symbol_expr(), nondet);
     symex_assign(state, assignment);
   }
 
diff --git a/src/goto-symex/symex_dereference_state.h b/src/goto-symex/symex_dereference_state.h
index a2aae7b3a87..3010ea2ae4f 100644
--- a/src/goto-symex/symex_dereference_state.h
+++ b/src/goto-symex/symex_dereference_state.h
@@ -32,13 +32,10 @@ class symex_dereference_statet:
   goto_symext &goto_symex;
   goto_symext::statet &state;
 
-  virtual void get_value_set(
-    const exprt &expr,
-    value_setst::valuest &value_set);
+  void
+  get_value_set(const exprt &expr, value_setst::valuest &value_set) override;
 
-  virtual bool has_failed_symbol(
-    const exprt &expr,
-    const symbolt *&symbol);
+  bool has_failed_symbol(const exprt &expr, const symbolt *&symbol) override;
 };
 
 #endif // CPROVER_GOTO_SYMEX_SYMEX_DEREFERENCE_STATE_H
diff --git a/src/goto-symex/symex_function_call.cpp b/src/goto-symex/symex_function_call.cpp
index abf85e6a514..5d555a43ac8 100644
--- a/src/goto-symex/symex_function_call.cpp
+++ b/src/goto-symex/symex_function_call.cpp
@@ -27,7 +27,7 @@ bool goto_symext::get_unwind_recursion(
 }
 
 void goto_symext::parameter_assignments(
-  const irep_idt function_identifier,
+  const irep_idt &function_identifier,
   const goto_functionst::goto_functiont &goto_function,
   statet &state,
   const exprt::operandst &arguments)
@@ -311,7 +311,7 @@ void goto_symext::symex_function_call_code(
 
   state.source.is_set=true;
   state.source.function = identifier;
-  symex_transition(state, goto_function.body.instructions.begin());
+  symex_transition(state, goto_function.body.instructions.begin(), false);
 }
 
 /// pop one call frame
@@ -323,7 +323,7 @@ void goto_symext::pop_frame(statet &state)
     statet::framet &frame=state.top();
 
     // restore program counter
-    symex_transition(state, frame.calling_location.pc);
+    symex_transition(state, frame.calling_location.pc, false);
     state.source.function = frame.calling_location.function;
 
     // restore L1 renaming
@@ -368,7 +368,7 @@ void goto_symext::symex_end_of_function(statet &state)
 /// preserves locality of local variables of a given function by applying L1
 /// renaming to the local identifiers
 void goto_symext::locality(
-  const irep_idt function_identifier,
+  const irep_idt &function_identifier,
   statet &state,
   const goto_functionst::goto_functiont &goto_function)
 {
diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp
index 95b91a14360..b846e34ce52 100644
--- a/src/goto-symex/symex_goto.cpp
+++ b/src/goto-symex/symex_goto.cpp
@@ -55,9 +55,9 @@ void goto_symext::symex_goto(statet &state)
   goto_programt::const_targett goto_target=
     instruction.get_target();
 
-  bool forward=!instruction.is_backwards_goto();
+  const bool backward = instruction.is_backwards_goto();
 
-  if(!forward) // backwards?
+  if(backward)
   {
     // is it label: goto label; or while(cond); - popular in SV-COMP
     if(
@@ -68,14 +68,10 @@ void goto_symext::symex_goto(statet &state)
     {
       // generate assume(false) or a suitable negation if this
       // instruction is a conditional goto
-      exprt negated_cond;
-
       if(new_guard.is_true())
-        negated_cond=false_exprt();
+        symex_assume(state, false_exprt());
       else
-        negated_cond=not_exprt(new_guard);
-
-      symex_assume(state, negated_cond);
+        symex_assume(state, not_exprt(new_guard));
 
       // next instruction
       symex_transition(state);
@@ -86,10 +82,8 @@ void goto_symext::symex_goto(statet &state)
       frame.loop_iterations[goto_programt::loop_id(*state.source.pc)].count;
     unwind++;
 
-    // continue unwinding?
-    if(get_unwind(state.source, state.call_stack(), unwind))
+    if(should_stop_unwind(state.source, state.call_stack(), unwind))
     {
-      // no!
       loop_bound_exceeded(state, new_guard);
 
       // next instruction
@@ -128,7 +122,7 @@ void goto_symext::symex_goto(statet &state)
   goto_programt::const_targett new_state_pc, state_pc;
   symex_targett::sourcet original_source=state.source;
 
-  if(forward)
+  if(!backward)
   {
     new_state_pc=goto_target;
     state_pc=state.source.pc;
@@ -141,7 +135,7 @@ void goto_symext::symex_goto(statet &state)
 
     if(state_pc==goto_target)
     {
-      symex_transition(state, goto_target);
+      symex_transition(state, goto_target, false);
       return; // nothing else to do
     }
   }
@@ -190,7 +184,7 @@ void goto_symext::symex_goto(statet &state)
     path_storaget::patht next_instruction(target, state);
     next_instruction.state.saved_target = state_pc;
     next_instruction.state.has_saved_next_instruction = true;
-    next_instruction.state.saved_target_is_backwards = !forward;
+    next_instruction.state.saved_target_is_backwards = backward;
 
     path_storaget::patht jump_target(target, state);
     jump_target.state.saved_target = new_state_pc;
@@ -198,7 +192,7 @@ void goto_symext::symex_goto(statet &state)
     // `forward` tells us where the branch we're _currently_ executing is
     // pointing to; this needs to be inverted for the branch that we're saving,
     // so let its truth value for `backwards` be the same as ours for `forward`.
-    jump_target.state.saved_target_is_backwards = forward;
+    jump_target.state.saved_target_is_backwards = !backward;
 
     log.debug() << "Saving next instruction '"
                 << next_instruction.state.saved_target->source_location << "'"
@@ -221,7 +215,7 @@ void goto_symext::symex_goto(statet &state)
 
   goto_state_list.push_back(statet::goto_statet(state));
 
-  symex_transition(state, state_pc, !forward);
+  symex_transition(state, state_pc, backward);
 
   // adjust guards
   if(new_guard.is_true())
@@ -275,7 +269,7 @@ void goto_symext::symex_goto(statet &state)
 
     if(state.has_saved_jump_target)
     {
-      if(forward)
+      if(!backward)
         state.guard.add(guard_expr);
       else
       {
@@ -286,7 +280,7 @@ void goto_symext::symex_goto(statet &state)
     else
     {
       statet::goto_statet &new_state = goto_state_list.back();
-      if(forward)
+      if(!backward)
       {
         new_state.guard.add(guard_expr);
         guard_expr.make_not();
@@ -302,23 +296,6 @@ void goto_symext::symex_goto(statet &state)
   }
 }
 
-void goto_symext::symex_step_goto(statet &state, bool taken)
-{
-  const goto_programt::instructiont &instruction=*state.source.pc;
-
-  exprt guard(instruction.guard);
-  dereference(guard, state, false);
-  state.rename(guard, ns);
-
-  if(!taken)
-    guard.make_not();
-
-  state.guard.guard_expr(guard);
-  do_simplify(guard);
-
-  target.assumption(state.guard.as_expr(), guard, state.source);
-}
-
 void goto_symext::merge_gotos(statet &state)
 {
   statet::framet &frame=state.top();
@@ -537,7 +514,7 @@ void goto_symext::loop_bound_exceeded(
   }
 }
 
-bool goto_symext::get_unwind(
+bool goto_symext::should_stop_unwind(
   const symex_targett::sourcet &,
   const goto_symex_statet::call_stackt &,
   unsigned)
diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp
index df00b4c0806..98a04878d83 100644
--- a/src/goto-symex/symex_main.cpp
+++ b/src/goto-symex/symex_main.cpp
@@ -144,7 +144,7 @@ void goto_symext::initialize_entry_point(
 
   state.dirty.populate_dirty_for_function(pc->function, entry_point_function);
 
-  symex_transition(state, state.source.pc);
+  symex_transition(state, state.source.pc, false);
 }
 
 void goto_symext::symex_threaded_step(
@@ -167,7 +167,7 @@ void goto_symext::symex_threaded_step(
     std::cout << "********* Now executing thread " << t << '\n';
 #endif
     state.switch_to_thread(t);
-    symex_transition(state, state.source.pc);
+    symex_transition(state, state.source.pc, false);
   }
 }
 
@@ -248,43 +248,6 @@ void goto_symext::resume_symex_from_saved_state(
       new_symbol_table);
 }
 
-void goto_symext::symex_instruction_range(
-  statet &state,
-  const goto_functionst &goto_functions,
-  const irep_idt &function_identifier,
-  const goto_programt::const_targett first,
-  const goto_programt::const_targett limit)
-{
-  symex_instruction_range(
-    state,
-    get_function_from_goto_functions(goto_functions),
-    function_identifier,
-    first,
-    limit);
-}
-
-void goto_symext::symex_instruction_range(
-  statet &state,
-  const get_goto_functiont &get_goto_function,
-  const irep_idt &function_identifier,
-  const goto_programt::const_targett first,
-  const goto_programt::const_targett limit)
-{
-  initialize_entry_point(
-    state, get_goto_function, function_identifier, first, limit);
-  ns = namespacet(outer_symbol_table, state.symbol_table);
-  while(state.source.function != limit->function || state.source.pc != limit)
-    symex_threaded_step(state, get_goto_function);
-}
-
-void goto_symext::symex_from_entry_point_of(
-  const goto_functionst &goto_functions,
-  symbol_tablet &new_symbol_table)
-{
-  symex_from_entry_point_of(
-    get_function_from_goto_functions(goto_functions), new_symbol_table);
-}
-
 void goto_symext::symex_from_entry_point_of(
   const get_goto_functiont &get_goto_function,
   symbol_tablet &new_symbol_table)
diff --git a/src/goto-symex/symex_target.h b/src/goto-symex/symex_target.h
index c6d7ed2da01..da7d9f7ccc3 100644
--- a/src/goto-symex/symex_target.h
+++ b/src/goto-symex/symex_target.h
@@ -30,6 +30,8 @@ class symex_targett
   {
     unsigned thread_nr;
     irep_idt function;
+    // The program counter is an iterator which indicates where the execution
+    // is in its program sequence
     goto_programt::const_targett pc;
     bool is_set;
 
diff --git a/src/pointer-analysis/dereference_callback.h b/src/pointer-analysis/dereference_callback.h
index 995daf9feae..b85d8e28f28 100644
--- a/src/pointer-analysis/dereference_callback.h
+++ b/src/pointer-analysis/dereference_callback.h
@@ -16,7 +16,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "value_sets.h"
 
-class guardt;
 class exprt;
 class symbolt;
 
diff --git a/src/pointer-analysis/value_set_dereference.cpp b/src/pointer-analysis/value_set_dereference.cpp
index dffa9f2e32e..31c6586b48a 100644
--- a/src/pointer-analysis/value_set_dereference.cpp
+++ b/src/pointer-analysis/value_set_dereference.cpp
@@ -32,8 +32,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/simplify_expr.h>
 #include <util/ssa_expr.h>
 
-/// \return The compound for a member expression, the array for an index
-///   expression, `expr` otherwise.
 const exprt &value_set_dereferencet::get_symbol(const exprt &expr)
 {
   if(expr.id()==ID_member || expr.id()==ID_index)
diff --git a/src/pointer-analysis/value_set_dereference.h b/src/pointer-analysis/value_set_dereference.h
index 3ad6258ba19..3425eb6068b 100644
--- a/src/pointer-analysis/value_set_dereference.h
+++ b/src/pointer-analysis/value_set_dereference.h
@@ -21,7 +21,6 @@ Author: Daniel Kroening, kroening@kroening.com
 class symbol_tablet;
 class guardt;
 class optionst;
-class modet;
 class symbolt;
 
 /// Wrapper for a function dereferencing pointer expressions using a value set.