diff --git a/jbmc/src/java_bytecode/java_bytecode_language.cpp b/jbmc/src/java_bytecode/java_bytecode_language.cpp
index 7d8ff0d17d3..a2cf076a131 100644
--- a/jbmc/src/java_bytecode/java_bytecode_language.cpp
+++ b/jbmc/src/java_bytecode/java_bytecode_language.cpp
@@ -165,23 +165,23 @@ std::set<std::string> java_bytecode_languaget::extensions() const
   return { "class", "jar" };
 }
 
-void java_bytecode_languaget::modules_provided(std::set<std::string> &modules)
+void java_bytecode_languaget::modules_provided(std::set<std::string> &)
 {
   // modules.insert(translation_unit(parse_path));
 }
 
 /// ANSI-C preprocessing
 bool java_bytecode_languaget::preprocess(
-  std::istream &instream,
-  const std::string &path,
-  std::ostream &outstream)
+  std::istream &,
+  const std::string &,
+  std::ostream &)
 {
   // there is no preprocessing!
   return true;
 }
 
 bool java_bytecode_languaget::parse(
-  std::istream &instream,
+  std::istream &,
   const std::string &path)
 {
   PRECONDITION(language_options_initialized);
@@ -601,7 +601,7 @@ static void create_stub_global_symbols(
 
 bool java_bytecode_languaget::typecheck(
   symbol_tablet &symbol_table,
-  const std::string &module)
+  const std::string &)
 {
   PRECONDITION(language_options_initialized);
 
@@ -1089,7 +1089,7 @@ bool java_bytecode_languaget::convert_single_method(
   return true;
 }
 
-bool java_bytecode_languaget::final(symbol_table_baset &symbol_table)
+bool java_bytecode_languaget::final(symbol_table_baset &)
 {
   PRECONDITION(language_options_initialized);
   return false;
diff --git a/jbmc/src/java_bytecode/java_types.h b/jbmc/src/java_bytecode/java_types.h
index c0d07df88fa..cfd847eaa65 100644
--- a/jbmc/src/java_bytecode/java_types.h
+++ b/jbmc/src/java_bytecode/java_types.h
@@ -93,7 +93,7 @@ inline annotated_typet &to_annotated_type(typet &type)
 }
 
 template <>
-inline bool can_cast_type<annotated_typet>(const typet &type)
+inline bool can_cast_type<annotated_typet>(const typet &)
 {
   return true;
 }
diff --git a/jbmc/src/java_bytecode/remove_exceptions.cpp b/jbmc/src/java_bytecode/remove_exceptions.cpp
index 41aaef59ac0..4ac6aa5ae95 100644
--- a/jbmc/src/java_bytecode/remove_exceptions.cpp
+++ b/jbmc/src/java_bytecode/remove_exceptions.cpp
@@ -616,7 +616,7 @@ void remove_exceptions(
   remove_exceptions_typest type)
 {
   remove_exceptionst::function_may_throwt any_function_may_throw =
-    [](const irep_idt &id) { return true; };
+    [](const irep_idt &) { return true; };
 
   remove_exceptionst remove_exceptions(
     symbol_table,
diff --git a/src/analyses/ai.cpp b/src/analyses/ai.cpp
index c12c1f4d0a3..9e317bc1447 100644
--- a/src/analyses/ai.cpp
+++ b/src/analyses/ai.cpp
@@ -319,7 +319,7 @@ bool ai_baset::do_function_call(
   locationt l_call, locationt l_return,
   const goto_functionst &goto_functions,
   const goto_functionst::function_mapt::const_iterator f_it,
-  const exprt::operandst &arguments,
+  const exprt::operandst &,
   const namespacet &ns)
 {
   // initialize state, if necessary
diff --git a/src/analyses/ai.h b/src/analyses/ai.h
index e2f3a4d83a4..ad75eed8d73 100644
--- a/src/analyses/ai.h
+++ b/src/analyses/ai.h
@@ -385,10 +385,10 @@ class ait:public ai_baset
 
   // not implemented in sequential analyses
   bool merge_shared(
-    const statet &src,
-    goto_programt::const_targett from,
-    goto_programt::const_targett to,
-    const namespacet &ns) override
+    const statet &,
+    goto_programt::const_targett,
+    goto_programt::const_targett,
+    const namespacet &) override
   {
     throw "not implemented";
   }
diff --git a/src/analyses/constant_propagator.cpp b/src/analyses/constant_propagator.cpp
index b6bb6688f62..e81badbfe1c 100644
--- a/src/analyses/constant_propagator.cpp
+++ b/src/analyses/constant_propagator.cpp
@@ -224,7 +224,7 @@ void constant_propagator_domaint::transform(
 /// handles equalities and conjunctions containing equalities
 bool constant_propagator_domaint::two_way_propagate_rec(
   const exprt &expr,
-  const namespacet &ns,
+  const namespacet &,
   const constant_propagator_ait *cp)
 {
 #ifdef DEBUG
@@ -391,7 +391,7 @@ void constant_propagator_domaint::valuest::output(
 
 void constant_propagator_domaint::output(
   std::ostream &out,
-  const ai_baset &ai,
+  const ai_baset &,
   const namespacet &ns) const
 {
   values.output(out, ns);
@@ -503,8 +503,8 @@ bool constant_propagator_domaint::valuest::meet(const valuest &src)
 /// \return Return true if "this" has changed.
 bool constant_propagator_domaint::merge(
   const constant_propagator_domaint &other,
-  locationt from,
-  locationt to)
+  locationt,
+  locationt)
 {
   return values.merge(other.values);
 }
diff --git a/src/analyses/custom_bitvector_analysis.cpp b/src/analyses/custom_bitvector_analysis.cpp
index cf19a7aa895..059756107e4 100644
--- a/src/analyses/custom_bitvector_analysis.cpp
+++ b/src/analyses/custom_bitvector_analysis.cpp
@@ -545,7 +545,7 @@ void custom_bitvector_domaint::transform(
 void custom_bitvector_domaint::output(
   std::ostream &out,
   const ai_baset &ai,
-  const namespacet &ns) const
+  const namespacet &) const
 {
   if(has_values.is_known())
   {
@@ -591,8 +591,8 @@ void custom_bitvector_domaint::output(
 
 bool custom_bitvector_domaint::merge(
   const custom_bitvector_domaint &b,
-  locationt from,
-  locationt to)
+  locationt,
+  locationt)
 {
   bool changed=has_values.is_false();
   has_values=tvt::unknown();
diff --git a/src/analyses/dependence_graph.cpp b/src/analyses/dependence_graph.cpp
index 24c0320af66..df9874371bb 100644
--- a/src/analyses/dependence_graph.cpp
+++ b/src/analyses/dependence_graph.cpp
@@ -24,8 +24,8 @@ Date: August 2013
 
 bool dep_graph_domaint::merge(
   const dep_graph_domaint &src,
-  goto_programt::const_targett from,
-  goto_programt::const_targett to)
+  goto_programt::const_targett,
+  goto_programt::const_targett)
 {
   // An abstract state at location `to` may be non-bottom even if
   // `merge(..., `to`) has not been called so far. This is due to the special
@@ -151,7 +151,7 @@ static bool may_be_def_use_pair(
 }
 
 void dep_graph_domaint::data_dependencies(
-  goto_programt::const_targett from,
+  goto_programt::const_targett,
   goto_programt::const_targett to,
   dependence_grapht &dep_graph,
   const namespacet &ns)
@@ -237,8 +237,8 @@ void dep_graph_domaint::transform(
 
 void dep_graph_domaint::output(
   std::ostream &out,
-  const ai_baset &ai,
-  const namespacet &ns) const
+  const ai_baset &,
+  const namespacet &) const
 {
   if(!control_deps.empty())
   {
@@ -275,8 +275,8 @@ void dep_graph_domaint::output(
 /// \par parameters: The abstract interpreter and the namespace.
 /// \return The domain, formatted as a JSON object.
 jsont dep_graph_domaint::output_json(
-  const ai_baset &ai,
-  const namespacet &ns) const
+  const ai_baset &,
+  const namespacet &) const
 {
   json_arrayt graph;
 
diff --git a/src/analyses/escape_analysis.cpp b/src/analyses/escape_analysis.cpp
index 1598b9ededa..cd2d297df4a 100644
--- a/src/analyses/escape_analysis.cpp
+++ b/src/analyses/escape_analysis.cpp
@@ -163,9 +163,9 @@ void escape_domaint::get_rhs_aliases_address_of(
 
 void escape_domaint::transform(
   locationt from,
-  locationt to,
-  ai_baset &ai,
-  const namespacet &ns)
+  locationt,
+  ai_baset &,
+  const namespacet &)
 {
   if(has_values.is_false())
     return;
@@ -255,8 +255,8 @@ void escape_domaint::transform(
 
 void escape_domaint::output(
   std::ostream &out,
-  const ai_baset &ai,
-  const namespacet &ns) const
+  const ai_baset &,
+  const namespacet &) const
 {
   if(has_values.is_known())
   {
@@ -301,8 +301,8 @@ void escape_domaint::output(
 
 bool escape_domaint::merge(
   const escape_domaint &b,
-  locationt from,
-  locationt to)
+  locationt,
+  locationt)
 {
   bool changed=has_values.is_false();
   has_values=tvt::unknown();
diff --git a/src/analyses/escape_analysis.h b/src/analyses/escape_analysis.h
index bbf05973b13..1ea16879a10 100644
--- a/src/analyses/escape_analysis.h
+++ b/src/analyses/escape_analysis.h
@@ -112,7 +112,7 @@ class escape_analysist:public ait<escape_domaint>
   void instrument(goto_modelt &);
 
 protected:
-  virtual void initialize(const goto_functionst &_goto_functions)
+  virtual void initialize(const goto_functionst &)
   {
   }
 
diff --git a/src/analyses/flow_insensitive_analysis.cpp b/src/analyses/flow_insensitive_analysis.cpp
index a91186a84c3..15204ee1c90 100644
--- a/src/analyses/flow_insensitive_analysis.cpp
+++ b/src/analyses/flow_insensitive_analysis.cpp
@@ -77,8 +77,8 @@ void flow_insensitive_analysis_baset::output(
 }
 
 void flow_insensitive_analysis_baset::output(
-  const goto_programt &goto_program,
-  const irep_idt &identifier,
+  const goto_programt &,
+  const irep_idt &,
   std::ostream &out) const
 {
   get_state().output(ns, out);
@@ -199,7 +199,7 @@ bool flow_insensitive_analysis_baset::do_function_call(
   locationt l_call,
   const goto_functionst &goto_functions,
   const goto_functionst::function_mapt::const_iterator f_it,
-  const exprt::operandst &arguments,
+  const exprt::operandst &,
   statet &state)
 {
   const goto_functionst::goto_functiont &goto_function=f_it->second;
@@ -405,14 +405,12 @@ bool flow_insensitive_analysis_baset::fixedpoint(
   return fixedpoint(it->second.body, goto_functions);
 }
 
-void flow_insensitive_analysis_baset::update(
-  const goto_functionst &goto_functions)
+void flow_insensitive_analysis_baset::update(const goto_functionst &)
 {
   // no need to copy value sets around
 }
 
-void flow_insensitive_analysis_baset::update(
-  const goto_programt &goto_program)
+void flow_insensitive_analysis_baset::update(const goto_programt &)
 {
   // no need to copy value sets around
 }
diff --git a/src/analyses/flow_insensitive_analysis.h b/src/analyses/flow_insensitive_analysis.h
index b2f1553c6f0..04b19c2d9b3 100644
--- a/src/analyses/flow_insensitive_analysis.h
+++ b/src/analyses/flow_insensitive_analysis.h
@@ -44,16 +44,16 @@ class flow_insensitive_abstract_domain_baset
   }
 
   virtual void output(
-    const namespacet &ns,
-    std::ostream &out) const
+    const namespacet &,
+    std::ostream &) const
   {
   }
 
   typedef std::unordered_set<exprt, irep_hash> expr_sett;
 
   virtual void get_reference_set(
-    const namespacet &ns,
-    const exprt &expr,
+    const namespacet &,
+    const exprt &,
     expr_sett &expr_set)
   {
     // dummy, overload me!
@@ -95,8 +95,7 @@ class flow_insensitive_analysis_baset
   {
   }
 
-  virtual void initialize(
-    const goto_programt &goto_program)
+  virtual void initialize(const goto_programt &)
   {
     if(!initialized)
     {
@@ -104,8 +103,7 @@ class flow_insensitive_analysis_baset
     }
   }
 
-  virtual void initialize(
-    const goto_functionst &goto_functions)
+  virtual void initialize(const goto_functionst &)
   {
     if(!initialized)
     {
diff --git a/src/analyses/global_may_alias.cpp b/src/analyses/global_may_alias.cpp
index 82c1f5a72dc..ce823ab9a66 100644
--- a/src/analyses/global_may_alias.cpp
+++ b/src/analyses/global_may_alias.cpp
@@ -77,9 +77,9 @@ void global_may_alias_domaint::get_rhs_aliases_address_of(
 
 void global_may_alias_domaint::transform(
   locationt from,
-  locationt to,
-  ai_baset &ai,
-  const namespacet &ns)
+  locationt,
+  ai_baset &,
+  const namespacet &)
 {
   if(has_values.is_false())
     return;
@@ -120,8 +120,8 @@ void global_may_alias_domaint::transform(
 
 void global_may_alias_domaint::output(
   std::ostream &out,
-  const ai_baset &ai,
-  const namespacet &ns) const
+  const ai_baset &,
+  const namespacet &) const
 {
   if(has_values.is_known())
   {
@@ -158,8 +158,8 @@ void global_may_alias_domaint::output(
 
 bool global_may_alias_domaint::merge(
   const global_may_alias_domaint &b,
-  locationt from,
-  locationt to)
+  locationt,
+  locationt)
 {
   bool changed=has_values.is_false();
   has_values=tvt::unknown();
diff --git a/src/analyses/global_may_alias.h b/src/analyses/global_may_alias.h
index b8f3480bb1c..2d7491d0ada 100644
--- a/src/analyses/global_may_alias.h
+++ b/src/analyses/global_may_alias.h
@@ -87,7 +87,7 @@ class global_may_alias_domaint:public ai_domain_baset
 class global_may_alias_analysist:public ait<global_may_alias_domaint>
 {
 protected:
-  virtual void initialize(const goto_functionst &_goto_functions)
+  virtual void initialize(const goto_functionst &)
   {
   }
 };
diff --git a/src/analyses/goto_rw.cpp b/src/analyses/goto_rw.cpp
index 61e7467669b..3d3fd80f1f1 100644
--- a/src/analyses/goto_rw.cpp
+++ b/src/analyses/goto_rw.cpp
@@ -34,8 +34,7 @@ range_domain_baset::~range_domain_baset()
 {
 }
 
-void range_domaint::output(
-  const namespacet &ns, std::ostream &out) const
+void range_domaint::output(const namespacet &, std::ostream &out) const
 {
   out << "[";
   for(const_iterator itr=begin();
@@ -123,8 +122,8 @@ void rw_range_sett::get_objects_if(
 void rw_range_sett::get_objects_dereference(
   get_modet mode,
   const dereference_exprt &deref,
-  const range_spect &range_start,
-  const range_spect &size)
+  const range_spect &,
+  const range_spect &)
 {
   const exprt &pointer=deref.pointer();
   get_objects_rec(get_modet::READ, pointer);
diff --git a/src/analyses/goto_rw.h b/src/analyses/goto_rw.h
index d84c6da1964..dd6c9e63c33 100644
--- a/src/analyses/goto_rw.h
+++ b/src/analyses/goto_rw.h
@@ -141,7 +141,7 @@ class rw_range_sett
   enum class get_modet { LHS_W, READ };
 
   virtual void get_objects_rec(
-    goto_programt::const_targett _target,
+    goto_programt::const_targett,
     get_modet mode,
     const exprt &expr)
   {
diff --git a/src/analyses/interval_domain.cpp b/src/analyses/interval_domain.cpp
index bdf1ccec09a..3e0db34c306 100644
--- a/src/analyses/interval_domain.cpp
+++ b/src/analyses/interval_domain.cpp
@@ -22,8 +22,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 void interval_domaint::output(
   std::ostream &out,
-  const ai_baset &ai,
-  const namespacet &ns) const
+  const ai_baset &,
+  const namespacet &) const
 {
   if(bottom)
   {
@@ -59,7 +59,7 @@ void interval_domaint::output(
 void interval_domaint::transform(
   locationt from,
   locationt to,
-  ai_baset &ai,
+  ai_baset &,
   const namespacet &ns)
 {
   const goto_programt::instructiont &instruction=*from;
diff --git a/src/analyses/interval_domain.h b/src/analyses/interval_domain.h
index f94236861e6..15c75e455d7 100644
--- a/src/analyses/interval_domain.h
+++ b/src/analyses/interval_domain.h
@@ -47,8 +47,8 @@ class interval_domaint:public ai_domain_baset
 public:
   bool merge(
     const interval_domaint &b,
-    locationt from,
-    locationt to)
+    locationt,
+    locationt)
   {
     return join(b);
   }
diff --git a/src/analyses/invariant_set.cpp b/src/analyses/invariant_set.cpp
index 8c4afe661b4..540e90e10ef 100644
--- a/src/analyses/invariant_set.cpp
+++ b/src/analyses/invariant_set.cpp
@@ -884,7 +884,7 @@ exprt invariant_sett::get_constant(const exprt &expr) const
 
 std::string inv_object_storet::to_string(
   unsigned a,
-  const irep_idt &identifier) const
+  const irep_idt &) const
 {
   return id2string(map[a]);
 }
diff --git a/src/analyses/invariant_set_domain.cpp b/src/analyses/invariant_set_domain.cpp
index 1e1015eb404..f7a524e7554 100644
--- a/src/analyses/invariant_set_domain.cpp
+++ b/src/analyses/invariant_set_domain.cpp
@@ -16,7 +16,7 @@ Author: Daniel Kroening, kroening@kroening.com
 void invariant_set_domaint::transform(
   locationt from_l,
   locationt to_l,
-  ai_baset &ai,
+  ai_baset &,
   const namespacet &ns)
 {
   switch(from_l->type)
diff --git a/src/analyses/invariant_set_domain.h b/src/analyses/invariant_set_domain.h
index 367e987c709..94a09a40ff3 100644
--- a/src/analyses/invariant_set_domain.h
+++ b/src/analyses/invariant_set_domain.h
@@ -31,8 +31,8 @@ class invariant_set_domaint:public ai_domain_baset
 
   bool merge(
     const invariant_set_domaint &other,
-    locationt from,
-    locationt to)
+    locationt,
+    locationt)
   {
     bool changed=invariant_set.make_union(other.invariant_set) ||
                  has_values.is_false();
@@ -43,8 +43,8 @@ class invariant_set_domaint:public ai_domain_baset
 
   void output(
     std::ostream &out,
-    const ai_baset &ai,
-    const namespacet &ns) const final override
+    const ai_baset &,
+    const namespacet &) const final override
   {
     if(has_values.is_known())
       out << has_values.to_string() << '\n';
diff --git a/src/analyses/is_threaded.cpp b/src/analyses/is_threaded.cpp
index ca1ddff4718..c48edd1113d 100644
--- a/src/analyses/is_threaded.cpp
+++ b/src/analyses/is_threaded.cpp
@@ -30,8 +30,8 @@ class is_threaded_domaint:public ai_domain_baset
 
   bool merge(
     const is_threaded_domaint &src,
-    locationt from,
-    locationt to)
+    locationt,
+    locationt)
   {
     INVARIANT(src.reachable,
               "Abstract states are only merged at reachable locations");
@@ -47,7 +47,7 @@ class is_threaded_domaint:public ai_domain_baset
   }
 
   void
-  transform(locationt from, locationt to, ai_baset &ai, const namespacet &ns)
+  transform(locationt from, locationt, ai_baset &, const namespacet &)
     final override
   {
     INVARIANT(reachable,
diff --git a/src/analyses/reaching_definitions.cpp b/src/analyses/reaching_definitions.cpp
index 7788835f0db..fad39334e0b 100644
--- a/src/analyses/reaching_definitions.cpp
+++ b/src/analyses/reaching_definitions.cpp
@@ -125,7 +125,7 @@ void rd_range_domaint::transform(
 }
 
 void rd_range_domaint::transform_dead(
-  const namespacet &ns,
+  const namespacet &,
   locationt from)
 {
   const irep_idt &identifier=
@@ -430,7 +430,7 @@ void rd_range_domaint::kill(
 }
 
 void rd_range_domaint::kill_inf(
-  const irep_idt &identifier,
+  const irep_idt &,
   const range_spect &range_start)
 {
   assert(range_start>=0);
@@ -628,8 +628,8 @@ bool rd_range_domaint::merge_inner(
 /// \return returns true iff there is something new
 bool rd_range_domaint::merge(
   const rd_range_domaint &other,
-  locationt from,
-  locationt to)
+  locationt,
+  locationt)
 {
   bool changed=has_values.is_false();
   has_values=tvt::unknown();
@@ -664,8 +664,8 @@ bool rd_range_domaint::merge(
 /// \return returns true iff there is something new
 bool rd_range_domaint::merge_shared(
   const rd_range_domaint &other,
-  goto_programt::const_targett from,
-  goto_programt::const_targett to,
+  goto_programt::const_targett,
+  goto_programt::const_targett,
   const namespacet &ns)
 {
   // TODO: dirty vars
diff --git a/src/analyses/reaching_definitions.h b/src/analyses/reaching_definitions.h
index 133f81ab04f..a4fd7702367 100644
--- a/src/analyses/reaching_definitions.h
+++ b/src/analyses/reaching_definitions.h
@@ -119,8 +119,8 @@ class rd_range_domaint:public ai_domain_baset
 
   void output(
     std::ostream &out,
-    const ai_baset &ai,
-    const namespacet &ns) const final override
+    const ai_baset &,
+    const namespacet &) const final override
   {
     output(out);
   }
diff --git a/src/analyses/static_analysis.cpp b/src/analyses/static_analysis.cpp
index 32504c7c4e1..8c239046d29 100644
--- a/src/analyses/static_analysis.cpp
+++ b/src/analyses/static_analysis.cpp
@@ -93,7 +93,7 @@ void static_analysis_baset::output(
 
 void static_analysis_baset::output(
   const goto_programt &goto_program,
-  const irep_idt &identifier,
+  const irep_idt &,
   std::ostream &out) const
 {
   forall_goto_program_instructions(i_it, goto_program)
@@ -248,7 +248,7 @@ void static_analysis_baset::do_function_call(
   locationt l_call, locationt l_return,
   const goto_functionst &goto_functions,
   const goto_functionst::function_mapt::const_iterator f_it,
-  const exprt::operandst &arguments,
+  const exprt::operandst &,
   statet &new_state)
 {
   const goto_functionst::goto_functiont &goto_function=f_it->second;
diff --git a/src/analyses/static_analysis.h b/src/analyses/static_analysis.h
index 405c6509bdc..805824f00f1 100644
--- a/src/analyses/static_analysis.h
+++ b/src/analyses/static_analysis.h
@@ -43,8 +43,8 @@ class domain_baset
   // will go away,
   // to be replaced by a factory class option to static_analysist
   virtual void initialize(
-    const namespacet &ns,
-    locationt l)
+    const namespacet &,
+    locationt)
   {
   }
 
@@ -62,8 +62,8 @@ class domain_baset
     locationt to)=0;
 
   virtual void output(
-    const namespacet &ns,
-    std::ostream &out) const
+    const namespacet &,
+    std::ostream &) const
   {
   }
 
@@ -71,8 +71,8 @@ class domain_baset
 
   // will go away
   virtual void get_reference_set(
-    const namespacet &ns,
-    const exprt &expr,
+    const namespacet &,
+    const exprt &,
     std::list<exprt> &dest)
   {
     // dummy, overload me!
@@ -363,9 +363,9 @@ class static_analysist:public static_analysis_baset
 
   // not implemented in sequential analyses
   virtual bool merge_shared(
-    statet &a,
-    const statet &b,
-    goto_programt::const_targett to)
+    statet &,
+    const statet &,
+    goto_programt::const_targett)
   {
     throw "not implemented";
   }
diff --git a/src/analyses/uncaught_exceptions_analysis.cpp b/src/analyses/uncaught_exceptions_analysis.cpp
index 21e4c47ec67..851df00bc7f 100644
--- a/src/analyses/uncaught_exceptions_analysis.cpp
+++ b/src/analyses/uncaught_exceptions_analysis.cpp
@@ -59,7 +59,7 @@ void uncaught_exceptions_domaint::join(
 void uncaught_exceptions_domaint::transform(
   const goto_programt::const_targett from,
   uncaught_exceptions_analysist &uea,
-  const namespacet &ns)
+  const namespacet &)
 {
   const goto_programt::instructiont &instruction=*from;
 
diff --git a/src/analyses/uninitialized_domain.cpp b/src/analyses/uninitialized_domain.cpp
index 5cff1d3f0b9..04c0bb8d0fa 100644
--- a/src/analyses/uninitialized_domain.cpp
+++ b/src/analyses/uninitialized_domain.cpp
@@ -20,8 +20,8 @@ Date: January 2010
 
 void uninitialized_domaint::transform(
   locationt from,
-  locationt to,
-  ai_baset &ai,
+  locationt,
+  ai_baset &,
   const namespacet &ns)
 {
   if(has_values.is_false())
@@ -67,8 +67,8 @@ void uninitialized_domaint::assign(const exprt &lhs)
 
 void uninitialized_domaint::output(
   std::ostream &out,
-  const ai_baset &ai,
-  const namespacet &ns) const
+  const ai_baset &,
+  const namespacet &) const
 {
   if(has_values.is_known())
     out << has_values.to_string() << '\n';
@@ -82,8 +82,8 @@ void uninitialized_domaint::output(
 /// \return returns true iff there is something new
 bool uninitialized_domaint::merge(
   const uninitialized_domaint &other,
-  locationt from,
-  locationt to)
+  locationt,
+  locationt)
 {
   auto old_uninitialized=uninitialized.size();
 
diff --git a/src/ansi-c/ansi_c_language.cpp b/src/ansi-c/ansi_c_language.cpp
index fc412f0387e..ae4c8f62f02 100644
--- a/src/ansi-c/ansi_c_language.cpp
+++ b/src/ansi-c/ansi_c_language.cpp
@@ -180,7 +180,7 @@ bool ansi_c_languaget::type_to_name(
 
 bool ansi_c_languaget::to_expr(
   const std::string &code,
-  const std::string &module,
+  const std::string &,
   exprt &expr,
   const namespacet &ns)
 {
diff --git a/src/ansi-c/c_typecheck_code.cpp b/src/ansi-c/c_typecheck_code.cpp
index be2d711416d..45ca0720e39 100644
--- a/src/ansi-c/c_typecheck_code.cpp
+++ b/src/ansi-c/c_typecheck_code.cpp
@@ -565,7 +565,7 @@ void c_typecheck_baset::typecheck_gcc_switch_case_range(codet &code)
   make_constant(code.op1());
 }
 
-void c_typecheck_baset::typecheck_gcc_local_label(codet &code)
+void c_typecheck_baset::typecheck_gcc_local_label(codet &)
 {
   // these are just declarations, e.g.,
   // __label__ here, there;
diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp
index b8b0e7fe595..027d7f287d4 100644
--- a/src/ansi-c/c_typecheck_expr.cpp
+++ b/src/ansi-c/c_typecheck_expr.cpp
@@ -2797,7 +2797,7 @@ void c_typecheck_baset::typecheck_function_call_arguments(
   }
 }
 
-void c_typecheck_baset::typecheck_expr_constant(exprt &expr)
+void c_typecheck_baset::typecheck_expr_constant(exprt &)
 {
   // nothing to do
 }
diff --git a/src/cpp/cpp_declarator_converter.cpp b/src/cpp/cpp_declarator_converter.cpp
index 880d05fe2ef..cf446a620c3 100644
--- a/src/cpp/cpp_declarator_converter.cpp
+++ b/src/cpp/cpp_declarator_converter.cpp
@@ -582,7 +582,7 @@ irep_idt cpp_declarator_convertert::get_pretty_name()
 }
 
 void cpp_declarator_convertert::operator_overloading_rules(
-  const symbolt &symbol)
+  const symbolt &)
 {
 }
 
diff --git a/src/cpp/cpp_language.cpp b/src/cpp/cpp_language.cpp
index e47d887d292..f00fbbceaea 100644
--- a/src/cpp/cpp_language.cpp
+++ b/src/cpp/cpp_language.cpp
@@ -229,7 +229,7 @@ bool cpp_languaget::from_type(
 bool cpp_languaget::type_to_name(
   const typet &type,
   std::string &name,
-  const namespacet &ns)
+  const namespacet &)
 {
   name=cpp_type2name(type);
   return false;
@@ -237,7 +237,7 @@ bool cpp_languaget::type_to_name(
 
 bool cpp_languaget::to_expr(
   const std::string &code,
-  const std::string &module,
+  const std::string &,
   exprt &expr,
   const namespacet &ns)
 {
diff --git a/src/cpp/cpp_typecheck.h b/src/cpp/cpp_typecheck.h
index 0f5431acbdd..08e078017e8 100644
--- a/src/cpp/cpp_typecheck.h
+++ b/src/cpp/cpp_typecheck.h
@@ -379,7 +379,7 @@ class cpp_typecheckt:public c_typecheck_baset
 
   void put_compound_into_scope(const struct_union_typet::componentt &component);
   void typecheck_compound_body(symbolt &symbol);
-  void typecheck_compound_body(struct_union_typet &type) { UNREACHABLE; }
+  void typecheck_compound_body(struct_union_typet &) { UNREACHABLE; }
   void typecheck_enum_body(symbolt &symbol);
   void typecheck_method_bodies();
   void typecheck_compound_bases(struct_typet &type);
diff --git a/src/cpp/cpp_typecheck_expr.cpp b/src/cpp/cpp_typecheck_expr.cpp
index 2ffd3524407..df8d3049092 100644
--- a/src/cpp/cpp_typecheck_expr.cpp
+++ b/src/cpp/cpp_typecheck_expr.cpp
@@ -1084,7 +1084,7 @@ void cpp_typecheckt::typecheck_expr_delete(exprt &expr)
   expr.set(ID_destructor, destructor_code);
 }
 
-void cpp_typecheckt::typecheck_expr_typecast(exprt &expr)
+void cpp_typecheckt::typecheck_expr_typecast(exprt &)
 {
   // should not be called
   #if 0
diff --git a/src/goto-cc/linker_script_merge.cpp b/src/goto-cc/linker_script_merge.cpp
index 469eb64ffdf..6244b998993 100644
--- a/src/goto-cc/linker_script_merge.cpp
+++ b/src/goto-cc/linker_script_merge.cpp
@@ -129,7 +129,7 @@ linker_script_merget::linker_script_merget(
       replacement_predicatet("address of array's first member",
         [](const exprt &expr) -> const symbol_exprt&
         { return to_symbol_expr(expr.op0().op0()); },
-        [](const exprt &expr, const namespacet &ns)
+        [](const exprt &expr, const namespacet &)
         {
           return expr.id()==ID_address_of &&
                  expr.type().id()==ID_pointer &&
@@ -146,7 +146,7 @@ linker_script_merget::linker_script_merget(
       replacement_predicatet("address of array",
         [](const exprt &expr) -> const symbol_exprt&
         { return to_symbol_expr(expr.op0()); },
-        [](const exprt &expr, const namespacet &ns)
+        [](const exprt &expr, const namespacet &)
         {
           return expr.id()==ID_address_of &&
                  expr.type().id()==ID_pointer &&
@@ -168,7 +168,7 @@ linker_script_merget::linker_script_merget(
       replacement_predicatet("array variable",
         [](const exprt &expr) -> const symbol_exprt&
         { return to_symbol_expr(expr); },
-        [](const exprt &expr, const namespacet &ns)
+        [](const exprt &expr, const namespacet &)
         {
           return expr.id()==ID_symbol &&
                  expr.type().id()==ID_array;
@@ -176,7 +176,7 @@ linker_script_merget::linker_script_merget(
       replacement_predicatet("pointer (does not need pointerizing)",
         [](const exprt &expr) -> const symbol_exprt&
         { return to_symbol_expr(expr); },
-        [](const exprt &expr, const namespacet &ns)
+        [](const exprt &expr, const namespacet &)
         {
           return expr.id()==ID_symbol &&
                  expr.type().id()==ID_pointer;
diff --git a/src/goto-instrument/accelerate/accelerate.cpp b/src/goto-instrument/accelerate/accelerate.cpp
index 639abfefd58..355a6065191 100644
--- a/src/goto-instrument/accelerate/accelerate.cpp
+++ b/src/goto-instrument/accelerate/accelerate.cpp
@@ -457,7 +457,7 @@ symbolt acceleratet::make_symbol(std::string name, typet type)
   return ret;
 }
 
-void acceleratet::decl(symbol_exprt &sym, goto_programt::targett t)
+void acceleratet::decl(symbol_exprt &, goto_programt::targett)
 {
 #if 0
   goto_programt::targett decl=program.insert_before(t);
diff --git a/src/goto-instrument/cover_instrument_condition.cpp b/src/goto-instrument/cover_instrument_condition.cpp
index 32ed359654e..fa4f2f5e949 100644
--- a/src/goto-instrument/cover_instrument_condition.cpp
+++ b/src/goto-instrument/cover_instrument_condition.cpp
@@ -19,7 +19,7 @@ Author: Daniel Kroening
 void cover_condition_instrumentert::instrument(
   goto_programt &goto_program,
   goto_programt::targett &i_it,
-  const cover_blocks_baset &basic_blocks) const
+  const cover_blocks_baset &) const
 {
   if(is_non_cover_assertion(i_it))
     i_it->make_skip();
diff --git a/src/goto-instrument/cover_instrument_decision.cpp b/src/goto-instrument/cover_instrument_decision.cpp
index 5427f38bff0..a144656e126 100644
--- a/src/goto-instrument/cover_instrument_decision.cpp
+++ b/src/goto-instrument/cover_instrument_decision.cpp
@@ -18,7 +18,7 @@ Author: Daniel Kroening
 void cover_decision_instrumentert::instrument(
   goto_programt &goto_program,
   goto_programt::targett &i_it,
-  const cover_blocks_baset &basic_blocks) const
+  const cover_blocks_baset &) const
 {
   if(is_non_cover_assertion(i_it))
     i_it->make_skip();
diff --git a/src/goto-instrument/cover_instrument_mcdc.cpp b/src/goto-instrument/cover_instrument_mcdc.cpp
index c5d58c962e0..e1b1ab7a52f 100644
--- a/src/goto-instrument/cover_instrument_mcdc.cpp
+++ b/src/goto-instrument/cover_instrument_mcdc.cpp
@@ -623,7 +623,7 @@ void minimize_mcdc_controlling(
 void cover_mcdc_instrumentert::instrument(
   goto_programt &goto_program,
   goto_programt::targett &i_it,
-  const cover_blocks_baset &basic_blocks) const
+  const cover_blocks_baset &) const
 {
   if(is_non_cover_assertion(i_it))
     i_it->make_skip();
diff --git a/src/goto-instrument/cover_instrument_other.cpp b/src/goto-instrument/cover_instrument_other.cpp
index e7d0795d7f7..ee33b8975d9 100644
--- a/src/goto-instrument/cover_instrument_other.cpp
+++ b/src/goto-instrument/cover_instrument_other.cpp
@@ -16,9 +16,9 @@ Author: Daniel Kroening
 #include "cover_util.h"
 
 void cover_path_instrumentert::instrument(
-  goto_programt &goto_program,
+  goto_programt &,
   goto_programt::targett &i_it,
-  const cover_blocks_baset &basic_blocks) const
+  const cover_blocks_baset &) const
 {
   if(is_non_cover_assertion(i_it))
     i_it->make_skip();
@@ -27,9 +27,9 @@ void cover_path_instrumentert::instrument(
 }
 
 void cover_assertion_instrumentert::instrument(
-  goto_programt &goto_program,
+  goto_programt &,
   goto_programt::targett &i_it,
-  const cover_blocks_baset &basic_blocks) const
+  const cover_blocks_baset &) const
 {
   // turn into 'assert(false)' to avoid simplification
   if(is_non_cover_assertion(i_it))
@@ -41,9 +41,9 @@ void cover_assertion_instrumentert::instrument(
 }
 
 void cover_cover_instrumentert::instrument(
-  goto_programt &goto_program,
+  goto_programt &,
   goto_programt::targett &i_it,
-  const cover_blocks_baset &basic_blocks) const
+  const cover_blocks_baset &) const
 {
   // turn __CPROVER_cover(x) into 'assert(!x)'
   if(i_it->is_function_call())
diff --git a/src/goto-instrument/goto_program2code.cpp b/src/goto-instrument/goto_program2code.cpp
index 5f8a4b00c74..6bda908a4bd 100644
--- a/src/goto-instrument/goto_program2code.cpp
+++ b/src/goto-instrument/goto_program2code.cpp
@@ -1403,7 +1403,7 @@ goto_programt::const_targett goto_program2codet::convert_start_thread(
 
 goto_programt::const_targett goto_program2codet::convert_throw(
     goto_programt::const_targett target,
-    codet &dest)
+    codet &)
 {
   // this isn't really clear as throw is not supported in expr2cpp either
   UNREACHABLE;
@@ -1412,8 +1412,8 @@ goto_programt::const_targett goto_program2codet::convert_throw(
 
 goto_programt::const_targett goto_program2codet::convert_catch(
     goto_programt::const_targett target,
-    goto_programt::const_targett upper_bound,
-    codet &dest)
+    goto_programt::const_targett,
+    codet &)
 {
   // this isn't really clear as catch is not supported in expr2cpp either
   UNREACHABLE;
diff --git a/src/goto-instrument/horn_encoding.cpp b/src/goto-instrument/horn_encoding.cpp
index bccce9a0580..7b2fe7bcb51 100644
--- a/src/goto-instrument/horn_encoding.cpp
+++ b/src/goto-instrument/horn_encoding.cpp
@@ -17,6 +17,6 @@ Date: June 2015
 
 void horn_encoding(
   const goto_modelt &,
-  std::ostream &out)
+  std::ostream &)
 {
 }
diff --git a/src/goto-instrument/rw_set.h b/src/goto-instrument/rw_set.h
index ead8d0e8c7f..1c5e9fdb66b 100644
--- a/src/goto-instrument/rw_set.h
+++ b/src/goto-instrument/rw_set.h
@@ -87,7 +87,7 @@ class rw_set_baset
   void output(std::ostream &out) const;
 
 protected:
-  virtual void track_deref(const entryt &entry, bool read) {}
+  virtual void track_deref(const entryt &, bool read) {}
   virtual void set_track_deref() {}
   virtual void reset_track_deref() {}
 
diff --git a/src/goto-instrument/wmm/event_graph.h b/src/goto-instrument/wmm/event_graph.h
index 190e6e87514..e963ec3ef70 100644
--- a/src/goto-instrument/wmm/event_graph.h
+++ b/src/goto-instrument/wmm/event_graph.h
@@ -267,7 +267,7 @@ class event_grapht
     std::map<unsigned, unsigned char> events_per_thread;
 
     /* for thread and filtering in backtrack */
-    virtual inline bool filtering(event_idt u)
+    virtual inline bool filtering(event_idt)
     {
       return false;
     }
diff --git a/src/goto-instrument/wmm/instrumenter_strategies.cpp b/src/goto-instrument/wmm/instrumenter_strategies.cpp
index 97ad9888f80..bd809a7a23f 100644
--- a/src/goto-instrument/wmm/instrumenter_strategies.cpp
+++ b/src/goto-instrument/wmm/instrumenter_strategies.cpp
@@ -159,14 +159,14 @@ void inline instrumentert::instrument_one_event_per_cycle_inserter(
 }
 
 void inline instrumentert::instrument_one_read_per_cycle_inserter(
-  const std::set<event_grapht::critical_cyclet> &set_of_cycles)
+  const std::set<event_grapht::critical_cyclet> &)
 {
   /* TODO */
   throw "read first strategy not implemented yet";
 }
 
 void inline instrumentert::instrument_one_write_per_cycle_inserter(
-  const std::set<event_grapht::critical_cyclet> &set_of_cycles)
+  const std::set<event_grapht::critical_cyclet> &)
 {
   /* TODO */
   throw "write first strategy not implemented yet";
diff --git a/src/goto-programs/cfg.h b/src/goto-programs/cfg.h
index ee77dd6ce37..db4a75c8939 100644
--- a/src/goto-programs/cfg.h
+++ b/src/goto-programs/cfg.h
@@ -245,10 +245,10 @@ void cfg_baset<T, P, I>::compute_edges_catch(
 
 template<class T, typename P, typename I>
 void cfg_baset<T, P, I>::compute_edges_throw(
-  const goto_programt &goto_program,
-  const goto_programt::instructiont &instruction,
-  goto_programt::const_targett next_PC,
-  entryt &entry)
+  const goto_programt &,
+  const goto_programt::instructiont &,
+  goto_programt::const_targett,
+  entryt &)
 {
   // no (trivial) successors
 }
@@ -256,7 +256,7 @@ void cfg_baset<T, P, I>::compute_edges_throw(
 template<class T, typename P, typename I>
 void cfg_baset<T, P, I>::compute_edges_start_thread(
   const goto_programt &goto_program,
-  const goto_programt::instructiont &instruction,
+  const goto_programt::instructiont &,
   goto_programt::const_targett next_PC,
   entryt &entry)
 {
@@ -333,7 +333,7 @@ void cfg_baset<T, P, I>::compute_edges_function_call(
 
 template<class T, typename P, typename I>
 void procedure_local_cfg_baset<T, P, I>::compute_edges_function_call(
-  const goto_functionst &goto_functions,
+  const goto_functionst &,
   const goto_programt &goto_program,
   const goto_programt::instructiont &instruction,
   goto_programt::const_targett next_PC,
diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp
index 7b82b3415c3..f36a16781f3 100644
--- a/src/goto-programs/goto_convert.cpp
+++ b/src/goto-programs/goto_convert.cpp
@@ -352,8 +352,8 @@ void goto_convertt::convert_label(
 }
 
 void goto_convertt::convert_gcc_local_label(
-  const codet &code,
-  goto_programt &dest)
+  const codet &,
+  goto_programt &)
 {
   // ignore for now
 }
@@ -712,8 +712,8 @@ void goto_convertt::convert_decl(
 }
 
 void goto_convertt::convert_decl_type(
-  const codet &code,
-  goto_programt &dest)
+  const codet &,
+  goto_programt &)
 {
   // we remove these
 }
diff --git a/src/goto-programs/goto_convert_class.h b/src/goto-programs/goto_convert_class.h
index 04888040fcc..cdfeb9177b6 100644
--- a/src/goto-programs/goto_convert_class.h
+++ b/src/goto-programs/goto_convert_class.h
@@ -193,7 +193,7 @@ class goto_convertt:public messaget
     const exprt::operandst &arguments,
     goto_programt &dest);
 
-  virtual void do_function_call_symbol(const symbolt &symbol)
+  virtual void do_function_call_symbol(const symbolt &)
   {
   }
 
diff --git a/src/goto-programs/goto_trace.cpp b/src/goto-programs/goto_trace.cpp
index 1416b20dc57..eac0ed4820d 100644
--- a/src/goto-programs/goto_trace.cpp
+++ b/src/goto-programs/goto_trace.cpp
@@ -33,7 +33,7 @@ void goto_tracet::output(
 }
 
 void goto_trace_stept::output(
-  const namespacet &ns,
+  const namespacet &,
   std::ostream &out) const
 {
   out << "*** ";
diff --git a/src/goto-programs/string_instrumentation.cpp b/src/goto-programs/string_instrumentation.cpp
index be5ccacfbbc..77e954b0aaa 100644
--- a/src/goto-programs/string_instrumentation.cpp
+++ b/src/goto-programs/string_instrumentation.cpp
@@ -635,9 +635,9 @@ void string_instrumentationt::do_format_string_write(
 }
 
 void string_instrumentationt::do_strncmp(
-  goto_programt &dest,
-  goto_programt::targett target,
-  code_function_callt &call)
+  goto_programt &,
+  goto_programt::targett,
+  code_function_callt &)
 {
 }
 
diff --git a/src/goto-programs/wp.cpp b/src/goto-programs/wp.cpp
index 91029d1f987..919af668fd8 100644
--- a/src/goto-programs/wp.cpp
+++ b/src/goto-programs/wp.cpp
@@ -218,7 +218,7 @@ exprt wp_assign(
 exprt wp_assume(
   const code_assumet &code,
   const exprt &post,
-  const namespacet &ns)
+  const namespacet &)
 {
   return implies_exprt(code.assumption(), post);
 }
diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h
index 0e253b28eb7..5f763d1559d 100644
--- a/src/goto-symex/goto_symex.h
+++ b/src/goto-symex/goto_symex.h
@@ -338,7 +338,7 @@ class goto_symext
   void pop_frame(statet &);
   void return_assignment(statet &);
 
-  virtual void no_body(const irep_idt &identifier)
+  virtual void no_body(const irep_idt &)
   {
   }
 
diff --git a/src/goto-symex/slice.cpp b/src/goto-symex/slice.cpp
index 654c45bbb68..8e9af5e820e 100644
--- a/src/goto-symex/slice.cpp
+++ b/src/goto-symex/slice.cpp
@@ -26,7 +26,7 @@ void symex_slicet::get_symbols(const exprt &expr)
     depends.insert(to_symbol_expr(expr).get_identifier());
 }
 
-void symex_slicet::get_symbols(const typet &type)
+void symex_slicet::get_symbols(const typet &)
 {
   // TODO
 }
diff --git a/src/goto-symex/symex_builtin_functions.cpp b/src/goto-symex/symex_builtin_functions.cpp
index 34a26fa1846..07104728643 100644
--- a/src/goto-symex/symex_builtin_functions.cpp
+++ b/src/goto-symex/symex_builtin_functions.cpp
@@ -453,8 +453,8 @@ void goto_symext::symex_cpp_new(
 }
 
 void goto_symext::symex_cpp_delete(
-  statet &state,
-  const codet &code)
+  statet &,
+  const codet &)
 {
   // TODO
   #if 0
@@ -502,9 +502,10 @@ void goto_symext::symex_trace(
 }
 
 void goto_symext::symex_fkt(
-  statet &state,
-  const code_function_callt &code)
+  statet &,
+  const code_function_callt &)
 {
+  UNREACHABLE;
   #if 0
   exprt new_fc(ID_function, fc.type());
 
@@ -525,7 +526,7 @@ void goto_symext::symex_fkt(
 }
 
 void goto_symext::symex_macro(
-  statet &state,
+  statet &,
   const code_function_callt &code)
 {
   const irep_idt &identifier=code.op0().get(ID_identifier);
diff --git a/src/goto-symex/symex_catch.cpp b/src/goto-symex/symex_catch.cpp
index c36deb71645..a5440bb3c90 100644
--- a/src/goto-symex/symex_catch.cpp
+++ b/src/goto-symex/symex_catch.cpp
@@ -11,8 +11,9 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "goto_symex.h"
 
-void goto_symext::symex_catch(statet &state)
+void goto_symext::symex_catch(statet &)
 {
+  UNREACHABLE;
   // there are two variants: 'push' and 'pop'
 
   #if 0
diff --git a/src/goto-symex/symex_dereference_state.cpp b/src/goto-symex/symex_dereference_state.cpp
index f1d43c7713c..7531f5c03bf 100644
--- a/src/goto-symex/symex_dereference_state.cpp
+++ b/src/goto-symex/symex_dereference_state.cpp
@@ -14,9 +14,9 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/symbol_table.h>
 
 void symex_dereference_statet::dereference_failure(
-  const std::string &property,
-  const std::string &msg,
-  const guardt &guard)
+  const std::string &,
+  const std::string &,
+  const guardt &)
 {
 }
 
diff --git a/src/goto-symex/symex_function_call.cpp b/src/goto-symex/symex_function_call.cpp
index 8e2f0707b86..67365ffe2af 100644
--- a/src/goto-symex/symex_function_call.cpp
+++ b/src/goto-symex/symex_function_call.cpp
@@ -18,9 +18,9 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/invariant.h>
 
 bool goto_symext::get_unwind_recursion(
-  const irep_idt &identifier,
-  const unsigned thread_nr,
-  unsigned unwind)
+  const irep_idt &,
+  const unsigned,
+  unsigned)
 {
   return false;
 }
diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp
index ca7008f7385..0bed128088f 100644
--- a/src/goto-symex/symex_goto.cpp
+++ b/src/goto-symex/symex_goto.cpp
@@ -539,9 +539,9 @@ void goto_symext::loop_bound_exceeded(
 }
 
 bool goto_symext::get_unwind(
-  const symex_targett::sourcet &source,
-  const goto_symex_statet::call_stackt &context,
-  unsigned unwind)
+  const symex_targett::sourcet &,
+  const goto_symex_statet::call_stackt &,
+  unsigned)
 {
   // by default, we keep going
   return false;
diff --git a/src/goto-symex/symex_target_equation.cpp b/src/goto-symex/symex_target_equation.cpp
index b0c03e154ce..21e43600fd7 100644
--- a/src/goto-symex/symex_target_equation.cpp
+++ b/src/goto-symex/symex_target_equation.cpp
@@ -184,9 +184,9 @@ void symex_target_equationt::decl(
 
 /// declare a fresh variable
 void symex_target_equationt::dead(
-  const exprt &guard,
-  const ssa_exprt &ssa_lhs,
-  const sourcet &source)
+  const exprt &,
+  const ssa_exprt &,
+  const sourcet &)
 {
   // we currently don't record these
 }
diff --git a/src/jsil/jsil_language.cpp b/src/jsil/jsil_language.cpp
index 83462732c1d..ad86320e3e7 100644
--- a/src/jsil/jsil_language.cpp
+++ b/src/jsil/jsil_language.cpp
@@ -42,9 +42,9 @@ bool jsil_languaget::interfaces(symbol_tablet &symbol_table)
 }
 
 bool jsil_languaget::preprocess(
-  std::istream &instream,
-  const std::string &path,
-  std::ostream &outstream)
+  std::istream &,
+  const std::string &,
+  std::ostream &)
 {
   // there is no preprocessing!
   return true;
@@ -78,7 +78,7 @@ bool jsil_languaget::parse(
 /// Converting from parse tree and type checking.
 bool jsil_languaget::typecheck(
   symbol_tablet &symbol_table,
-  const std::string &module)
+  const std::string &)
 {
   if(jsil_typecheck(symbol_table, get_message_handler()))
     return true;
@@ -124,7 +124,7 @@ bool jsil_languaget::from_type(
 
 bool jsil_languaget::to_expr(
   const std::string &code,
-  const std::string &module,
+  const std::string &,
   exprt &expr,
   const namespacet &ns)
 {
diff --git a/src/jsil/jsil_typecheck.cpp b/src/jsil/jsil_typecheck.cpp
index 56af74f6675..43604741238 100644
--- a/src/jsil/jsil_typecheck.cpp
+++ b/src/jsil/jsil_typecheck.cpp
@@ -922,7 +922,7 @@ bool jsil_typecheck(
 bool jsil_typecheck(
   exprt &expr,
   message_handlert &message_handler,
-  const namespacet &ns)
+  const namespacet &)
 {
   const unsigned errors_before=
     message_handler.get_message_count(messaget::M_ERROR);
diff --git a/src/jsil/jsil_typecheck.h b/src/jsil/jsil_typecheck.h
index 689a1eecd6b..cdd65c9b170 100644
--- a/src/jsil/jsil_typecheck.h
+++ b/src/jsil/jsil_typecheck.h
@@ -56,7 +56,7 @@ class jsil_typecheckt:public typecheckt
 
   void update_expr_type(exprt &expr, const typet &type);
   void make_type_compatible(exprt &expr, const typet &type, bool must);
-  void typecheck_type_symbol(symbolt &symbol) {}
+  void typecheck_type_symbol(symbolt &) {}
   void typecheck_non_type_symbol(symbolt &symbol);
   void typecheck_symbol_expr(symbol_exprt &symbol_expr);
   void typecheck_expr_side_effect_throw(side_effect_expr_throwt &expr);
diff --git a/src/langapi/language.cpp b/src/langapi/language.cpp
index 443062dce08..c75e810026c 100644
--- a/src/langapi/language.cpp
+++ b/src/langapi/language.cpp
@@ -18,26 +18,26 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/cprover_prefix.h>
 #include <util/std_types.h>
 
-bool languaget::final(symbol_table_baset &symbol_table)
+bool languaget::final(symbol_table_baset &)
 {
   return false;
 }
 
-bool languaget::interfaces(symbol_tablet &symbol_table)
+bool languaget::interfaces(symbol_tablet &)
 {
   return false;
 }
 
 void languaget::dependencies(
-  const std::string &module,
-  std::set<std::string> &modules)
+  const std::string &,
+  std::set<std::string> &)
 {
 }
 
 bool languaget::from_expr(
   const exprt &expr,
   std::string &code,
-  const namespacet &ns)
+  const namespacet &)
 {
   code=expr.pretty();
   return false;
@@ -46,7 +46,7 @@ bool languaget::from_expr(
 bool languaget::from_type(
   const typet &type,
   std::string &code,
-  const namespacet &ns)
+  const namespacet &)
 {
   code=type.pretty();
   return false;
@@ -55,7 +55,7 @@ bool languaget::from_type(
 bool languaget::type_to_name(
   const typet &type,
   std::string &name,
-  const namespacet &ns)
+  const namespacet &)
 {
   // probably ansi-c/type2name could be used as better fallback if moved to
   // util/
diff --git a/src/langapi/language_ui.cpp b/src/langapi/language_ui.cpp
index 4f3f3ec479e..85b0371fbe6 100644
--- a/src/langapi/language_ui.cpp
+++ b/src/langapi/language_ui.cpp
@@ -140,7 +140,7 @@ void language_uit::show_symbol_table(bool brief)
   }
 }
 
-void language_uit::show_symbol_table_xml_ui(bool brief)
+void language_uit::show_symbol_table_xml_ui(bool)
 {
   error() << "cannot show symbol table in this format" << eom;
 }
diff --git a/src/pointer-analysis/value_set.h b/src/pointer-analysis/value_set.h
index e879d2837f3..dfeb8588150 100644
--- a/src/pointer-analysis/value_set.h
+++ b/src/pointer-analysis/value_set.h
@@ -533,7 +533,7 @@ class value_sett
   /// originated in a particular place, vs. those that have been copied.
   virtual void adjust_assign_rhs_values(
     const exprt &rhs,
-    const namespacet &ns,
+    const namespacet &,
     object_mapt &rhs_values) const
   {
   }
@@ -545,7 +545,7 @@ class value_sett
   virtual void apply_assign_side_effects(
     const exprt &lhs,
     const exprt &rhs,
-    const namespacet &ns)
+    const namespacet &)
   {
   }
 };
diff --git a/src/pointer-analysis/value_set_domain.h b/src/pointer-analysis/value_set_domain.h
index 27e1201c0c2..3f6be037208 100644
--- a/src/pointer-analysis/value_set_domain.h
+++ b/src/pointer-analysis/value_set_domain.h
@@ -25,7 +25,7 @@ class value_set_domain_templatet:public domain_baset
 
   // overloading
 
-  bool merge(const value_set_domain_templatet<VST> &other, locationt to)
+  bool merge(const value_set_domain_templatet<VST> &other, locationt)
   {
     return value_set.make_union(other.value_set);
   }
@@ -38,7 +38,7 @@ class value_set_domain_templatet:public domain_baset
   }
 
   virtual void initialize(
-    const namespacet &ns,
+    const namespacet &,
     locationt l)
   {
     value_set.clear();
diff --git a/src/pointer-analysis/value_set_domain_fi.h b/src/pointer-analysis/value_set_domain_fi.h
index 24e2ac1be2c..e50ebcc8f7a 100644
--- a/src/pointer-analysis/value_set_domain_fi.h
+++ b/src/pointer-analysis/value_set_domain_fi.h
@@ -36,8 +36,7 @@ class value_set_domain_fit:public flow_insensitive_abstract_domain_baset
     value_set.output(ns, out);
   }
 
-  virtual void initialize(
-    const namespacet &ns)
+  virtual void initialize(const namespacet &)
   {
     value_set.clear();
   }
diff --git a/src/pointer-analysis/value_set_domain_fivr.h b/src/pointer-analysis/value_set_domain_fivr.h
index 4ecb8879517..3dde90527e0 100644
--- a/src/pointer-analysis/value_set_domain_fivr.h
+++ b/src/pointer-analysis/value_set_domain_fivr.h
@@ -32,7 +32,7 @@ class value_set_domain_fivrt:public flow_insensitive_abstract_domain_baset
   }
 
   virtual void initialize(
-    const namespacet &ns)
+    const namespacet &)
   {
     value_set.clear();
   }
diff --git a/src/pointer-analysis/value_set_domain_fivrns.h b/src/pointer-analysis/value_set_domain_fivrns.h
index 4e7827e4617..130f3367a4b 100644
--- a/src/pointer-analysis/value_set_domain_fivrns.h
+++ b/src/pointer-analysis/value_set_domain_fivrns.h
@@ -33,7 +33,7 @@ class value_set_domain_fivrnst:
   }
 
   virtual void initialize(
-    const namespacet &ns)
+    const namespacet &)
   {
     value_set.clear();
   }
diff --git a/src/solvers/flattening/arrays.cpp b/src/solvers/flattening/arrays.cpp
index b48f4c65647..cd3b17f23f1 100644
--- a/src/solvers/flattening/arrays.cpp
+++ b/src/solvers/flattening/arrays.cpp
@@ -573,8 +573,8 @@ void arrayst::add_array_constraints_with(
 }
 
 void arrayst::add_array_constraints_update(
-  const index_sett &index_set,
-  const update_exprt &expr)
+  const index_sett &,
+  const update_exprt &)
 {
   // we got x=UPDATE(y, [i], v)
   // add constaint x[i]=v
diff --git a/src/solvers/floatbv/float_utils.cpp b/src/solvers/floatbv/float_utils.cpp
index cb2fce7c329..0479983d7cd 100644
--- a/src/solvers/floatbv/float_utils.cpp
+++ b/src/solvers/floatbv/float_utils.cpp
@@ -1305,14 +1305,14 @@ bvt float_utilst::sticky_right_shift(
 
 bvt float_utilst::debug1(
   const bvt &src1,
-  const bvt &src2)
+  const bvt &)
 {
   return src1;
 }
 
 bvt float_utilst::debug2(
   const bvt &op0,
-  const bvt &op1)
+  const bvt &)
 {
   return op0;
 }
diff --git a/src/solvers/prop/prop.h b/src/solvers/prop/prop.h
index bb1a530656e..bf9820c6f3e 100644
--- a/src/solvers/prop/prop.h
+++ b/src/solvers/prop/prop.h
@@ -82,12 +82,12 @@ class propt:public messaget
   virtual bool cnf_handled_well() const { return true; }
 
   // assumptions
-  virtual void set_assumptions(const bvt &_assumptions) { }
+  virtual void set_assumptions(const bvt &) { }
   virtual bool has_set_assumptions() const { return false; }
 
   // variables
   virtual literalt new_variable()=0;
-  virtual void set_variable_name(literalt a, const irep_idt &name) { }
+  virtual void set_variable_name(literalt, const irep_idt &) { }
   virtual size_t no_variables() const=0;
   bvt new_variables(std::size_t width);
 
@@ -108,10 +108,10 @@ class propt:public messaget
   virtual bool has_is_in_conflict() const { return false; }
 
   // an incremental solver may remove any variables that aren't frozen
-  virtual void set_frozen(literalt a) { }
+  virtual void set_frozen(literalt) { }
 
   // Resource limits:
-  virtual void set_time_limit_seconds(uint32_t lim)
+  virtual void set_time_limit_seconds(uint32_t)
   {
     warning() << "CPU limit ignored (not implemented)" << eom;
   }
diff --git a/src/solvers/prop/prop_conv.cpp b/src/solvers/prop/prop_conv.cpp
index 0e929871f53..b2066e53a9c 100644
--- a/src/solvers/prop/prop_conv.cpp
+++ b/src/solvers/prop/prop_conv.cpp
@@ -10,7 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <algorithm>
 
 /// determine whether a variable is in the final conflict
-bool prop_convt::is_in_conflict(literalt l) const
+bool prop_convt::is_in_conflict(literalt) const
 {
   UNREACHABLE;
   return false;
diff --git a/src/solvers/qbf/qbf_quantor.cpp b/src/solvers/qbf/qbf_quantor.cpp
index 8f605c0b9f1..5f5890e5a1b 100644
--- a/src/solvers/qbf/qbf_quantor.cpp
+++ b/src/solvers/qbf/qbf_quantor.cpp
@@ -20,7 +20,7 @@ qbf_quantort::~qbf_quantort()
 {
 }
 
-tvt qbf_quantort::l_get(literalt a) const
+tvt qbf_quantort::l_get(literalt) const
 {
   assert(false);
   return tvt::unknown();
diff --git a/src/solvers/qbf/qbf_qube.cpp b/src/solvers/qbf/qbf_qube.cpp
index 37ad3374705..4057801afca 100644
--- a/src/solvers/qbf/qbf_qube.cpp
+++ b/src/solvers/qbf/qbf_qube.cpp
@@ -22,7 +22,7 @@ qbf_qubet::~qbf_qubet()
 {
 }
 
-tvt qbf_qubet::l_get(literalt a) const
+tvt qbf_qubet::l_get(literalt) const
 {
   assert(false);
   return tvt(false);
diff --git a/src/solvers/qbf/qbf_qube_core.cpp b/src/solvers/qbf/qbf_qube_core.cpp
index 877a5a27a85..b92b0393ea1 100644
--- a/src/solvers/qbf/qbf_qube_core.cpp
+++ b/src/solvers/qbf/qbf_qube_core.cpp
@@ -129,12 +129,12 @@ propt::resultt qbf_qube_coret::prop_solve()
   }
 }
 
-bool qbf_qube_coret::is_in_core(literalt l) const
+bool qbf_qube_coret::is_in_core(literalt) const
 {
   throw "not supported";
 }
 
-qdimacs_coret::modeltypet qbf_qube_coret::m_get(literalt a) const
+qdimacs_coret::modeltypet qbf_qube_coret::m_get(literalt) const
 {
   throw "not supported";
 }
diff --git a/src/solvers/qbf/qbf_qube_core.h b/src/solvers/qbf/qbf_qube_core.h
index 29d68088e5c..f1f31589035 100644
--- a/src/solvers/qbf/qbf_qube_core.h
+++ b/src/solvers/qbf/qbf_qube_core.h
@@ -49,7 +49,7 @@ class qbf_qube_coret:public qdimacs_coret
 
   virtual modeltypet m_get(literalt a) const;
 
-  virtual const exprt f_get(literalt l)
+  virtual const exprt f_get(literalt)
   {
     throw "qube does not support full certificates.";
   }
diff --git a/src/solvers/qbf/qbf_skizzo.cpp b/src/solvers/qbf/qbf_skizzo.cpp
index d8fb7e59f31..be5850ae6ed 100644
--- a/src/solvers/qbf/qbf_skizzo.cpp
+++ b/src/solvers/qbf/qbf_skizzo.cpp
@@ -22,7 +22,7 @@ qbf_skizzot::~qbf_skizzot()
 {
 }
 
-tvt qbf_skizzot::l_get(literalt a) const
+tvt qbf_skizzot::l_get(literalt) const
 {
   assert(false);
   return tvt(false);
diff --git a/src/solvers/refinement/string_builtin_function.h b/src/solvers/refinement/string_builtin_function.h
index 72e526ab102..376a11fdc5b 100644
--- a/src/solvers/refinement/string_builtin_function.h
+++ b/src/solvers/refinement/string_builtin_function.h
@@ -470,7 +470,7 @@ class string_builtin_function_with_no_evalt : public string_builtin_functiont
   }
 
   optionalt<exprt>
-  eval(const std::function<exprt(const exprt &)> &get_value) const override
+  eval(const std::function<exprt(const exprt &)> &) const override
   {
     return {};
   }
diff --git a/src/solvers/sat/cnf_clause_list.h b/src/solvers/sat/cnf_clause_list.h
index 5f931f20232..aa95681612a 100644
--- a/src/solvers/sat/cnf_clause_list.h
+++ b/src/solvers/sat/cnf_clause_list.h
@@ -31,7 +31,7 @@ class cnf_clause_listt:public cnft
   virtual const std::string solver_text()
   { return "CNF clause list"; }
 
-  virtual tvt l_get(literalt literal) const
+  virtual tvt l_get(literalt) const
   {
     return tvt::unknown();
   }
diff --git a/src/solvers/sat/dimacs_cnf.cpp b/src/solvers/sat/dimacs_cnf.cpp
index 982aca0e037..ee3e08c809a 100644
--- a/src/solvers/sat/dimacs_cnf.cpp
+++ b/src/solvers/sat/dimacs_cnf.cpp
@@ -19,12 +19,12 @@ dimacs_cnft::dimacs_cnft():break_lines(false)
 {
 }
 
-void dimacs_cnft::set_assignment(literalt a, bool value)
+void dimacs_cnft::set_assignment(literalt, bool)
 {
   UNIMPLEMENTED;
 }
 
-bool dimacs_cnft::is_in_conflict(literalt l) const
+bool dimacs_cnft::is_in_conflict(literalt) const
 {
   UNREACHABLE;
   return false;
diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp
index c1b14961d76..007e4fdd3d7 100644
--- a/src/solvers/smt2/smt2_conv.cpp
+++ b/src/solvers/smt2/smt2_conv.cpp
@@ -4069,7 +4069,7 @@ void smt2_convt::unflatten(
   }
 }
 
-void smt2_convt::convert_overflow(const exprt &expr)
+void smt2_convt::convert_overflow(const exprt &)
 {
   UNREACHABLE;
 }
diff --git a/src/solvers/smt2/smt2_conv.h b/src/solvers/smt2/smt2_conv.h
index e89363f4338..28f9639df09 100644
--- a/src/solvers/smt2/smt2_conv.h
+++ b/src/solvers/smt2/smt2_conv.h
@@ -108,7 +108,7 @@ class smt2_convt:public prop_convt
 
   // overloading interfaces
   virtual literalt convert(const exprt &expr);
-  virtual void set_frozen(literalt a) { /* not needed */ }
+  virtual void set_frozen(literalt) { /* not needed */ }
   virtual void set_to(const exprt &expr, bool value);
   virtual exprt get(const exprt &expr) const;
   virtual std::string decision_procedure_text() const { return "SMT2"; }
diff --git a/src/solvers/smt2/smt2_parser.cpp b/src/solvers/smt2/smt2_parser.cpp
index 3ef2a7cc09e..d5f1fe1ad2b 100644
--- a/src/solvers/smt2/smt2_parser.cpp
+++ b/src/solvers/smt2/smt2_parser.cpp
@@ -280,8 +280,8 @@ exprt smt2_parsert::quantifier_expression(irep_idt id)
 }
 
 exprt smt2_parsert::function_application(
-  const irep_idt &identifier,
-  const exprt::operandst &op)
+  const irep_idt &,
+  const exprt::operandst &)
 {
   #if 0
   const auto &f = id_map[identifier];
diff --git a/src/util/bv_arithmetic.cpp b/src/util/bv_arithmetic.cpp
index b04dee98aa0..808c769e6d4 100644
--- a/src/util/bv_arithmetic.cpp
+++ b/src/util/bv_arithmetic.cpp
@@ -52,7 +52,7 @@ void bv_arithmetict::print(std::ostream &out) const
   out << to_ansi_c_string();
 }
 
-std::string bv_arithmetict::format(const format_spect &format_spec) const
+std::string bv_arithmetict::format(const format_spect &) const
 {
   std::string result;
 
diff --git a/src/util/cout_message.cpp b/src/util/cout_message.cpp
index 44203df75fb..9e264df0e37 100644
--- a/src/util/cout_message.cpp
+++ b/src/util/cout_message.cpp
@@ -100,7 +100,7 @@ void console_message_handlert::flush(unsigned level)
 void gcc_message_handlert::print(
   unsigned level,
   const std::string &message,
-  int sequence_number,
+  int,
   const source_locationt &location)
 {
   const irep_idt file=location.get_file();
diff --git a/src/util/expr.h b/src/util/expr.h
index 9e18d0a0c18..0c82b649510 100644
--- a/src/util/expr.h
+++ b/src/util/expr.h
@@ -162,14 +162,14 @@ class expr_visitort
 {
 public:
   virtual ~expr_visitort() { }
-  virtual void operator()(exprt &expr) { }
+  virtual void operator()(exprt &) { }
 };
 
 class const_expr_visitort
 {
 public:
   virtual ~const_expr_visitort() { }
-  virtual void operator()(const exprt &expr) { }
+  virtual void operator()(const exprt &) { }
 };
 
 #endif // CPROVER_UTIL_EXPR_H
diff --git a/src/util/message.cpp b/src/util/message.cpp
index 06c28b746ad..3e3ed886cba 100644
--- a/src/util/message.cpp
+++ b/src/util/message.cpp
@@ -14,7 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com
 void message_handlert::print(
   unsigned level,
   const std::string &message,
-  int sequence_number,
+  int,
   const source_locationt &location)
 {
   std::string dest;
@@ -58,7 +58,7 @@ void message_handlert::print(
 
 void message_handlert::print(
   unsigned level,
-  const std::string &message)
+  const std::string &)
 {
   if(level>=message_count.size())
     message_count.resize(level+1, 0);
diff --git a/src/util/message.h b/src/util/message.h
index 7f17398cc2d..1e16ae1def9 100644
--- a/src/util/message.h
+++ b/src/util/message.h
@@ -89,8 +89,8 @@ class null_message_handlert:public message_handlert
   virtual void print(
     unsigned level,
     const std::string &message,
-    int sequence_number,
-    const source_locationt &location)
+    int,
+    const source_locationt &)
   {
     print(level, message);
   }
diff --git a/src/util/parser.cpp b/src/util/parser.cpp
index 98f1508e07e..dffdb151c02 100644
--- a/src/util/parser.cpp
+++ b/src/util/parser.cpp
@@ -10,7 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "parser.h"
 
 #ifdef _WIN32
-int isatty(int f)
+int isatty(int)
 {
   return 0;
 }
diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp
index f7e442e40ef..1b1591e81b1 100644
--- a/src/util/simplify_expr.cpp
+++ b/src/util/simplify_expr.cpp
@@ -1251,7 +1251,7 @@ bool simplify_exprt::get_values(
   return true;
 }
 
-bool simplify_exprt::simplify_lambda(exprt &expr)
+bool simplify_exprt::simplify_lambda(exprt &)
 {
   bool result=true;
 
diff --git a/src/util/ui_message.cpp b/src/util/ui_message.cpp
index f97aa30deeb..c6ab39f1022 100644
--- a/src/util/ui_message.cpp
+++ b/src/util/ui_message.cpp
@@ -264,7 +264,7 @@ void ui_message_handlert::ui_msg(
 void ui_message_handlert::xml_ui_msg(
   const std::string &type,
   const std::string &msg1,
-  const std::string &msg2,
+  const std::string &,
   const source_locationt &location)
 {
   xmlt result;
@@ -287,7 +287,7 @@ void ui_message_handlert::xml_ui_msg(
 void ui_message_handlert::json_ui_msg(
   const std::string &type,
   const std::string &msg1,
-  const std::string &msg2,
+  const std::string &,
   const source_locationt &location)
 {
   INVARIANT(json_stream, "JSON stream must be initialized before use");