diff --git a/src/goto-cc/linker_script_merge.cpp b/src/goto-cc/linker_script_merge.cpp
index 78458bfd8a3..88579044870 100644
--- a/src/goto-cc/linker_script_merge.cpp
+++ b/src/goto-cc/linker_script_merge.cpp
@@ -480,11 +480,13 @@ int linker_script_merget::ls_data2instructions(
       symbol_exprt end_sym(d["end-symbol"].value, pointer_type(char_type()));
       linker_values[d["end-symbol"].value]=std::make_pair(end_sym, array_end);
 
-      auto it=std::find_if(data["addresses"].array.begin(),
-                           data["addresses"].array.end(),
-                           [&d](const jsont &add)
-                           { return add["sym"].value==d["end-symbol"].value; });
-      if(it==data["addresses"].array.end())
+      auto entry = std::find_if(
+        data["addresses"].array.begin(),
+        data["addresses"].array.end(),
+        [&d](const jsont &add) {
+          return add["sym"].value == d["end-symbol"].value;
+        });
+      if(entry == data["addresses"].array.end())
       {
         error() << "Could not find address corresponding to symbol '"
                 << d["end-symbol"].value << "' (end of section)" << eom;
@@ -493,9 +495,9 @@ int linker_script_merget::ls_data2instructions(
       source_locationt  end_loc;
       end_loc.set_file(linker_script);
       std::ostringstream end_comment;
-      end_comment << "Pointer to end of object section '"
-                  << d["section"].value << "'. Original address in object file"
-                  << " is " << (*it)["val"].value;
+      end_comment << "Pointer to end of object section '" << d["section"].value
+                  << "'. Original address in object file"
+                  << " is " << (*entry)["val"].value;
       end_loc.set_comment(end_comment.str());
       end_sym.add_source_location()=end_loc;
 
diff --git a/src/goto-instrument/accelerate/accelerate.cpp b/src/goto-instrument/accelerate/accelerate.cpp
index 355a6065191..62948970db2 100644
--- a/src/goto-instrument/accelerate/accelerate.cpp
+++ b/src/goto-instrument/accelerate/accelerate.cpp
@@ -183,15 +183,18 @@ void acceleratet::insert_accelerator(
   goto_programt::targett &loop_header,
   goto_programt::targett &back_jump,
   path_acceleratort &accelerator,
-  subsumed_patht &subsumed)
+  subsumed_patht &subsumed_path)
 {
   insert_looping_path(
-    loop_header, back_jump, accelerator.pure_accelerator, subsumed.accelerator);
+    loop_header,
+    back_jump,
+    accelerator.pure_accelerator,
+    subsumed_path.accelerator);
 
   if(!accelerator.overflow_path.instructions.empty())
   {
     insert_looping_path(
-      loop_header, back_jump, accelerator.overflow_path, subsumed.residue);
+      loop_header, back_jump, accelerator.overflow_path, subsumed_path.residue);
   }
 }
 
diff --git a/src/goto-instrument/accelerate/accelerate.h b/src/goto-instrument/accelerate/accelerate.h
index 05dec188f28..9535852041b 100644
--- a/src/goto-instrument/accelerate/accelerate.h
+++ b/src/goto-instrument/accelerate/accelerate.h
@@ -84,7 +84,7 @@ class acceleratet
     goto_programt::targett &loop_header,
     goto_programt::targett &back_jump,
     path_acceleratort &accelerator,
-    subsumed_patht &subsumed);
+    subsumed_patht &subsumed_path);
 
   void set_dirty_vars(path_acceleratort &accelerator);
   void add_dirty_checks();
diff --git a/src/goto-instrument/accelerate/acceleration_utils.cpp b/src/goto-instrument/accelerate/acceleration_utils.cpp
index a04c5ef1a22..4ef547ca802 100644
--- a/src/goto-instrument/accelerate/acceleration_utils.cpp
+++ b/src/goto-instrument/accelerate/acceleration_utils.cpp
@@ -556,7 +556,6 @@ acceleration_utilst::expr_pairst acceleration_utilst::gather_array_assignments(
 bool acceleration_utilst::do_arrays(
   goto_programt::instructionst &loop_body,
   std::map<exprt, polynomialt> &polynomials,
-  exprt &loop_counter,
   substitutiont &substitution,
   scratch_programt &program)
 {
@@ -881,7 +880,6 @@ bool acceleration_utilst::expr2poly(
 bool acceleration_utilst::do_nonrecursive(
   goto_programt::instructionst &body,
   std::map<exprt, polynomialt> &polynomials,
-  exprt &loop_counter,
   substitutiont &substitution,
   expr_sett &nonrecursive,
   scratch_programt &program)
@@ -1004,7 +1002,7 @@ bool acceleration_utilst::do_nonrecursive(
     const exprt &lhs=*it;
     const exprt &rhs=state[*it];
 
-    if(!assign_array(lhs, rhs, loop_counter, program))
+    if(!assign_array(lhs, rhs, program))
     {
 #ifdef DEBUG
       std::cout << "Failed to assign a nonrecursive array: " <<
@@ -1020,7 +1018,6 @@ bool acceleration_utilst::do_nonrecursive(
 bool acceleration_utilst::assign_array(
   const exprt &lhs,
   const exprt &rhs,
-  const exprt &loop_counter,
   scratch_programt &program)
 {
 #ifdef DEBUG
@@ -1245,12 +1242,8 @@ void acceleration_utilst::extract_polynomial(
       continue;
     }
 
-    for(expr_listt::iterator it=terms.begin();
-        it!=terms.end();
-        ++it)
+    for(const auto &term : terms)
     {
-      exprt term=*it;
-
       if(degrees.find(term)!=degrees.end())
       {
         degrees[term]++;
diff --git a/src/goto-instrument/accelerate/acceleration_utils.h b/src/goto-instrument/accelerate/acceleration_utils.h
index 3d12c7db549..c9213919376 100644
--- a/src/goto-instrument/accelerate/acceleration_utils.h
+++ b/src/goto-instrument/accelerate/acceleration_utils.h
@@ -101,7 +101,6 @@ class acceleration_utilst
 
   bool do_arrays(goto_programt::instructionst &loop_body,
                  std::map<exprt, polynomialt> &polynomials,
-                 exprt &loop_counter,
                  substitutiont &substitution,
                  scratch_programt &program);
   expr_pairst gather_array_assignments(
@@ -120,14 +119,12 @@ class acceleration_utilst
   bool do_nonrecursive(
     goto_programt::instructionst &loop_body,
     std::map<exprt, polynomialt> &polynomials,
-    exprt &loop_counter,
     substitutiont &substitution,
     expr_sett &nonrecursive,
     scratch_programt &program);
   bool assign_array(
     const exprt &lhs,
     const exprt &rhs,
-    const exprt &loop_counter,
     scratch_programt &program);
 
   void gather_array_accesses(const exprt &expr, expr_sett &arrays);
@@ -157,8 +154,6 @@ class acceleration_utilst
   const goto_functionst &goto_functions;
   exprt &loop_counter;
   nil_exprt nil;
-
-  static int num_symbols;
 };
 
 #endif // CPROVER_GOTO_INSTRUMENT_ACCELERATE_ACCELERATION_UTILS_H
diff --git a/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp b/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp
index b94b616ea31..00e20612208 100644
--- a/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp
+++ b/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp
@@ -315,7 +315,7 @@ bool disjunctive_polynomial_accelerationt::accelerate(
   }
 
   // Add in any array assignments we can do now.
-  if(!utils.do_arrays(assigns, polynomials, loop_counter, stashed, program))
+  if(!utils.do_arrays(assigns, polynomials, stashed, program))
   {
     // We couldn't model some of the array assignments with polynomials...
     // Unfortunately that means we just have to bail out.
diff --git a/src/goto-instrument/accelerate/polynomial_accelerator.cpp b/src/goto-instrument/accelerate/polynomial_accelerator.cpp
index 874b6f04639..2330e0eda59 100644
--- a/src/goto-instrument/accelerate/polynomial_accelerator.cpp
+++ b/src/goto-instrument/accelerate/polynomial_accelerator.cpp
@@ -251,7 +251,7 @@ bool polynomial_acceleratort::accelerate(
 
   // Add in any array assignments we can do now.
   if(!utils.do_nonrecursive(
-      assigns, polynomials, loop_counter, stashed, nonrecursive, program))
+       assigns, polynomials, stashed, nonrecursive, program))
   {
     // We couldn't model some of the array assignments with polynomials...
     // Unfortunately that means we just have to bail out.
diff --git a/src/goto-instrument/accelerate/polynomial_accelerator.h b/src/goto-instrument/accelerate/polynomial_accelerator.h
index 8b92c0989ad..a9d2eb8ff40 100644
--- a/src/goto-instrument/accelerate/polynomial_accelerator.h
+++ b/src/goto-instrument/accelerate/polynomial_accelerator.h
@@ -133,7 +133,6 @@ class polynomial_acceleratort
   bool do_arrays(
     goto_programt::instructionst &loop_body,
     std::map<exprt, polynomialt> &polynomials,
-    exprt &loop_counter,
     substitutiont &substitution,
     scratch_programt &program);
   expr_pairst gather_array_assignments(
diff --git a/src/goto-instrument/concurrency.cpp b/src/goto-instrument/concurrency.cpp
index e2215da6bf2..49f91970fe8 100644
--- a/src/goto-instrument/concurrency.cpp
+++ b/src/goto-instrument/concurrency.cpp
@@ -130,8 +130,8 @@ void concurrency_instrumentationt::instrument(
       instrument(code.function());
 
       // instrument(code.lhs(), LHS);
-      Forall_expr(it, code.arguments())
-        instrument(*it);
+      for(auto &arg : code.arguments())
+        instrument(arg);
     }
   }
 }
diff --git a/src/goto-instrument/document_properties.cpp b/src/goto-instrument/document_properties.cpp
index d0cae86735e..b3a15283e7c 100644
--- a/src/goto-instrument/document_properties.cpp
+++ b/src/goto-instrument/document_properties.cpp
@@ -155,9 +155,9 @@ void document_propertiest::get_code(
   dest="";
 
   const irep_idt &file=source_location.get_file();
-  const irep_idt &line=source_location.get_line();
+  const irep_idt &source_line = source_location.get_line();
 
-  if(file=="" || line=="")
+  if(file == "" || source_line == "")
     return;
 
   std::ifstream in(id2string(file));
@@ -170,7 +170,7 @@ void document_propertiest::get_code(
     return;
   }
 
-  int line_int=unsafe_string2int(id2string(line));
+  int line_int = unsafe_string2int(id2string(source_line));
 
   int line_start=line_int-3,
       line_end=line_int+3;
diff --git a/src/goto-instrument/dot.cpp b/src/goto-instrument/dot.cpp
index 02bb5cf4148..5acaa52076e 100644
--- a/src/goto-instrument/dot.cpp
+++ b/src/goto-instrument/dot.cpp
@@ -264,8 +264,6 @@ void dott::output(std::ostream &out)
   out << "digraph G {\n";
   out << DOTGRAPHSETTINGS << '\n';
 
-  std::list<exprt> clusters;
-
   forall_goto_functions(it, goto_model.goto_functions)
     if(it->second.body_available())
       write_dot_subgraph(out, id2string(it->first), it->second.body);
diff --git a/src/goto-instrument/nondet_static.cpp b/src/goto-instrument/nondet_static.cpp
index c329763be2a..c786d848ef9 100644
--- a/src/goto-instrument/nondet_static.cpp
+++ b/src/goto-instrument/nondet_static.cpp
@@ -73,11 +73,11 @@ void nondet_static(
   goto_functionst &goto_functions,
   const irep_idt &fct_name)
 {
-  goto_functionst::function_mapt::iterator
-    i_it=goto_functions.function_map.find(fct_name);
-  assert(i_it!=goto_functions.function_map.end());
+  goto_functionst::function_mapt::iterator fct_entry =
+    goto_functions.function_map.find(fct_name);
+  CHECK_RETURN(fct_entry != goto_functions.function_map.end());
 
-  goto_programt &init=i_it->second.body;
+  goto_programt &init = fct_entry->second.body;
 
   Forall_goto_program_instructions(i_it, init)
   {
diff --git a/src/goto-instrument/thread_instrumentation.cpp b/src/goto-instrument/thread_instrumentation.cpp
index a3a7518c2df..8c07698f891 100644
--- a/src/goto-instrument/thread_instrumentation.cpp
+++ b/src/goto-instrument/thread_instrumentation.cpp
@@ -120,14 +120,14 @@ void mutex_init_instrumentation(goto_modelt &goto_model)
 {
   // get pthread_mutex_lock
 
-  symbol_tablet::symbolst::const_iterator f_it=
+  symbol_tablet::symbolst::const_iterator lock_entry =
     goto_model.symbol_table.symbols.find("pthread_mutex_lock");
 
-  if(f_it==goto_model.symbol_table.symbols.end())
+  if(lock_entry == goto_model.symbol_table.symbols.end())
     return;
 
   // get type of lock argument
-  code_typet code_type=to_code_type(to_code_type(f_it->second.type));
+  code_typet code_type = to_code_type(to_code_type(lock_entry->second.type));
   if(code_type.parameters().size()!=1)
     return;
 
diff --git a/src/goto-instrument/unwind.cpp b/src/goto-instrument/unwind.cpp
index a7ef29eb16d..38129fd7f6e 100644
--- a/src/goto-instrument/unwind.cpp
+++ b/src/goto-instrument/unwind.cpp
@@ -55,9 +55,10 @@ void goto_unwindt::copy_segment(
   assert(goto_program.instructions.size()==target_vector.size());
 
   // adjust intra-segment gotos
-  for(std::size_t i=0; i<target_vector.size(); i++)
+  for(std::size_t target_index = 0; target_index < target_vector.size();
+      target_index++)
   {
-    goto_programt::targett t=target_vector[i];
+    goto_programt::targett t = target_vector[target_index];
 
     if(!t->is_goto())
       continue;
diff --git a/src/goto-instrument/wmm/goto2graph.cpp b/src/goto-instrument/wmm/goto2graph.cpp
index bd9e179ea42..22d8febc8ef 100644
--- a/src/goto-instrument/wmm/goto2graph.cpp
+++ b/src/goto-instrument/wmm/goto2graph.cpp
@@ -210,9 +210,13 @@ void instrumentert::cfg_visitort::visit_cfg_function(
     /* a:=b -o-> Rb -po-> Wa */
     else if(instruction.is_assign())
     {
-      visit_cfg_assign(value_sets, ns, i_it, no_dependencies
+      visit_cfg_assign(
+        value_sets,
+        i_it,
+        no_dependencies
 #ifdef LOCAL_MAY
-        , local_may
+        ,
+        local_may
 #endif
       ); // NOLINT(whitespace/parens)
     }
@@ -783,7 +787,6 @@ void instrumentert::cfg_visitort::visit_cfg_asm_fence(
 
 void instrumentert::cfg_visitort::visit_cfg_assign(
   value_setst &value_sets,
-  namespacet &ns,
   goto_programt::instructionst::iterator &i_it,
   bool no_dependencies
 #ifdef LOCAL_MAY
diff --git a/src/goto-instrument/wmm/goto2graph.h b/src/goto-instrument/wmm/goto2graph.h
index bf1cb30693e..89bc0e30e7c 100644
--- a/src/goto-instrument/wmm/goto2graph.h
+++ b/src/goto-instrument/wmm/goto2graph.h
@@ -125,11 +125,14 @@ class instrumentert
       goto_programt::const_targett i_it);
     void inline visit_cfg_duplicate(goto_programt::const_targett targ,
       goto_programt::const_targett i_it);
-    void visit_cfg_assign(value_setst &value_sets, namespacet &ns,
-      goto_programt::instructionst::iterator &i_it, bool no_dependencies
-      #ifdef LOCAL_MAY
-      , local_may_aliast &local_may
-      #endif
+    void visit_cfg_assign(
+      value_setst &value_sets,
+      goto_programt::instructionst::iterator &i_it,
+      bool no_dependencies
+#ifdef LOCAL_MAY
+      ,
+      local_may_aliast &local_may
+#endif
     ); // NOLINT(whitespace/parens)
     void visit_cfg_fence(goto_programt::instructionst::iterator i_it);
     void visit_cfg_skip(goto_programt::instructionst::iterator i_it);
diff --git a/src/goto-instrument/wmm/instrumenter_strategies.cpp b/src/goto-instrument/wmm/instrumenter_strategies.cpp
index 6acf938246e..925d9001940 100644
--- a/src/goto-instrument/wmm/instrumenter_strategies.cpp
+++ b/src/goto-instrument/wmm/instrumenter_strategies.cpp
@@ -81,11 +81,12 @@ void instrumentert::instrument_with_strategy(instrumentation_strategyt strategy)
 }
 
 void inline instrumentert::instrument_all_inserter(
-  const std::set<event_grapht::critical_cyclet> &set_of_cycles)
+  const std::set<event_grapht::critical_cyclet> &subset_of_cycles)
 {
-  for(std::set<event_grapht::critical_cyclet>::const_iterator
-    it=(set_of_cycles).begin();
-    it!=(set_of_cycles).end(); ++it)
+  for(std::set<event_grapht::critical_cyclet>::const_iterator it =
+        subset_of_cycles.begin();
+      it != subset_of_cycles.end();
+      ++it)
   {
     for(std::set<event_grapht::critical_cyclet::delayt>::const_iterator
       p_it=it->unsafe_pairs.begin();
@@ -109,15 +110,16 @@ void inline instrumentert::instrument_all_inserter(
 }
 
 void inline instrumentert::instrument_one_event_per_cycle_inserter(
-  const std::set<event_grapht::critical_cyclet> &set_of_cycles)
+  const std::set<event_grapht::critical_cyclet> &subset_of_cycles)
 {
   /* to keep track of the delayed pair, and to avoid the instrumentation
      of two pairs in a same cycle */
   std::set<event_grapht::critical_cyclet::delayt> delayed;
 
-  for(std::set<event_grapht::critical_cyclet>::iterator
-    it=set_of_cycles.begin();
-    it!=set_of_cycles.end(); ++it)
+  for(std::set<event_grapht::critical_cyclet>::iterator it =
+        subset_of_cycles.begin();
+      it != subset_of_cycles.end();
+      ++it)
   {
     /* cycle with already a delayed pair? */
     bool next=false;
@@ -189,7 +191,7 @@ unsigned inline instrumentert::cost(
 }
 
 void inline instrumentert::instrument_minimum_interference_inserter(
-  const std::set<event_grapht::critical_cyclet> &set_of_cycles)
+  const std::set<event_grapht::critical_cyclet> &subset_of_cycles)
 {
   /* Idea:
      We solve this by a linear programming approach,
@@ -216,10 +218,10 @@ void inline instrumentert::instrument_minimum_interference_inserter(
 #ifdef HAVE_GLPK
   /* first, identify all the unsafe pairs */
   std::set<event_grapht::critical_cyclet::delayt> edges;
-  for(std::set<event_grapht::critical_cyclet>::iterator
-    C_j=set_of_cycles.begin();
-    C_j!=set_of_cycles.end();
-    ++C_j)
+  for(std::set<event_grapht::critical_cyclet>::iterator C_j =
+        subset_of_cycles.begin();
+      C_j != subset_of_cycles.end();
+      ++C_j)
     for(std::set<event_grapht::critical_cyclet::delayt>::const_iterator e_i=
       C_j->unsafe_pairs.begin();
       e_i!=C_j->unsafe_pairs.end();
@@ -236,8 +238,8 @@ void inline instrumentert::instrument_minimum_interference_inserter(
   glp_set_prob_name(lp, "instrumentation optimisation");
   glp_set_obj_dir(lp, GLP_MIN);
 
-  message.debug() << "edges: "<<edges.size()<<" cycles:"<<set_of_cycles.size()
-    << messaget::eom;
+  message.debug() << "edges: " << edges.size()
+                  << " cycles:" << subset_of_cycles.size() << messaget::eom;
 
   /* sets the variables and coefficients */
   glp_add_cols(lp, edges.size());
@@ -256,12 +258,12 @@ void inline instrumentert::instrument_minimum_interference_inserter(
   }
 
   /* sets the constraints (soundness): one per cycle */
-  glp_add_rows(lp, set_of_cycles.size());
+  glp_add_rows(lp, subset_of_cycles.size());
   i=0;
-  for(std::set<event_grapht::critical_cyclet>::iterator
-    C_j=set_of_cycles.begin();
-    C_j!=set_of_cycles.end();
-    ++C_j)
+  for(std::set<event_grapht::critical_cyclet>::iterator C_j =
+        subset_of_cycles.begin();
+      C_j != subset_of_cycles.end();
+      ++C_j)
   {
     ++i;
     std::string name="C_"+std::to_string(i);
@@ -269,7 +271,7 @@ void inline instrumentert::instrument_minimum_interference_inserter(
     glp_set_row_bnds(lp, i, GLP_LO, 1.0, 0.0); /* >= 1*/
   }
 
-  const std::size_t mat_size=set_of_cycles.size()*edges.size();
+  const std::size_t mat_size = subset_of_cycles.size() * edges.size();
   message.debug() << "size of the system: " << mat_size
     << messaget::eom;
   std::vector<int> imat(mat_size+1);
@@ -287,10 +289,10 @@ void inline instrumentert::instrument_minimum_interference_inserter(
     ++e_i)
   {
     row=1;
-    for(std::set<event_grapht::critical_cyclet>::iterator
-      C_j=set_of_cycles.begin();
-      C_j!=set_of_cycles.end();
-      ++C_j)
+    for(std::set<event_grapht::critical_cyclet>::iterator C_j =
+          subset_of_cycles.begin();
+        C_j != subset_of_cycles.end();
+        ++C_j)
     {
       imat[i]=row;
       jmat[i]=col;
@@ -344,7 +346,7 @@ void inline instrumentert::instrument_minimum_interference_inserter(
 
   glp_delete_prob(lp);
 #else
-  (void)set_of_cycles; // unused parameter
+  (void)subset_of_cycles; // unused parameter
   throw "sorry, minimum interference option requires glpk; "
         "please recompile goto-instrument with glpk";
 #endif
diff --git a/src/goto-instrument/wmm/shared_buffers.cpp b/src/goto-instrument/wmm/shared_buffers.cpp
index 39964ab9841..0f140c9ed12 100644
--- a/src/goto-instrument/wmm/shared_buffers.cpp
+++ b/src/goto-instrument/wmm/shared_buffers.cpp
@@ -1021,7 +1021,6 @@ bool shared_bufferst::is_buffered_in_general(
 /// variables (non necessarily shared themselves) whose value could be changed
 /// as effect of a read delay
 void shared_bufferst::affected_by_delay(
-  symbol_tablet &symbol_table,
   value_setst &value_sets,
   goto_functionst &goto_functions)
 {
diff --git a/src/goto-instrument/wmm/shared_buffers.h b/src/goto-instrument/wmm/shared_buffers.h
index c9733b514fc..d80a600099f 100644
--- a/src/goto-instrument/wmm/shared_buffers.h
+++ b/src/goto-instrument/wmm/shared_buffers.h
@@ -184,7 +184,6 @@ class shared_bufferst
     goto_functionst &goto_functions);
 
   void affected_by_delay(
-    symbol_tablet &symbol_table,
     value_setst &value_sets,
     goto_functionst &goto_functions);
 
diff --git a/src/goto-instrument/wmm/weak_memory.cpp b/src/goto-instrument/wmm/weak_memory.cpp
index 08ffcf7dc0a..d9014c54d3d 100644
--- a/src/goto-instrument/wmm/weak_memory.cpp
+++ b/src/goto-instrument/wmm/weak_memory.cpp
@@ -222,8 +222,7 @@ void weak_memory(
   shared_buffers.cycles_r_loc = instrumenter.id2cycloc; // places in the cycles
 
   // for reads delays
-  shared_buffers.affected_by_delay(
-    goto_model.symbol_table, value_sets, goto_model.goto_functions);
+  shared_buffers.affected_by_delay(value_sets, goto_model.goto_functions);
 
   for(std::set<irep_idt>::iterator it=
     shared_buffers.affected_by_delay_set.begin();