diff --git a/src/analyses/ai.cpp b/src/analyses/ai.cpp
index 10653ada420..9591d0b2725 100644
--- a/src/analyses/ai.cpp
+++ b/src/analyses/ai.cpp
@@ -122,7 +122,7 @@ void ai_baset::output(
     find_state(i_it).output(out, *this, ns);
     out << "\n";
     #if 1
-    goto_program.output_instruction(ns, identifier, out, i_it);
+    goto_program.output_instruction(ns, identifier, out, *i_it);
     out << "\n";
     #endif
   }
@@ -174,7 +174,7 @@ jsont ai_baset::output_json(
 
     // Ideally we need output_instruction_json
     std::ostringstream out;
-    goto_program.output_instruction(ns, identifier, out, i_it);
+    goto_program.output_instruction(ns, identifier, out, *i_it);
     location["instruction"]=json_stringt(out.str());
 
     contents.push_back(location);
@@ -235,7 +235,7 @@ xmlt ai_baset::output_xml(
 
     // Ideally we need output_instruction_xml
     std::ostringstream out;
-    goto_program.output_instruction(ns, identifier, out, i_it);
+    goto_program.output_instruction(ns, identifier, out, *i_it);
     location.set_attribute("instruction", out.str());
 
     function_body.new_element(location);
diff --git a/src/analyses/local_bitvector_analysis.cpp b/src/analyses/local_bitvector_analysis.cpp
index 341eab33d42..c45a4c90f79 100644
--- a/src/analyses/local_bitvector_analysis.cpp
+++ b/src/analyses/local_bitvector_analysis.cpp
@@ -349,7 +349,7 @@ void local_bitvector_analysist::output(
     }
 
     out << "\n";
-    goto_function.body.output_instruction(ns, "", out, i_it);
+    goto_function.body.output_instruction(ns, "", out, *i_it);
     out << "\n";
 
     l++;
diff --git a/src/analyses/local_may_alias.cpp b/src/analyses/local_may_alias.cpp
index e1af3b4e883..9e0751f9da9 100644
--- a/src/analyses/local_may_alias.cpp
+++ b/src/analyses/local_may_alias.cpp
@@ -466,7 +466,7 @@ void local_may_aliast::output(
     }
 
     out << "\n";
-    goto_function.body.output_instruction(ns, "", out, i_it);
+    goto_function.body.output_instruction(ns, "", out, *i_it);
     out << "\n";
 
     l++;
diff --git a/src/cbmc/symex_bmc.cpp b/src/cbmc/symex_bmc.cpp
index 1212e0405d8..4a1c59096b5 100644
--- a/src/cbmc/symex_bmc.cpp
+++ b/src/cbmc/symex_bmc.cpp
@@ -108,7 +108,7 @@ bool symex_bmct::get_unwind(
   const symex_targett::sourcet &source,
   unsigned unwind)
 {
-  const irep_idt id=goto_programt::loop_id(source.pc);
+  const irep_idt id=goto_programt::loop_id(*source.pc);
 
   // We use the most specific limit we have,
   // and 'infinity' when we have none.
diff --git a/src/goto-analyzer/unreachable_instructions.cpp b/src/goto-analyzer/unreachable_instructions.cpp
index c852ca7f6c2..183b149eff2 100644
--- a/src/goto-analyzer/unreachable_instructions.cpp
+++ b/src/goto-analyzer/unreachable_instructions.cpp
@@ -71,7 +71,7 @@ static void output_dead_plain(
   for(dead_mapt::const_iterator it=dead_map.begin();
       it!=dead_map.end();
       ++it)
-    goto_program.output_instruction(ns, "", os, it->second);
+    goto_program.output_instruction(ns, "", os, *it->second);
 }
 
 static void add_to_json(
@@ -101,7 +101,7 @@ static void add_to_json(
       ++it)
   {
     std::ostringstream oss;
-    goto_program.output_instruction(ns, "", oss, it->second);
+    goto_program.output_instruction(ns, "", oss, *it->second);
     std::string s=oss.str();
 
     std::string::size_type n=s.find('\n');
diff --git a/src/goto-diff/change_impact.cpp b/src/goto-diff/change_impact.cpp
index cec37680a53..67bcc2535b0 100644
--- a/src/goto-diff/change_impact.cpp
+++ b/src/goto-diff/change_impact.cpp
@@ -732,7 +732,7 @@ void change_impactt::output_instruction(char prefix,
   else
   {
     std::cout << prefix;
-    goto_program.output_instruction(ns, function, std::cout, target);
+    goto_program.output_instruction(ns, function, std::cout, *target);
   }
 }
 
diff --git a/src/goto-diff/unified_diff.cpp b/src/goto-diff/unified_diff.cpp
index 804592dc9d1..75924bfca5d 100644
--- a/src/goto-diff/unified_diff.cpp
+++ b/src/goto-diff/unified_diff.cpp
@@ -132,27 +132,15 @@ void unified_difft::output_diff(
     {
       case differencet::SAME:
         os << ' ';
-        new_goto_program.output_instruction(
-          ns_new,
-          identifier,
-          os,
-          d.first);
+        new_goto_program.output_instruction(ns_new, identifier, os, *d.first);
         break;
       case differencet::DELETED:
         os << '-';
-        old_goto_program.output_instruction(
-          ns_old,
-          identifier,
-          os,
-          d.first);
+        old_goto_program.output_instruction(ns_old, identifier, os, *d.first);
         break;
       case differencet::NEW:
         os << '+';
-        new_goto_program.output_instruction(
-          ns_new,
-          identifier,
-          os,
-          d.first);
+        new_goto_program.output_instruction(ns_new, identifier, os, *d.first);
         break;
     }
   }
diff --git a/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp b/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp
index acf0bf264cf..cf971a023f5 100644
--- a/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp
+++ b/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp
@@ -65,7 +65,7 @@ bool disjunctive_polynomial_accelerationt::accelerate(
   {
     if(loop.find(it)!=loop.end())
     {
-      goto_program.output_instruction(ns, "scratch", std::cout, it);
+      goto_program.output_instruction(ns, "scratch", std::cout, *it);
     }
   }
 
diff --git a/src/goto-instrument/accelerate/enumerating_loop_acceleration.cpp b/src/goto-instrument/accelerate/enumerating_loop_acceleration.cpp
index 01cf26f477f..2d56611f523 100644
--- a/src/goto-instrument/accelerate/enumerating_loop_acceleration.cpp
+++ b/src/goto-instrument/accelerate/enumerating_loop_acceleration.cpp
@@ -32,7 +32,7 @@ bool enumerating_loop_accelerationt::accelerate(
         it!=path.end();
         ++it)
     {
-      goto_program.output_instruction(ns, "OMG", std::cout, it->loc);
+      goto_program.output_instruction(ns, "OMG", std::cout, *it->loc);
     }
 #endif
 
diff --git a/src/goto-instrument/accelerate/path.cpp b/src/goto-instrument/accelerate/path.cpp
index 229c72cdb6b..6ae468a3a96 100644
--- a/src/goto-instrument/accelerate/path.cpp
+++ b/src/goto-instrument/accelerate/path.cpp
@@ -22,5 +22,5 @@ void output_path(
   std::ostream &str)
 {
   for(const auto &step : path)
-    program.output_instruction(ns, "path", str, step.loc);
+    program.output_instruction(ns, "path", str, *step.loc);
 }
diff --git a/src/goto-instrument/accelerate/polynomial_accelerator.cpp b/src/goto-instrument/accelerate/polynomial_accelerator.cpp
index 10f1793fcef..aa4850cd401 100644
--- a/src/goto-instrument/accelerate/polynomial_accelerator.cpp
+++ b/src/goto-instrument/accelerate/polynomial_accelerator.cpp
@@ -71,7 +71,7 @@ bool polynomial_acceleratort::accelerate(
       it!=body.end();
       ++it)
   {
-    program.output_instruction(ns, "scratch", std::cout, it);
+    program.output_instruction(ns, "scratch", std::cout, *it);
   }
 
   std::cout << "Modified:\n";
diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp
index 4681864736b..5fa1567001b 100644
--- a/src/goto-instrument/goto_instrument_parse_options.cpp
+++ b/src/goto-instrument/goto_instrument_parse_options.cpp
@@ -250,7 +250,7 @@ int goto_instrument_parse_optionst::doit()
 
         forall_goto_program_instructions(i_it, goto_program)
         {
-          goto_program.output_instruction(ns, "", std::cout, i_it);
+          goto_program.output_instruction(ns, "", std::cout, *i_it);
           std::cout << "Is threaded: " << (is_threaded(i_it)?"True":"False")
                     << "\n\n";
         }
diff --git a/src/goto-instrument/unwind.cpp b/src/goto-instrument/unwind.cpp
index 81f19d30c7a..01b0087c522 100644
--- a/src/goto-instrument/unwind.cpp
+++ b/src/goto-instrument/unwind.cpp
@@ -328,7 +328,7 @@ void goto_unwindt::unwind(
     symbol_tablet st;
     namespacet ns(st);
     std::cout << "Instruction:\n";
-    goto_program.output_instruction(ns, "", std::cout, i_it);
+    goto_program.output_instruction(ns, "", std::cout, *i_it);
 #endif
 
     if(!i_it->is_backwards_goto())
diff --git a/src/goto-programs/goto_functions_template.h b/src/goto-programs/goto_functions_template.h
index 3ea7a7bad83..1a95d670f60 100644
--- a/src/goto-programs/goto_functions_template.h
+++ b/src/goto-programs/goto_functions_template.h
@@ -185,42 +185,37 @@ template <class bodyT>
 void goto_functions_templatet<bodyT>::compute_location_numbers()
 {
   unsigned nr=0;
-
-  for(typename function_mapt::iterator
-      it=function_map.begin();
-      it!=function_map.end();
-      it++)
-    it->second.body.compute_location_numbers(nr);
+  for(auto &func : function_map)
+  {
+    func.second.body.compute_location_numbers(nr);
+  }
 }
 
 template <class bodyT>
 void goto_functions_templatet<bodyT>::compute_incoming_edges()
 {
-  for(typename function_mapt::iterator
-      it=function_map.begin();
-      it!=function_map.end();
-      it++)
-    it->second.body.compute_incoming_edges();
+  for(auto &func : function_map)
+  {
+    func.second.body.compute_incoming_edges();
+  }
 }
 
 template <class bodyT>
 void goto_functions_templatet<bodyT>::compute_target_numbers()
 {
-  for(typename function_mapt::iterator
-      it=function_map.begin();
-      it!=function_map.end();
-      it++)
-    it->second.body.compute_target_numbers();
+  for(auto &func : function_map)
+  {
+    func.second.body.compute_target_numbers();
+  }
 }
 
 template <class bodyT>
 void goto_functions_templatet<bodyT>::compute_loop_numbers()
 {
-  for(typename function_mapt::iterator
-      it=function_map.begin();
-      it!=function_map.end();
-      it++)
-    it->second.body.compute_loop_numbers();
+  for(auto &func : function_map)
+  {
+    func.second.body.compute_loop_numbers();
+  }
 }
 
 #endif // CPROVER_GOTO_PROGRAMS_GOTO_FUNCTIONS_TEMPLATE_H
diff --git a/src/goto-programs/goto_inline_class.cpp b/src/goto-programs/goto_inline_class.cpp
index a21768f7732..ee89b365ec6 100644
--- a/src/goto-programs/goto_inline_class.cpp
+++ b/src/goto-programs/goto_inline_class.cpp
@@ -444,7 +444,7 @@ void goto_inlinet::expand_function_call(
 
 #ifdef DEBUG
   std::cout << "Expanding call:\n";
-  dest.output_instruction(ns, "", std::cout, target);
+  dest.output_instruction(ns, "", std::cout, *target);
 #endif
 
   exprt lhs;
@@ -815,7 +815,7 @@ void goto_inlinet::output_inline_map(
         bool transitive=call.second;
 
         out << "  Call:\n";
-        goto_program.output_instruction(ns, "", out, target);
+        goto_program.output_instruction(ns, "", out, *target);
         out << "  Transitive: " << transitive << "\n";
       }
     }
diff --git a/src/goto-programs/goto_program.cpp b/src/goto-programs/goto_program.cpp
index 6cf8414899a..9b194fc4e5b 100644
--- a/src/goto-programs/goto_program.cpp
+++ b/src/goto-programs/goto_program.cpp
@@ -17,22 +17,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <langapi/language_util.h>
 
-/// See below.
-/// \param ns: the namespace to resolve the expressions in
-/// \param identifier: the identifier used to find a symbol to identify the
-///   source language
-/// \param out: the stream to write the goto string to
-/// \param it: an iterator pointing to the instruction to convert
-/// \return See below.
-std::ostream &goto_programt::output_instruction(
-  const class namespacet &ns,
-  const irep_idt &identifier,
-  std::ostream &out,
-  instructionst::const_iterator it) const
-{
-  return output_instruction(ns, identifier, out, *it);
-}
-
 /// Writes to \p out a two/three line string representation of a given
 /// \p instruction. The output is of the format:
 /// ```
diff --git a/src/goto-programs/goto_program.h b/src/goto-programs/goto_program.h
index 64b67cb6626..4ef4262a0d1 100644
--- a/src/goto-programs/goto_program.h
+++ b/src/goto-programs/goto_program.h
@@ -28,13 +28,7 @@ class goto_programt:public goto_program_templatet<codet, exprt>
     const class namespacet &ns,
     const irep_idt &identifier,
     std::ostream &out,
-    instructionst::const_iterator it) const;
-
-  std::ostream &output_instruction(
-    const class namespacet &ns,
-    const irep_idt &identifier,
-    std::ostream &out,
-    const instructiont &instruction) const;
+    const instructiont &instruction) const override;
 
   goto_programt() { }
 
diff --git a/src/goto-programs/goto_program_template.h b/src/goto-programs/goto_program_template.h
index da596927fc2..264cf77c77c 100644
--- a/src/goto-programs/goto_program_template.h
+++ b/src/goto-programs/goto_program_template.h
@@ -503,7 +503,7 @@ class goto_program_templatet
     const namespacet &ns,
     const irep_idt &identifier,
     std::ostream &out,
-    typename instructionst::const_iterator it) const=0;
+    const typename instructionst::value_type &it) const = 0;
 
   /// Compute the target numbers
   void compute_target_numbers();
@@ -529,10 +529,10 @@ class goto_program_templatet
   void update();
 
   /// Human-readable loop name
-  static irep_idt loop_id(const_targett target)
+  static irep_idt loop_id(const instructiont &instruction)
   {
-    return id2string(target->function)+"."+
-           std::to_string(target->loop_number);
+    return id2string(instruction.function)+"."+
+           std::to_string(instruction.loop_number);
   }
 
   /// Is the program empty?
@@ -665,11 +665,8 @@ std::ostream &goto_program_templatet<codeT, guardT>::output(
 {
   // output program
 
-  for(typename instructionst::const_iterator
-      it=instructions.begin();
-      it!=instructions.end();
-      ++it)
-    output_instruction(ns, identifier, out, it);
+  for(const auto &instruction : instructions)
+    output_instruction(ns, identifier, out, instruction);
 
   return out;
 }
diff --git a/src/goto-programs/interpreter.cpp b/src/goto-programs/interpreter.cpp
index b2542cbeee7..05107b6d896 100644
--- a/src/goto-programs/interpreter.cpp
+++ b/src/goto-programs/interpreter.cpp
@@ -114,7 +114,7 @@ void interpretert::show_state()
       ns,
       function->first,
       status(),
-      pc);
+      *pc);
 
   status() << eom;
 }
diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp
index a86efc0815e..d4875f27228 100644
--- a/src/goto-symex/symex_goto.cpp
+++ b/src/goto-symex/symex_goto.cpp
@@ -78,7 +78,7 @@ void goto_symext::symex_goto(statet &state)
     }
 
     unsigned &unwind=
-      frame.loop_iterations[goto_programt::loop_id(state.source.pc)].count;
+      frame.loop_iterations[goto_programt::loop_id(*state.source.pc)].count;
     unwind++;
 
     // continue unwinding?
diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp
index d7a897e7f85..3deef4ae22c 100644
--- a/src/goto-symex/symex_main.cpp
+++ b/src/goto-symex/symex_main.cpp
@@ -40,7 +40,7 @@ void goto_symext::symex_transition(
       if(i_e->is_goto() && i_e->is_backwards_goto() &&
          (!is_backwards_goto ||
           state.source.pc->location_number>i_e->location_number))
-        frame.loop_iterations[goto_programt::loop_id(i_e)].count=0;
+        frame.loop_iterations[goto_programt::loop_id(*i_e)].count=0;
   }
 
   state.source.pc=to;
diff --git a/src/pointer-analysis/value_set_analysis_fivr.h b/src/pointer-analysis/value_set_analysis_fivr.h
index d583379ab0e..edd1b512f32 100644
--- a/src/pointer-analysis/value_set_analysis_fivr.h
+++ b/src/pointer-analysis/value_set_analysis_fivr.h
@@ -53,7 +53,7 @@ class value_set_analysis_fivrt:
       out << "**** " << it->source_location << '\n';
       output(it, out);
       out << '\n';
-      goto_program.output_instruction(ns, "", out, it);
+      goto_program.output_instruction(ns, "", out, *it);
       out << '\n';
     }
   }
diff --git a/src/pointer-analysis/value_set_analysis_fivrns.h b/src/pointer-analysis/value_set_analysis_fivrns.h
index a5fd4fd3fcd..d87595b02a1 100644
--- a/src/pointer-analysis/value_set_analysis_fivrns.h
+++ b/src/pointer-analysis/value_set_analysis_fivrns.h
@@ -55,7 +55,7 @@ class value_set_analysis_fivrnst:
       out << "**** " << it->source_location << '\n';
       output(it, out);
       out << '\n';
-      goto_program.output_instruction(ns, "", out, it);
+      goto_program.output_instruction(ns, "", out, *it);
       out << '\n';
     }
   }