diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp
index 66ee0398ca3..12d05874369 100644
--- a/src/goto-instrument/goto_instrument_parse_options.cpp
+++ b/src/goto-instrument/goto_instrument_parse_options.cpp
@@ -1245,9 +1245,6 @@ void goto_instrument_parse_optionst::instrument_goto_program()
         /* default: instruments all unsafe pairs */
         inst_strategy=all;
 
-      const unsigned unwind_loops=
-        cmdline.isset("unwind")?
-        unsafe_string2unsigned(cmdline.get_value("unwind")):0;
       const unsigned max_var=
         cmdline.isset("max-var")?
         unsafe_string2unsigned(cmdline.get_value("max-var")):0;
@@ -1295,7 +1292,6 @@ void goto_instrument_parse_optionst::instrument_goto_program()
           goto_model,
           cmdline.isset("scc"),
           inst_strategy,
-          unwind_loops,
           !cmdline.isset("cfg-kill"),
           cmdline.isset("no-dependencies"),
           loops,
diff --git a/src/goto-instrument/wmm/event_graph.cpp b/src/goto-instrument/wmm/event_graph.cpp
index 110a3618ea2..bff690bd15b 100644
--- a/src/goto-instrument/wmm/event_graph.cpp
+++ b/src/goto-instrument/wmm/event_graph.cpp
@@ -1098,8 +1098,7 @@ std::string event_grapht::critical_cyclet::print_output() const
 std::string event_grapht::critical_cyclet::print_detail(
   const critical_cyclet &reduced,
   std::map<std::string, std::string> &map_id2var,
-  std::map<std::string, std::string> &map_var2id,
-  memory_modelt model) const
+  std::map<std::string, std::string> &map_var2id) const
 {
   std::string cycle;
   for(const_iterator it=reduced.begin(); it!=reduced.end(); ++it)
@@ -1140,13 +1139,13 @@ std::string event_grapht::critical_cyclet::print_all(
     critical_cyclet reduced(egraph, id);
     this->hide_internals(reduced);
     assert(reduced.size() > 0);
-    cycle+=print_detail(reduced, map_id2var, map_var2id, model);
+    cycle+=print_detail(reduced, map_id2var, map_var2id);
     cycle+=": ";
     cycle+=print_name(reduced, model);
   }
   else
   {
-    cycle+=print_detail(*this, map_id2var, map_var2id, model);
+    cycle+=print_detail(*this, map_id2var, map_var2id);
     cycle+=": ";
     cycle+=print_name(*this, model);
   }
diff --git a/src/goto-instrument/wmm/event_graph.h b/src/goto-instrument/wmm/event_graph.h
index 9d896a75255..190e6e87514 100644
--- a/src/goto-instrument/wmm/event_graph.h
+++ b/src/goto-instrument/wmm/event_graph.h
@@ -48,8 +48,7 @@ class event_grapht
 
     std::string print_detail(const critical_cyclet &reduced,
       std::map<std::string, std::string> &map_id2var,
-      std::map<std::string, std::string> &map_var2id,
-      memory_modelt model) const;
+      std::map<std::string, std::string> &map_var2id) const;
     std::string print_name(const critical_cyclet &redyced,
       memory_modelt model) const;
 
@@ -377,7 +376,7 @@ class event_grapht
     {}
 
     void set_naive() {naive=true;}
-    void collect_pairs(namespacet &ns);
+    void collect_pairs();
   };
 
 public:
@@ -577,17 +576,17 @@ class event_grapht
 
   /* collects all the pairs of events with respectively at least one cmp,
      regardless of the architecture (Pensieve'05 strategy) */
-  void collect_pairs(namespacet &ns)
+  void collect_pairs()
   {
     graph_pensieve_explorert exploration(*this, max_var, max_po_trans);
-    exploration.collect_pairs(ns);
+    exploration.collect_pairs();
   }
 
-  void collect_pairs_naive(namespacet &ns)
+  void collect_pairs_naive()
   {
     graph_pensieve_explorert exploration(*this, max_var, max_po_trans);
     exploration.set_naive();
-    exploration.collect_pairs(ns);
+    exploration.collect_pairs();
   }
 };
 #endif // CPROVER_GOTO_INSTRUMENT_WMM_EVENT_GRAPH_H
diff --git a/src/goto-instrument/wmm/goto2graph.cpp b/src/goto-instrument/wmm/goto2graph.cpp
index e29d78d6b46..9ced322139a 100644
--- a/src/goto-instrument/wmm/goto2graph.cpp
+++ b/src/goto-instrument/wmm/goto2graph.cpp
@@ -152,8 +152,6 @@ void instrumentert::cfg_visitort::visit_cfg_function(
     loop_strategyt replicate_body,
     /* function to analyse */
     const irep_idt &function,
-    /* incoming edges */
-    const std::set<instrumentert::cfg_visitort::nodet> &initial_vertex,
     /* outcoming edges */
     std::set<instrumentert::cfg_visitort::nodet> &ending_vertex)
 {
@@ -657,11 +655,6 @@ void instrumentert::cfg_visitort::visit_cfg_function_call(
   loop_strategyt replicate_body)
 {
   const goto_programt::instructiont &instruction=*i_it;
-  std::set<nodet> s;
-  for(const auto &in : instruction.incoming_edges)
-    if(in_pos.find(in)!=in_pos.end())
-      for(const auto &node : in_pos[in])
-        s.insert(node);
 
   const exprt &fun=to_code_function_call(instruction.code).function();
   const irep_idt &fun_id=to_symbol_expr(fun).get_identifier();
@@ -689,7 +682,7 @@ void instrumentert::cfg_visitort::visit_cfg_function_call(
       {
         /* just inlines */
         /* TODO */
-        visit_cfg_function(value_sets, model, no_dependencies, fun_id, s,
+        visit_cfg_function(value_sets, model, no_dependencies, fun_id,
           in_pos[i_it]);
         updated.insert(i_it);
       }
@@ -699,7 +692,7 @@ void instrumentert::cfg_visitort::visit_cfg_function_call(
     {
       /* normal inlining strategy */
       visit_cfg_function(value_sets, model, no_dependencies, replicate_body,
-        fun_id, s, in_pos[i_it]);
+        fun_id, in_pos[i_it]);
       updated.insert(i_it);
     }
 
diff --git a/src/goto-instrument/wmm/goto2graph.h b/src/goto-instrument/wmm/goto2graph.h
index ce69edc5644..bf1cb30693e 100644
--- a/src/goto-instrument/wmm/goto2graph.h
+++ b/src/goto-instrument/wmm/goto2graph.h
@@ -245,10 +245,9 @@ class instrumentert
       {
         /* forbids recursive function */
         enter_function(function);
-        const std::set<nodet> empty_in;
         std::set<nodet> end_out;
         visit_cfg_function(value_sets, model, no_dependencies, duplicate_body,
-          function, empty_in, end_out);
+          function, end_out);
         leave_function(function);
       }
       catch(const std::string &s)
@@ -266,8 +265,6 @@ class instrumentert
       loop_strategyt duplicate_body,
       /// function to analyse
       const irep_idt &function,
-      /// incoming edges
-      const std::set<nodet> &initial_vertex,
       /// outcoming edges
       std::set<nodet> &ending_vertex);
 
diff --git a/src/goto-instrument/wmm/instrumenter_pensieve.h b/src/goto-instrument/wmm/instrumenter_pensieve.h
index cb7afeb45dc..d637999b8d1 100644
--- a/src/goto-instrument/wmm/instrumenter_pensieve.h
+++ b/src/goto-instrument/wmm/instrumenter_pensieve.h
@@ -26,15 +26,15 @@ class instrumenter_pensievet:public instrumentert
   {
   }
 
-  void collect_pairs_naive(namespacet &ns)
+  void collect_pairs_naive()
   {
-    egraph.collect_pairs_naive(ns);
+    egraph.collect_pairs_naive();
   }
 
   /* collects directly all the pairs in the graph */
-  void collect_pairs(namespacet &ns)
+  void collect_pairs()
   {
-    egraph.collect_pairs(ns);
+    egraph.collect_pairs();
   }
 };
 
diff --git a/src/goto-instrument/wmm/pair_collection.cpp b/src/goto-instrument/wmm/pair_collection.cpp
index d620a3bfd2f..0fd36c30c92 100644
--- a/src/goto-instrument/wmm/pair_collection.cpp
+++ b/src/goto-instrument/wmm/pair_collection.cpp
@@ -22,7 +22,7 @@ Date: 2013
 #define OUTPUT(s, fence, file, line, id, type)  \
   s<<fence<<"|"<<file<<"|"<<line<<"|"<<id<<"|"<<type<<'\n'
 
-void event_grapht::graph_pensieve_explorert::collect_pairs(namespacet &ns)
+void event_grapht::graph_pensieve_explorert::collect_pairs()
 {
   std::ofstream res;
   res.open("results.txt");
diff --git a/src/goto-instrument/wmm/shared_buffers.cpp b/src/goto-instrument/wmm/shared_buffers.cpp
index 05c339c2117..ed410dfb0b8 100644
--- a/src/goto-instrument/wmm/shared_buffers.cpp
+++ b/src/goto-instrument/wmm/shared_buffers.cpp
@@ -970,11 +970,10 @@ bool shared_bufferst::is_buffered(
   if(instrumentations.find(identifier)!=instrumentations.end())
     return false; // these are instrumentations
 
-  return is_buffered_in_general(ns, symbol_expr, is_write);
+  return is_buffered_in_general(symbol_expr, is_write);
 }
 
 bool shared_bufferst::is_buffered_in_general(
-  const namespacet &ns,
   const symbol_exprt &symbol_expr,
   bool is_write
   // are we asking for the variable (false), or for the variable and the
@@ -1042,7 +1041,7 @@ void shared_bufferst::affected_by_delay(
             message.debug() <<"debug: "<<id2string(w_it->second.object)
               <<" reads from "<<id2string(r_it->second.object)
               <<messaget::eom;
-            if(is_buffered_in_general(ns, r_it->second.symbol_expr, true))
+            if(is_buffered_in_general(r_it->second.symbol_expr, true))
               // shouldn't it be true? false => overapprox
               affected_by_delay_set.insert(w_it->second.object);
           }
diff --git a/src/goto-instrument/wmm/shared_buffers.h b/src/goto-instrument/wmm/shared_buffers.h
index 7f946522858..c9733b514fc 100644
--- a/src/goto-instrument/wmm/shared_buffers.h
+++ b/src/goto-instrument/wmm/shared_buffers.h
@@ -173,7 +173,6 @@ class shared_bufferst
     bool is_write);
 
   bool is_buffered_in_general(
-    const namespacet&,
     const symbol_exprt&,
     bool is_write);
 
diff --git a/src/goto-instrument/wmm/weak_memory.cpp b/src/goto-instrument/wmm/weak_memory.cpp
index 2375b4f590c..08ffcf7dc0a 100644
--- a/src/goto-instrument/wmm/weak_memory.cpp
+++ b/src/goto-instrument/wmm/weak_memory.cpp
@@ -107,7 +107,6 @@ void weak_memory(
   goto_modelt &goto_model,
   bool SCC,
   instrumentation_strategyt event_strategy,
-  unsigned unwinding_bound,
   bool no_cfg_kill,
   bool no_dependencies,
   loop_strategyt duplicate_body,
diff --git a/src/goto-instrument/wmm/weak_memory.h b/src/goto-instrument/wmm/weak_memory.h
index d4eb6078174..a8764f7877b 100644
--- a/src/goto-instrument/wmm/weak_memory.h
+++ b/src/goto-instrument/wmm/weak_memory.h
@@ -31,7 +31,6 @@ void weak_memory(
   goto_modelt &,
   bool SCC,
   instrumentation_strategyt event_stategy,
-  unsigned unwinding_bound,
   bool no_cfg_kill,
   bool no_dependencies,
   loop_strategyt duplicate_body,