diff --git a/src/goto-instrument/wmm/cycle_collection.cpp b/src/goto-instrument/wmm/cycle_collection.cpp
index 5d2d34148ec..589dfec5d34 100644
--- a/src/goto-instrument/wmm/cycle_collection.cpp
+++ b/src/goto-instrument/wmm/cycle_collection.cpp
@@ -393,7 +393,7 @@ bool event_grapht::graph_explorert::backtrack(
     if(!get_com_only)
     {
       /* we first visit via po transition, if existing */
-      for(graph<abstract_eventt>::edgest::const_iterator
+      for(wmm_grapht::edgest::const_iterator
         w_it=egraph.po_out(vertex).begin();
         w_it!=egraph.po_out(vertex).end(); w_it++)
       {
@@ -436,7 +436,7 @@ bool event_grapht::graph_explorert::backtrack(
 
     if(!no_comm)
     /* we then visit via com transitions, if existing */
-    for(graph<abstract_eventt>::edgest::const_iterator
+    for(wmm_grapht::edgest::const_iterator
       w_it=egraph.com_out(vertex).begin();
       w_it!=egraph.com_out(vertex).end(); w_it++)
     {
@@ -568,7 +568,7 @@ bool event_grapht::graph_explorert::backtrack(
          (!this_vertex.WRfence
            && egraph[point_stack.top()].operation==abstract_eventt::Write));
 
-    for(graph<abstract_eventt>::edgest::const_iterator w_it=
+    for(wmm_grapht::edgest::const_iterator w_it=
       egraph.po_out(vertex).begin();
       w_it!=egraph.po_out(vertex).end(); w_it++)
     {
diff --git a/src/goto-instrument/wmm/event_graph.cpp b/src/goto-instrument/wmm/event_graph.cpp
index 79ed0b6a13f..c6332fa43b0 100644
--- a/src/goto-instrument/wmm/event_graph.cpp
+++ b/src/goto-instrument/wmm/event_graph.cpp
@@ -34,15 +34,15 @@ Function: event_grapht::print_rec_graph
 
 \*******************************************************************/
 
-void event_grapht::print_rec_graph(std::ofstream& file, unsigned node_id,
-  std::set<unsigned>& visited)
+void event_grapht::print_rec_graph(std::ofstream& file, event_idt node_id,
+  std::set<event_idt>& visited)
 {
   const abstract_eventt& node=operator[](node_id);
   file << node_id << "[label=\"" << node << ", " << node.source_location <<
     "\"];" << std::endl;
   visited.insert(node_id);
 
-  for(graph<abstract_eventt>::edgest::const_iterator
+  for(wmm_grapht::edgest::const_iterator
     it=po_out(node_id).begin();
     it!=po_out(node_id).end(); ++it)
   {
@@ -52,7 +52,7 @@ void event_grapht::print_rec_graph(std::ofstream& file, unsigned node_id,
       print_rec_graph(file, it->first, visited);
   }
 
-  for(graph<abstract_eventt>::edgest::const_iterator
+  for(wmm_grapht::edgest::const_iterator
     it=com_out(node_id).begin();
     it!=com_out(node_id).end(); ++it)
   {
@@ -76,8 +76,8 @@ Function: event_grapht::print_graph
 
 void event_grapht::print_graph() {
   assert(po_order.size()>0);
-  std::set<unsigned> visited;
-  unsigned root=po_order.front();
+  std::set<event_idt> visited;
+  event_idt root=po_order.front();
   std::ofstream file;
   file.open("graph.dot");
   file << "digraph G {" << std::endl;
@@ -99,8 +99,8 @@ Function: event_grapht::copy_segment
 
 \*******************************************************************/
 
-void event_grapht::explore_copy_segment(std::set<unsigned>& explored,
-  unsigned begin, unsigned end) const
+void event_grapht::explore_copy_segment(std::set<event_idt>& explored,
+  event_idt begin, event_idt end) const
 {
   //std::cout << "explores " << begin << " against " << end << std::endl;
   if(explored.find(begin)!=explored.end())
@@ -111,13 +111,13 @@ void event_grapht::explore_copy_segment(std::set<unsigned>& explored,
   if(begin==end)
     return;
 
-  for(graph<abstract_eventt>::edgest::const_iterator it=po_out(begin).begin();
+  for(wmm_grapht::edgest::const_iterator it=po_out(begin).begin();
     it!=po_out(begin).end();
     ++it)
     explore_copy_segment(explored, it->first, end);
 }
 
-unsigned event_grapht::copy_segment(unsigned begin, unsigned end)
+event_idt event_grapht::copy_segment(event_idt begin, event_idt end)
 {
   const abstract_eventt& begin_event=operator[](begin);
   const abstract_eventt& end_event=operator[](end);
@@ -137,7 +137,7 @@ unsigned event_grapht::copy_segment(unsigned begin, unsigned end)
 
   message.status() << "tries to duplicate between " << begin_event.source_location
     << " and " << end_event.source_location << messaget::eom;
-  std::set<unsigned> covered;
+  std::set<event_idt> covered;
 
   /* collects the nodes of the subgraph */
   explore_copy_segment(covered, begin, end);
@@ -145,17 +145,17 @@ unsigned event_grapht::copy_segment(unsigned begin, unsigned end)
   if(covered.size()==0)
     return end;
 
-//  for(std::set<unsigned>::const_iterator it=covered.begin(); it!=covered.end(); ++it)
+//  for(std::set<event_idt>::const_iterator it=covered.begin(); it!=covered.end(); ++it)
 //    std::cout << "covered: " << *it << std::endl;
 
-  std::map<unsigned, unsigned> orig2copy;
+  std::map<event_idt, event_idt> orig2copy;
 
   /* duplicates nodes */
-  for(std::set<unsigned>::const_iterator it=covered.begin();
+  for(std::set<event_idt>::const_iterator it=covered.begin();
     it!=covered.end();
     ++it)
   {
-    const unsigned new_node=add_node();
+    const event_idt new_node=add_node();
     operator[](new_node)(operator[](*it));
     orig2copy[*it]=new_node;
   }
@@ -165,11 +165,11 @@ unsigned event_grapht::copy_segment(unsigned begin, unsigned end)
   // (working on back-edges...)
 
   /* replicates the po_s forward-edges -- O(#E^2) */
-  for(std::set<unsigned>::const_iterator it_i=covered.begin();
+  for(std::set<event_idt>::const_iterator it_i=covered.begin();
     it_i!=covered.end();
     ++it_i)
   {
-    for(std::set<unsigned>::const_iterator it_j=covered.begin();
+    for(std::set<event_idt>::const_iterator it_j=covered.begin();
       it_j!=covered.end();
       ++it_j)
     {
@@ -187,11 +187,11 @@ unsigned event_grapht::copy_segment(unsigned begin, unsigned end)
 
   // TODO: to move to goto2graph, after po_s construction
   /* replicates the cmp-edges -- O(#E x #G) */
-  for(std::set<unsigned>::const_iterator it_i=covered.begin();
+  for(std::set<event_idt>::const_iterator it_i=covered.begin();
     it_i!=covered.end();
     ++it_i)
   {
-    for(unsigned it_j=0;
+    for(event_idt it_j=0;
       it_j<size();
       ++it_j)
     {
@@ -547,8 +547,8 @@ bool event_grapht::critical_cyclet::is_unsafe(memory_modelt model, bool fast)
     if(first.unsafe_pair(second,model)
       && (first.thread!=second.thread || egraph.are_po_ordered(back(),*s_it)))
     {
-      std::list<unsigned>::const_iterator before_first;
-      std::list<unsigned>::const_iterator after_second;
+      std::list<event_idt>::const_iterator before_first;
+      std::list<event_idt>::const_iterator after_second;
 
       before_first = end();
       --before_first;
@@ -581,8 +581,8 @@ bool event_grapht::critical_cyclet::is_unsafe(memory_modelt model, bool fast)
     if(first.unsafe_pair_lwfence(second,model)
       && (first.thread!=second.thread || egraph.are_po_ordered(back(),*s_it)))
     {
-      std::list<unsigned>::const_iterator before_first;
-      std::list<unsigned>::const_iterator after_second;
+      std::list<event_idt>::const_iterator before_first;
+      std::list<event_idt>::const_iterator after_second;
 
       before_first = end();
       --before_first;
@@ -1332,7 +1332,7 @@ Function: event_grapht::critical_cyclet::hide_internals
 
 void event_grapht::critical_cyclet::hide_internals(critical_cyclet& reduced)  const
 {
-  std::set<unsigned> reduced_evts;
+  std::set<event_idt> reduced_evts;
   const_iterator first_it, prev_it=end();
 
   /* finds an element first of its thread */
diff --git a/src/goto-instrument/wmm/event_graph.h b/src/goto-instrument/wmm/event_graph.h
index 7c0bac7f8b6..1a10ded69c3 100644
--- a/src/goto-instrument/wmm/event_graph.h
+++ b/src/goto-instrument/wmm/event_graph.h
@@ -29,11 +29,14 @@ class namespacet;
                      graph of abstract events
 \*******************************************************************/
 
+typedef graph<abstract_eventt> wmm_grapht;
+typedef wmm_grapht::node_indext event_idt;
+
 class event_grapht
 {
 public:
   /* critical cycle */
-  class critical_cyclet:public std::list<unsigned>
+  class critical_cyclet:public std::list<event_idt>
   {
   protected:
     event_grapht& egraph;
@@ -126,21 +129,21 @@ class event_grapht
     /* pair of events in a cycle */
     struct delayt
     {
-      unsigned first;
-      unsigned second;
+      event_idt first;
+      event_idt second;
       bool is_po;
 
-      delayt(unsigned _first)
+      delayt(event_idt _first)
         :first(_first),is_po(true)
       {
       }
 
-      delayt(unsigned _first, unsigned _second)
+      delayt(event_idt _first, event_idt _second)
         :first(_first),second(_second),is_po(false)
       {
       }
 
-      delayt(unsigned _first, unsigned _second, bool _is_po)
+      delayt(event_idt _first, event_idt _second, bool _is_po)
         :first(_first),second(_second),is_po(_is_po)
       {
       }
@@ -194,14 +197,14 @@ class event_grapht
 
     inline bool operator<(const critical_cyclet& other) const
     {
-      return ( ((std::list<unsigned>) *this) < (std::list<unsigned>)other);
+      return ( ((std::list<event_idt>) *this) < (std::list<event_idt>)other);
     }
   };
 
 protected:
   /* graph contains po and com transitions */
-  graph<abstract_eventt> po_graph;
-  graph<abstract_eventt> com_graph;
+  wmm_grapht po_graph;
+  wmm_grapht com_graph;
 
   /* parameters limiting the exploration */
   unsigned max_var;
@@ -229,13 +232,13 @@ class event_grapht
     std::map<unsigned,unsigned char> events_per_thread;
 
     /* for thread and filtering in backtrack */
-    virtual inline bool filtering(unsigned u)
+    virtual inline bool filtering(event_idt u)
     {
       return false;
     }
 
-    virtual inline std::list<unsigned>* order_filtering(
-      std::list<unsigned>* order)
+    virtual inline std::list<event_idt>* order_filtering(
+      std::list<event_idt>* order)
     {
       return order;
     }
@@ -246,7 +249,7 @@ class event_grapht
     /* events in thin-air executions met so far */
     /* any execution blocked by thin-air is guaranteed
        to have all its events in this set */
-    std::set<unsigned> thin_air_events;
+    std::set<event_idt> thin_air_events;
 
     /* after the collection, eliminates the executions forbidden by an
        indirect thin-air */
@@ -260,20 +263,20 @@ class event_grapht
     }
 
     /* structures for graph exploration */
-    std::map<unsigned,bool> mark;
-    std::stack<unsigned> marked_stack;
-    std::stack<unsigned> point_stack;
+    std::map<event_idt,bool> mark;
+    std::stack<event_idt> marked_stack;
+    std::stack<event_idt> point_stack;
 
-    std::set<unsigned> skip_tracked;
+    std::set<event_idt> skip_tracked;
 
-    critical_cyclet extract_cycle(unsigned vertex,
-      unsigned source, unsigned number_of_cycles);
+    critical_cyclet extract_cycle(event_idt vertex,
+      event_idt source, unsigned number_of_cycles);
 
     bool backtrack(std::set<critical_cyclet>& set_of_cycles,
-      unsigned source,
-      unsigned vertex,
+      event_idt source,
+      event_idt vertex,
       bool unsafe_met,
-      unsigned po_trans,
+      event_idt po_trans,
       bool same_var_pair,
       bool lwsync_met,
       bool has_to_be_unsafe,
@@ -290,26 +293,26 @@ class event_grapht
   class graph_conc_explorert:public graph_explorert
   {
   protected:
-    const std::set<unsigned>& filter;
+    const std::set<event_idt>& filter;
 
   public:
     graph_conc_explorert(event_grapht& _egraph, unsigned _max_var,
-      unsigned _max_po_trans, const std::set<unsigned>& _filter)
+      unsigned _max_po_trans, const std::set<event_idt>& _filter)
       :graph_explorert(_egraph,_max_var,_max_po_trans),filter(_filter)
     {
     }
 
-    inline bool filtering(unsigned u)
+    inline bool filtering(event_idt u)
     {
       return filter.find(u)==filter.end();
     }
 
-    inline std::list<unsigned>* initial_filtering(std::list<unsigned>* order)
+    inline std::list<event_idt>* initial_filtering(std::list<event_idt>* order)
     {
-      static std::list<unsigned> new_order;
+      static std::list<event_idt> new_order;
 
       /* intersection */
-      for(std::list<unsigned>::iterator it=order->begin();it!=order->end();it++)
+      for(std::list<event_idt>::iterator it=order->begin();it!=order->end();it++)
         if(filter.find(*it)!=filter.end())
           new_order.push_back(*it);
 
@@ -321,10 +324,10 @@ class event_grapht
   class graph_pensieve_explorert:public graph_explorert
   {
   protected:
-    std::set<unsigned> visited_nodes;
+    std::set<event_idt> visited_nodes;
     bool naive;
 
-    bool find_second_event(unsigned source);
+    bool find_second_event(event_idt source);
 
   public:
     graph_pensieve_explorert(event_grapht& _egraph, unsigned _max_var,
@@ -352,60 +355,60 @@ class event_grapht
   std::map<unsigned,data_dpt> map_data_dp;
 
   /* orders */
-  std::list<unsigned> po_order;
-  std::list<unsigned> poUrfe_order;
+  std::list<event_idt> po_order;
+  std::list<event_idt> poUrfe_order;
 
-  std::set<std::pair<unsigned,unsigned> > loops;
+  std::set<std::pair<event_idt,event_idt> > loops;
 
-  unsigned add_node()
+  event_idt add_node()
   {
-    const unsigned po_no = po_graph.add_node();
-    const unsigned com_no = com_graph.add_node();
+    const event_idt po_no = po_graph.add_node();
+    const event_idt com_no = com_graph.add_node();
     assert(po_no == com_no);
     return po_no;
   }
 
-  inline graph<abstract_eventt>::nodet &operator[](unsigned n)
+  inline wmm_grapht::nodet &operator[](event_idt n)
   {
     return po_graph[n];
   }
 
-  bool has_po_edge(unsigned i, unsigned j) const
+  bool has_po_edge(event_idt i, event_idt j) const
   {
     return po_graph.has_edge(i,j);
   }
 
-  bool has_com_edge(unsigned i, unsigned j) const
+  bool has_com_edge(event_idt i, event_idt j) const
   {
     return com_graph.has_edge(i,j);
   }
 
-  inline unsigned size() const
+  inline std::size_t size() const
   {
     return po_graph.size();
   }
 
-  inline const graph<abstract_eventt>::edgest &po_in(unsigned n) const
+  inline const wmm_grapht::edgest &po_in(event_idt n) const
   {
     return po_graph.in(n);
   }
 
-  inline const graph<abstract_eventt>::edgest &po_out(unsigned n) const
+  inline const wmm_grapht::edgest &po_out(event_idt n) const
   {
     return po_graph.out(n);
   }
 
-  inline const graph<abstract_eventt>::edgest &com_in(unsigned n) const
+  inline const wmm_grapht::edgest &com_in(event_idt n) const
   {
     return com_graph.in(n);
   }
 
-  inline const graph<abstract_eventt>::edgest &com_out(unsigned n) const
+  inline const wmm_grapht::edgest &com_out(event_idt n) const
   {
     return com_graph.out(n);
   }
 
-  void add_po_edge(unsigned a, unsigned b)
+  void add_po_edge(event_idt a, event_idt b)
   {
     assert(a!=b);
     assert(operator[](a).thread==operator[](b).thread);
@@ -414,42 +417,42 @@ class event_grapht
     poUrfe_order.push_back(a);
   }
 
-  void add_po_back_edge(unsigned a, unsigned b)
+  void add_po_back_edge(event_idt a, event_idt b)
   {
     assert(a!=b);
     assert(operator[](a).thread==operator[](b).thread);
     po_graph.add_edge(a,b);
     po_order.push_back(a);
     poUrfe_order.push_back(a);
-    loops.insert(std::pair<unsigned,unsigned>(a,b));
-    loops.insert(std::pair<unsigned,unsigned>(b,a));
+    loops.insert(std::pair<event_idt,event_idt>(a,b));
+    loops.insert(std::pair<event_idt,event_idt>(b,a));
   }
 
-  void add_com_edge(unsigned a, unsigned b)
+  void add_com_edge(event_idt a, event_idt b)
   {
     assert(a!=b);
     com_graph.add_edge(a,b);
     poUrfe_order.push_back(a);
   }
 
-  void add_undirected_com_edge(unsigned a, unsigned b)
+  void add_undirected_com_edge(event_idt a, event_idt b)
   {
     assert(a!=b);
     add_com_edge(a,b);
     add_com_edge(b,a);
   }
 
-  void remove_po_edge(unsigned a, unsigned b)
+  void remove_po_edge(event_idt a, event_idt b)
   {
     po_graph.remove_edge(a,b);
   }
 
-  void remove_com_edge(unsigned a, unsigned b)
+  void remove_com_edge(event_idt a, event_idt b)
   {
     com_graph.remove_edge(a,b);
   }
 
-  void remove_edge(unsigned a, unsigned b)
+  void remove_edge(event_idt a, event_idt b)
   {
     remove_po_edge(a,b);
     remove_com_edge(a,b);
@@ -457,30 +460,30 @@ class event_grapht
 
   /* copies the sub-graph G between begin and end into G', connects
      G.end with G'.begin, and returns G'.end */
-  void explore_copy_segment(std::set<unsigned>& explored, unsigned begin,
-    unsigned end) const;
-  unsigned copy_segment(unsigned begin, unsigned end);
+  void explore_copy_segment(std::set<event_idt>& explored, event_idt begin,
+    event_idt end) const;
+  event_idt copy_segment(event_idt begin, event_idt end);
 
   /* to keep track of the loop already copied */
   std::set<std::pair<const abstract_eventt&, const abstract_eventt&> > duplicated_bodies;
 
-  bool is_local(unsigned a)
+  bool is_local(event_idt a)
   {
     return operator[](a).local;
   }
 
   /* a -po-> b  -- transitive */
-  bool are_po_ordered(unsigned a, unsigned b)
+  bool are_po_ordered(event_idt a, event_idt b)
   {
     if(operator[](a).thread!=operator[](b).thread)
       return false;
 
     /* if back-edge, a-po->b \/ b-po->a */
-    if( loops.find(std::pair<unsigned,unsigned>(a,b))!=loops.end() )
+    if( loops.find(std::pair<event_idt,event_idt>(a,b))!=loops.end() )
       return true;
 
     // would be true if no cycle in po
-    for(std::list<unsigned>::iterator it=po_order.begin();
+    for(std::list<event_idt>::iterator it=po_order.begin();
       it!=po_order.end();it++)
       if(*it==a)
         return true;
@@ -499,13 +502,13 @@ class event_grapht
 
   /* prints to graph.dot */
   void print_graph();
-  void print_rec_graph(std::ofstream& file, unsigned node_id,
-    std::set<unsigned>& visited);
+  void print_rec_graph(std::ofstream& file, event_idt node_id,
+    std::set<event_idt>& visited);
 
   /* Tarjan 1972 adapted and modified for events + po-transitivity */
   void collect_cycles(std::set<critical_cyclet>& set_of_cycles,
     memory_modelt model,
-    const std::set<unsigned>& filter)
+    const std::set<event_idt>& filter)
   {
     graph_conc_explorert exploration(*this, max_var, max_po_trans,filter);
     exploration.collect_cycles(set_of_cycles,model);
diff --git a/src/goto-instrument/wmm/goto2graph.cpp b/src/goto-instrument/wmm/goto2graph.cpp
index 98f6d69b52b..f4b790aa2f1 100644
--- a/src/goto-instrument/wmm/goto2graph.cpp
+++ b/src/goto-instrument/wmm/goto2graph.cpp
@@ -126,12 +126,12 @@ unsigned instrumentert::goto2graph_cfg(
   std::vector<std::size_t> subgraph_index;
   num_sccs = egraph_alt.SCCs(subgraph_index);
   assert(egraph_SCCs.empty());
-  egraph_SCCs.resize(num_sccs, std::set<unsigned>());
-  for(std::map<unsigned,unsigned>::const_iterator it=map_vertex_gnode.begin();
+  egraph_SCCs.resize(num_sccs, std::set<event_idt>());
+  for(std::map<event_idt,event_idt>::const_iterator it=map_vertex_gnode.begin();
     it!=map_vertex_gnode.end();
     it++)
   {
-    const unsigned sg = subgraph_index[it->second];
+    const std::size_t sg = subgraph_index[it->second];
     egraph_SCCs[sg].insert(it->first);
   }
 
@@ -150,7 +150,7 @@ unsigned instrumentert::goto2graph_cfg(
   message.statistics() <<"Number of writes: "<<visitor.write_counter<<messaget::eom;
   message.statistics() <<"Number of wse: "<<visitor.ws_counter<<messaget::eom;
   message.statistics() <<"Number of rfe/fre: "<<visitor.fr_rf_counter<<messaget::eom;
-  unsigned instr_counter=0;
+  std::size_t instr_counter=0;
   for(goto_functionst::function_mapt::const_iterator it=goto_functions.function_map.begin();
       it!=goto_functions.function_map.end();
       ++it)
@@ -404,8 +404,8 @@ void inline instrumentert::cfg_visitort::visit_cfg_reference_function (
   /* beginning of the function */
   goto_programt::instructionst::iterator targ=body.begin();
 
-  std::set<unsigned> in_nodes;
-  std::set<unsigned> out_nodes;
+  std::set<event_idt> in_nodes;
+  std::set<event_idt> out_nodes;
 
   /* if the target has already been covered by fwd analysis */
   if(in_pos.find(targ)!=in_pos.end())
@@ -477,8 +477,8 @@ Function: alt_copy_segment
 
 \*******************************************************************/
 
-unsigned alt_copy_segment(graph<abstract_eventt>& alt_egraph,
-  unsigned begin, unsigned end)
+event_idt alt_copy_segment(wmm_grapht& alt_egraph,
+  event_idt begin, event_idt end)
 {
   /* no need to duplicate the loop nodes for the SCC-detection graph -- a
      single back-edge will ensure the same connectivity */
@@ -669,8 +669,8 @@ void inline instrumentert::cfg_visitort::visit_cfg_duplicate(
       egraph.copy_segment(begin_it->first, end_it->first);
       alt_copy_segment(egraph_alt, begin_it->second, end_it->second);
 #if 0
-      const unsigned end=egraph.copy_segment(begin_it->first, end_it->first);
-      const unsigned alt_end=alt_copy_segment(egraph_alt, begin_it->second, end_it->second);
+      const event_idt end=egraph.copy_segment(begin_it->first, end_it->first);
+      const event_idt alt_end=alt_copy_segment(egraph_alt, begin_it->second, end_it->second);
       //in_pos[i_it].insert(nodet(end, alt_end)); // copied; no need for back-edge!
 #endif
     }
@@ -889,9 +889,9 @@ void instrumentert::cfg_visitort::visit_cfg_lwfence(
   const goto_programt::instructiont& instruction=*i_it;
   const abstract_eventt new_fence_event(abstract_eventt::Lwfence,
     thread, "f", instrumenter.unique_id++, instruction.source_location, false);
-  const unsigned new_fence_node=egraph.add_node();
+  const event_idt new_fence_node=egraph.add_node();
   egraph[new_fence_node](new_fence_event);
-  const unsigned new_fence_gnode=egraph_alt.add_node();
+  const event_idt new_fence_gnode=egraph_alt.add_node();
   egraph_alt[new_fence_gnode]=new_fence_event;
   instrumenter.map_vertex_gnode.insert(
     std::make_pair(new_fence_node, new_fence_gnode));
@@ -941,9 +941,9 @@ void instrumentert::cfg_visitort::visit_cfg_asm_fence(
   const abstract_eventt new_fence_event(abstract_eventt::ASMfence,
     thread, "asm", instrumenter.unique_id++, instruction.source_location,
     false, WRfence, WWfence, RRfence, RWfence, WWcumul, RWcumul, RRcumul);
-  const unsigned new_fence_node=egraph.add_node();
+  const event_idt new_fence_node=egraph.add_node();
   egraph[new_fence_node](new_fence_event);
-  const unsigned new_fence_gnode=egraph_alt.add_node();
+  const event_idt new_fence_gnode=egraph_alt.add_node();
   egraph_alt[new_fence_gnode]=new_fence_event;
   instrumenter.map_vertex_gnode.insert(
     std::make_pair(new_fence_node, new_fence_gnode));
@@ -998,8 +998,8 @@ void instrumentert::cfg_visitort::visit_cfg_assign(
 #endif
   );
 
-  unsigned previous=std::numeric_limits<unsigned>::max();
-  unsigned previous_gnode=std::numeric_limits<unsigned>::max();
+  event_idt previous=std::numeric_limits<event_idt>::max();
+  event_idt previous_gnode=std::numeric_limits<event_idt>::max();
 
 #if 0
   /* for the moment, use labels ASSERT in front of the assertions
@@ -1031,7 +1031,7 @@ void instrumentert::cfg_visitort::visit_cfg_assign(
       thread, id2string(read), instrumenter.unique_id++,
       instruction.source_location, local(read));
 
-    const unsigned new_read_node=egraph.add_node();
+    const event_idt new_read_node=egraph.add_node();
     egraph[new_read_node]=new_read_event;
     instrumenter.message.debug() << "new Read"<<read<<" @thread"
       <<(thread)<<"("<<instruction.source_location<<","
@@ -1041,7 +1041,7 @@ void instrumentert::cfg_visitort::visit_cfg_assign(
     if(read==ID_unknown)
       unknown_read_nodes.insert(new_read_node);
 
-    const unsigned new_read_gnode=egraph_alt.add_node();
+    const event_idt new_read_gnode=egraph_alt.add_node();
     egraph_alt[new_read_gnode]=new_read_event;
     instrumenter.map_vertex_gnode.insert(
     std::make_pair(new_read_node,new_read_gnode));
@@ -1078,7 +1078,7 @@ void instrumentert::cfg_visitort::visit_cfg_assign(
       {
         instrumenter.message.debug() << id_it->second<<"<-com->"
           <<new_read_node << messaget::eom;
-        std::map<unsigned,unsigned>::const_iterator entry=
+        std::map<event_idt,event_idt>::const_iterator entry=
           instrumenter.map_vertex_gnode.find(id_it->second);
         assert(entry!=instrumenter.map_vertex_gnode.end());
         egraph.add_com_edge(new_read_node,id_it->second);
@@ -1089,7 +1089,7 @@ void instrumentert::cfg_visitort::visit_cfg_assign(
       }
 
     /* for unknown writes */
-    for(std::set<unsigned>::const_iterator id_it=
+    for(std::set<event_idt>::const_iterator id_it=
       unknown_write_nodes.begin();
       id_it!=unknown_write_nodes.end();
       ++id_it)
@@ -1097,7 +1097,7 @@ void instrumentert::cfg_visitort::visit_cfg_assign(
       {
         instrumenter.message.debug() << *id_it<<"<-com->"
           <<new_read_node << messaget::eom;
-        std::map<unsigned,unsigned>::const_iterator entry=
+        std::map<event_idt,event_idt>::const_iterator entry=
           instrumenter.map_vertex_gnode.find(*id_it);
         assert(entry!=instrumenter.map_vertex_gnode.end());
         egraph.add_com_edge(new_read_node,*id_it);
@@ -1131,7 +1131,7 @@ void instrumentert::cfg_visitort::visit_cfg_assign(
       thread, id2string(write), instrumenter.unique_id++,
       instruction.source_location, local(write));
 
-    const unsigned new_write_node=egraph.add_node();
+    const event_idt new_write_node=egraph.add_node();
     egraph[new_write_node](new_write_event);
     instrumenter.message.debug() << "new Write "<<write<<" @thread"<<(thread)
       <<"("<<instruction.source_location<<","
@@ -1141,13 +1141,13 @@ void instrumentert::cfg_visitort::visit_cfg_assign(
     if(write==ID_unknown)
       unknown_read_nodes.insert(new_write_node);
 
-    const unsigned new_write_gnode=egraph_alt.add_node();
+    const event_idt new_write_gnode=egraph_alt.add_node();
     egraph_alt[new_write_gnode]=new_write_event;
     instrumenter.map_vertex_gnode.insert(
-      std::pair<unsigned,unsigned>(new_write_node, new_write_gnode));
+      std::pair<event_idt,event_idt>(new_write_node, new_write_gnode));
 
     /* creates Read -po-> Write */
-    if(previous!=std::numeric_limits<unsigned>::max())
+    if(previous!=std::numeric_limits<event_idt>::max())
     {
       instrumenter.message.debug() << previous<<"-po->"<<new_write_node
         << messaget::eom;
@@ -1182,7 +1182,7 @@ void instrumentert::cfg_visitort::visit_cfg_assign(
       {
         instrumenter.message.debug() <<idr_it->second<<"<-com->"
           <<new_write_node << messaget::eom;
-        std::map<unsigned,unsigned>::const_iterator entry=
+        std::map<event_idt,event_idt>::const_iterator entry=
           instrumenter.map_vertex_gnode.find(idr_it->second);
         assert(entry!=instrumenter.map_vertex_gnode.end());
         egraph.add_com_edge(new_write_node,idr_it->second);
@@ -1201,7 +1201,7 @@ void instrumentert::cfg_visitort::visit_cfg_assign(
       {
         instrumenter.message.debug() << idw_it->second<<"<-com->"
           <<new_write_node << messaget::eom;
-        std::map<unsigned,unsigned>::const_iterator entry=
+        std::map<event_idt,event_idt>::const_iterator entry=
           instrumenter.map_vertex_gnode.find(idw_it->second);
         assert(entry!=instrumenter.map_vertex_gnode.end());
         egraph.add_com_edge(new_write_node,idw_it->second);
@@ -1212,7 +1212,7 @@ void instrumentert::cfg_visitort::visit_cfg_assign(
       }
 
     /* for unknown writes */
-    for(std::set<unsigned>::const_iterator id_it=
+    for(std::set<event_idt>::const_iterator id_it=
       unknown_write_nodes.begin();
       id_it!=unknown_write_nodes.end();
       ++id_it)
@@ -1220,7 +1220,7 @@ void instrumentert::cfg_visitort::visit_cfg_assign(
       {
         instrumenter.message.debug() << *id_it<<"<-com->"
           <<new_write_node << messaget::eom;
-        std::map<unsigned,unsigned>::const_iterator entry=
+        std::map<event_idt,event_idt>::const_iterator entry=
           instrumenter.map_vertex_gnode.find(*id_it);
         assert(entry!=instrumenter.map_vertex_gnode.end());
         egraph.add_com_edge(new_write_node,*id_it);
@@ -1231,7 +1231,7 @@ void instrumentert::cfg_visitort::visit_cfg_assign(
       }
 
     /* for unknown reads */
-    for(std::set<unsigned>::const_iterator id_it=
+    for(std::set<event_idt>::const_iterator id_it=
       unknown_read_nodes.begin();
       id_it!=unknown_read_nodes.end();
       ++id_it)
@@ -1239,7 +1239,7 @@ void instrumentert::cfg_visitort::visit_cfg_assign(
       {
         instrumenter.message.debug() << *id_it<<"<-com->"
           <<new_write_node << messaget::eom;
-        std::map<unsigned,unsigned>::const_iterator entry=
+        std::map<event_idt,event_idt>::const_iterator entry=
           instrumenter.map_vertex_gnode.find(*id_it);
         assert(entry!=instrumenter.map_vertex_gnode.end());
         egraph.add_com_edge(new_write_node,*id_it);
@@ -1255,7 +1255,7 @@ void instrumentert::cfg_visitort::visit_cfg_assign(
     previous_gnode = new_write_gnode;
   }
 
-  if(previous!=std::numeric_limits<unsigned>::max())
+  if(previous!=std::numeric_limits<event_idt>::max())
   {
     in_pos[i_it].clear();
     in_pos[i_it].insert(nodet(previous,previous_gnode));
@@ -1316,9 +1316,9 @@ void instrumentert::cfg_visitort::visit_cfg_fence(
   const goto_programt::instructiont& instruction=*i_it;
   const abstract_eventt new_fence_event(abstract_eventt::Fence,
     thread, "F", instrumenter.unique_id++, instruction.source_location, false);
-  const unsigned new_fence_node=egraph.add_node();
+  const event_idt new_fence_node=egraph.add_node();
   egraph[new_fence_node](new_fence_event);
-  const unsigned new_fence_gnode=egraph_alt.add_node();
+  const event_idt new_fence_gnode=egraph_alt.add_node();
   egraph_alt[new_fence_gnode]=new_fence_event;
   instrumenter.map_vertex_gnode.insert(
     std::make_pair(new_fence_node, new_fence_gnode));
@@ -1457,13 +1457,13 @@ bool instrumentert::is_cfg_spurious(const event_grapht::critical_cyclet& cyc)
     }
     assert(current_po);
 
-    const graph<abstract_eventt>::edgest& pos_cur = egraph.po_out(*e_it);
-    const graph<abstract_eventt>::edgest& pos_next = egraph.po_out(*(++e_it));
+    const wmm_grapht::edgest& pos_cur = egraph.po_out(*e_it);
+    const wmm_grapht::edgest& pos_next = egraph.po_out(*(++e_it));
     --e_it;
 
     bool exists_n = false;
 
-    for(graph<abstract_eventt>::edgest::const_iterator edge_it=pos_cur.begin();
+    for(wmm_grapht::edgest::const_iterator edge_it=pos_cur.begin();
       edge_it!=pos_cur.end(); edge_it++)
     {
       if(pos_next.find(edge_it->first)!=pos_next.end())
@@ -1655,12 +1655,12 @@ void inline instrumentert::print_outputs_local(
   bool hide_internals)
 {
   /* to represent the po aligned in the dot */
-  std::map<unsigned,std::set<unsigned> > same_po;
+  std::map<unsigned,std::set<event_idt> > same_po;
   unsigned max_thread = 0;
   unsigned colour = 0;
 
   /* to represent the files as clusters */
-  std::map<irep_idt,std::set<unsigned> > same_file;
+  std::map<irep_idt,std::set<event_idt> > same_file;
 
   /* to summarise in a table all the variables */
   std::map<std::string,std::string> map_id2var;
@@ -1679,7 +1679,7 @@ void inline instrumentert::print_outputs_local(
       << std::endl;
 
     /* emphasises instrumented events */
-    for(std::list<unsigned>::const_iterator it_e=it->begin();
+    for(std::list<event_idt>::const_iterator it_e=it->begin();
       it_e!=it->end(); it_e++)
     {
       const abstract_eventt& ev = egraph[*it_e];
@@ -1710,7 +1710,7 @@ void inline instrumentert::print_outputs_local(
       {
         dot << "{rank=same; thread_" << i
           << "[shape=plaintext, label=\"thread " << i << "\"];";
-        for(std::set<unsigned>::iterator it=same_po[i].begin();
+        for(std::set<event_idt>::iterator it=same_po[i].begin();
           it!=same_po[i].end(); it++)
           dot << egraph[*it].id << ";";
         dot << "};" << std::endl;
@@ -1718,13 +1718,13 @@ void inline instrumentert::print_outputs_local(
 
   /* clusters events by file/function */
   if(render_by_file || render_by_function)
-    for(std::map<irep_idt,std::set<unsigned> >::const_iterator it=
+    for(std::map<irep_idt,std::set<event_idt> >::const_iterator it=
       same_file.begin();
       it!=same_file.end(); it++)
     {
       dot << "subgraph cluster_" << irep_id_hash()(it->first) << "{" << std::endl;
       dot << "  label=\"" << it->first << "\";" << std::endl;
-      for(std::set<unsigned>::const_iterator ev_it=it->second.begin();
+      for(std::set<event_idt>::const_iterator ev_it=it->second.begin();
         ev_it!=it->second.end(); ev_it++)
       {
         dot << "  " << egraph[*ev_it].id << ";" << std::endl;
@@ -1816,7 +1816,7 @@ void instrumentert::collect_cycles_by_SCCs(memory_modelt model)
   unsigned scc = 0;
   set_of_cycles_per_SCC.resize(num_sccs,
     std::set<event_grapht::critical_cyclet>());
-  for(std::vector<std::set<unsigned> >::const_iterator it=egraph_SCCs.begin();
+  for(std::vector<std::set<event_idt> >::const_iterator it=egraph_SCCs.begin();
     it!=egraph_SCCs.end(); it++)
     if(it->size()>=4)
       egraph.collect_cycles(set_of_cycles_per_SCC[scc++],model,*it);
@@ -1827,12 +1827,12 @@ class pthread_argumentt
 public:
   instrumentert& instr;
   memory_modelt mem;
-  const std::set<unsigned>& filter;
+  const std::set<event_idt>& filter;
   std::set<event_grapht::critical_cyclet>& cycles;
 
   pthread_argumentt(instrumentert& _instr,
     memory_modelt _mem,
-    const std::set<unsigned>& _filter,
+    const std::set<event_idt>& _filter,
     std::set<event_grapht::critical_cyclet>& _cycles)
     :instr(_instr),mem(_mem),filter(_filter),cycles(_cycles)
   {
@@ -1845,7 +1845,7 @@ void* collect_cycles_in_thread(void* arg)
   /* arguments */
   instrumentert& this_instrumenter = ((pthread_argumentt*) arg)->instr;
   memory_modelt model = ((pthread_argumentt*) arg)->mem;
-  const std::set<unsigned>& filter = ((pthread_argumentt*) arg)->filter;
+  const std::set<event_idt>& filter = ((pthread_argumentt*) arg)->filter;
   std::set<event_grapht::critical_cyclet>& cycles =
     ((pthread_argumentt*) arg)->cycles;
 
@@ -1872,7 +1872,7 @@ void instrumentert::collect_cycles_by_SCCs(memory_modelt model)
       interesting_SCCs.insert(scc);
       pthread_argumentt arg(*this,model,*it,set_of_cycles_per_SCC[scc]);
 
-      unsigned rc = pthread_create(&threads[scc++], NULL,
+      int rc = pthread_create(&threads[scc++], NULL,
         collect_cycles_in_thread, (void*) &arg);
 
       message.status()<<(rc!=0?"Failure ":"Success ")
@@ -1882,7 +1882,7 @@ void instrumentert::collect_cycles_by_SCCs(memory_modelt model)
   for(unsigned i=0; i<number_of_sccs; i++)
     if(interesting_SCCs.find(i)!=interesting_SCCs.end())
     {
-      unsigned rc = pthread_join(threads[i],NULL);
+      int rc = pthread_join(threads[i],NULL);
       message.status()<<(rc!=0?"Failure ":"Success ")
         <<"in joining thread for SCC #"<<i<<messaget::eom;
     }
diff --git a/src/goto-instrument/wmm/goto2graph.h b/src/goto-instrument/wmm/goto2graph.h
index 8c66a8a4f63..05e5b2c37ec 100644
--- a/src/goto-instrument/wmm/goto2graph.h
+++ b/src/goto-instrument/wmm/goto2graph.h
@@ -37,8 +37,8 @@ class instrumentert
   goto_functionst &goto_functions;
 
   /* alternative representation of graph (SCC) */
-  std::map<unsigned,unsigned> map_vertex_gnode;
-  graph<abstract_eventt> egraph_alt;
+  std::map<event_idt,event_idt> map_vertex_gnode;
+  wmm_grapht egraph_alt;
 
   unsigned unique_id;
 
@@ -70,7 +70,7 @@ class instrumentert
   void inline instrument_minimum_interference_inserter(
     const set_of_cyclest& set);
   void inline instrument_my_events_inserter(
-    const set_of_cyclest& set, const std::set<unsigned>& events);
+    const set_of_cyclest& set, const std::set<event_idt>& events);
 
   void inline print_outputs_local(
     const std::set<event_grapht::critical_cyclet>& set,
@@ -92,8 +92,8 @@ class instrumentert
 
     /* pointer to the egraph(s) that we construct */
     event_grapht& egraph;
-    std::vector<std::set<unsigned> >& egraph_SCCs;
-    graph<abstract_eventt>& egraph_alt;
+    std::vector<std::set<event_idt> >& egraph_SCCs;
+    wmm_grapht& egraph_alt;
 
     /* for thread marking (dynamic) */
     unsigned current_thread;
@@ -158,8 +158,8 @@ class instrumentert
     unsigned max_thread;
 
     /* relations between irep and Reads/Writes */
-    typedef std::multimap<irep_idt,unsigned> id2nodet;
-    typedef std::pair<irep_idt,unsigned> id2node_pairt;
+    typedef std::multimap<irep_idt,event_idt> id2nodet;
+    typedef std::pair<irep_idt,event_idt> id2node_pairt;
     id2nodet map_reads, map_writes;
 
     unsigned write_counter;
@@ -168,7 +168,7 @@ class instrumentert
     unsigned fr_rf_counter;
 
     /* previous nodes (fwd analysis) */
-    typedef std::pair<unsigned,unsigned> nodet;
+    typedef std::pair<event_idt,event_idt> nodet;
     typedef std::map<goto_programt::instructiont::targett,std::set<nodet> >
       incoming_post;
 
@@ -198,8 +198,8 @@ class instrumentert
     data_dpt data_dp;
 
     /* writes and reads to unknown addresses -- conservative */
-    std::set<unsigned> unknown_read_nodes;
-    std::set<unsigned> unknown_write_nodes;
+    std::set<event_idt> unknown_read_nodes;
+    std::set<event_idt> unknown_write_nodes;
 
     /* set of functions visited so far -- we don't handle recursive functions */
     std::set<irep_idt> functions_met;
@@ -278,7 +278,7 @@ class instrumentert
   event_grapht egraph;
 
   /* graph split into strongly connected components */
-  std::vector<std::set<unsigned> > egraph_SCCs;
+  std::vector<std::set<event_idt> > egraph_SCCs;
 
   /* critical cycles */
   std::set<event_grapht::critical_cyclet> set_of_cycles;
@@ -289,8 +289,8 @@ class instrumentert
 
   /* map from function to begin and end of the corresponding part of the
      graph */
-  typedef std::map<irep_idt,std::pair<std::set<unsigned>,
-    std::set<unsigned> > > map_function_nodest;
+  typedef std::map<irep_idt,std::pair<std::set<event_idt>,
+    std::set<event_idt> > > map_function_nodest;
   map_function_nodest map_function_graph;
 
   void print_map_function_graph() const {
@@ -300,13 +300,13 @@ class instrumentert
     {
        message.debug() << "FUNCTION " << it->first << ": " << messaget::eom;
        message.debug() << "Start nodes: ";
-       for(std::set<unsigned>::const_iterator in_it=it->second.first.begin();
+       for(std::set<event_idt>::const_iterator in_it=it->second.first.begin();
          in_it!=it->second.first.end();
          ++in_it)
          message.debug() << *in_it << " ";
        message.debug() << messaget::eom;
        message.debug() << "End nodes: ";
-       for(std::set<unsigned>::const_iterator in_it=it->second.second.begin();
+       for(std::set<event_idt>::const_iterator in_it=it->second.second.begin();
          in_it!=it->second.second.end();
          ++in_it)
          message.debug() << *in_it << " ";
@@ -366,11 +366,11 @@ class instrumentert
 
   /* strategies for instrumentation */
   void instrument_with_strategy(instrumentation_strategyt strategy);
-  void instrument_my_events(const std::set<unsigned>& events);
+  void instrument_my_events(const std::set<event_idt>& events);
 
   /* retrieves events to filter in the instrumentation choice
      with option --my-events */
-  static std::set<unsigned> extract_my_events();
+  static std::set<event_idt> extract_my_events();
 
   /* sets rendering options */
   void set_rendering_options(bool aligned, bool file, bool function)
diff --git a/src/goto-instrument/wmm/pair_collection.cpp b/src/goto-instrument/wmm/pair_collection.cpp
index 475e094c550..df5d29c4171 100644
--- a/src/goto-instrument/wmm/pair_collection.cpp
+++ b/src/goto-instrument/wmm/pair_collection.cpp
@@ -35,11 +35,11 @@ void event_grapht::graph_pensieve_explorert::collect_pairs(namespacet& ns)
   std::ofstream res;
   res.open("results.txt");
 
-  for(std::list<unsigned>::const_iterator st_it=egraph.po_order.begin();
+  for(std::list<event_idt>::const_iterator st_it=egraph.po_order.begin();
     st_it!=egraph.po_order.end(); ++st_it)
   {
     /* pick X */
-    unsigned first=*st_it;
+    event_idt first=*st_it;
     egraph.message.debug() << "first: " << egraph[first].id << messaget::eom;
 
     if(visited_nodes.find(first)!=visited_nodes.end())
@@ -82,14 +82,14 @@ Function: event_grapht::graph_explorert::find_second_event
 \*******************************************************************/
 
 bool event_grapht::graph_pensieve_explorert::find_second_event(
-  unsigned current)
+  event_idt current)
 {
   if(visited_nodes.find(current)!=visited_nodes.end())
     return false;
 
   visited_nodes.insert(current);
 
-  for(graph<abstract_eventt>::edgest::const_iterator
+  for(wmm_grapht::edgest::const_iterator
     it=egraph.po_out(current).begin();
     it!=egraph.po_out(current).end(); ++it)
   {
diff --git a/src/goto-programs/goto_program_template.h b/src/goto-programs/goto_program_template.h
index 4f76eed1be6..8e8e1c80a4d 100644
--- a/src/goto-programs/goto_program_template.h
+++ b/src/goto-programs/goto_program_template.h
@@ -127,7 +127,7 @@ class goto_program_templatet
 
     //! is this node a branch target?
     inline bool is_target() const
-    { return target_number!=std::numeric_limits<unsigned>::max(); }
+    { return target_number!=nil_target; }
 
     //! clear the node
     inline void clear(goto_program_instruction_typet _type)
@@ -189,7 +189,7 @@ class goto_program_templatet
       type(NO_INSTRUCTION_TYPE),
       guard(true_exprt()),
       location_number(0),
-      target_number(std::numeric_limits<unsigned>::max())
+      target_number(nil_target)
     {
     }
 
@@ -198,7 +198,7 @@ class goto_program_templatet
       type(_type),
       guard(true_exprt()),
       location_number(0),
-      target_number(std::numeric_limits<unsigned>::max())
+      target_number(nil_target)
     {
     }
 
@@ -213,6 +213,10 @@ class goto_program_templatet
       instruction.function.swap(function);
     }
 
+    //! Uniquely identify an invalid target or location
+    static const unsigned nil_target=
+      std::numeric_limits<unsigned>::max();
+
     //! A globally unique number to identify a program location.
     //! It's guaranteed to be ordered in program order within
     //! one goto_program.
@@ -222,7 +226,7 @@ class goto_program_templatet
     unsigned loop_number;
 
     //! A number to identify branch targets.
-    //! This is -1 if it's not a target.
+    //! This is \ref nil_target if it's not a target.
     unsigned target_number;
 
     //! Returns true if the instruction is a backwards branch.
@@ -577,7 +581,7 @@ void goto_program_templatet<codeT, guardT>::compute_target_numbers()
   // reset marking
 
   for(auto & i : instructions)
-    i.target_number=-1;
+    i.target_number=instructiont::nil_target;
 
   // mark the goto targets
 
@@ -612,7 +616,7 @@ void goto_program_templatet<codeT, guardT>::compute_target_numbers()
       if(t!=instructions.end())
       {
         assert(t->target_number!=0);
-        assert(t->target_number!=std::numeric_limits<unsigned>::max());
+        assert(t->target_number!=instructiont::nil_target);
       }
     }
   }
diff --git a/src/musketeer/cycles_visitor.cpp b/src/musketeer/cycles_visitor.cpp
index 7a6c0344571..66936a8fadf 100644
--- a/src/musketeer/cycles_visitor.cpp
+++ b/src/musketeer/cycles_visitor.cpp
@@ -61,24 +61,24 @@ void cycles_visitort::po_edges(std::set<unsigned>& edges)
         {
           /* also add pos of non-delaying pos+ of cycles, as they could AC or
              BC */
-          for(graph<abstract_eventt>::edgest::const_iterator
+          for(wmm_grapht::edgest::const_iterator
             next_it=egraph.po_in(e_i->first).begin();
             next_it!=egraph.po_in(e_i->first).end();
             ++next_it)
           {
-            std::list<unsigned> new_path;
+            std::list<event_idt> new_path;
             new_path.push_back(e_i->first);
             new_path.push_back(next_it->first);
             fence_inserter.const_graph_visitor.const_graph_explore_AC(egraph,
               next_it->first, new_path);
           }
 
-          for(graph<abstract_eventt>::edgest::const_iterator
+          for(wmm_grapht::edgest::const_iterator
             next_it=egraph.po_out(e_i->second).begin();
             next_it!=egraph.po_out(e_i->second).end();
             ++next_it)
           {
-            std::list<unsigned> new_path;
+            std::list<event_idt> new_path;
             new_path.push_back(e_i->second);
             new_path.push_back(next_it->first);
             fence_inserter.const_graph_visitor.const_graph_explore_BC(egraph,
@@ -105,12 +105,12 @@ void cycles_visitort::po_edges(std::set<unsigned>& edges)
       else
       {
         /* adds basic pos from this pos^+ */
-        for(graph<abstract_eventt>::edgest::const_iterator
+        for(wmm_grapht::edgest::const_iterator
           next_it=egraph.po_out(e_i.first).begin();
           next_it!=egraph.po_out(e_i.first).end();
           ++next_it)
         {
-          std::list<unsigned> new_path;
+          std::list<event_idt> new_path;
           new_path.push_back(e_i.first);
           new_path.push_back(next_it->first);
           fence_inserter.const_graph_visitor.const_graph_explore(egraph,
@@ -129,12 +129,12 @@ void cycles_visitort::po_edges(std::set<unsigned>& edges)
         else
         {
           /* adds basic pos from this pos^+ */
-          for(graph<abstract_eventt>::edgest::const_iterator
+          for(wmm_grapht::edgest::const_iterator
             next_it=egraph.po_out(e_i.first).begin();
             next_it!=egraph.po_out(e_i.first).end();
             ++next_it)
           {
-            std::list<unsigned> new_path;
+            std::list<event_idt> new_path;
             new_path.push_back(e_i.first);
             new_path.push_back(next_it->first);
             fence_inserter.const_graph_visitor.const_graph_explore(egraph,
@@ -224,10 +224,10 @@ void cycles_visitort::po_edges(std::set<unsigned>& edges)
         it!=m_threads.end(); ++it)
         if(k_threads.find(*it)!=k_threads.end())
         {
-          const unsigned a=*m_begin[*it];
-          const unsigned b=*m_end[*it];
-          const unsigned c=*k_begin[*it];
-          const unsigned d=*k_end[*it];
+          const event_idt a=*m_begin[*it];
+          const event_idt b=*m_end[*it];
+          const event_idt c=*k_begin[*it];
+          const event_idt d=*k_end[*it];
 
           if(egraph.are_po_ordered(b,c))
             continue;
@@ -406,8 +406,8 @@ void cycles_visitort::com_constraint(
 #if 0
   event_grapht& egraph=instrumenter.egraph;
 
-  std::list<unsigned>::const_iterator e_it=C_j.begin();
-  std::list<unsigned>::const_iterator next_it=e_it;
+  std::list<event_idt>::const_iterator e_it=C_j.begin();
+  std::list<event_idt>::const_iterator next_it=e_it;
   assert(C_j.size()>0);
   ++next_it;
   for(;  next_it!=C_j.end() && e_it!=C_j.end(); ++e_it, ++next_it)
diff --git a/src/musketeer/graph_visitor.cpp b/src/musketeer/graph_visitor.cpp
index dc7cccec97e..e6a627f8d62 100644
--- a/src/musketeer/graph_visitor.cpp
+++ b/src/musketeer/graph_visitor.cpp
@@ -24,13 +24,13 @@ Author: Vincent Nimal
 
 \*******************************************************************/
 
-void const_graph_visitort::graph_explore(event_grapht& egraph, unsigned next,
-  unsigned end, std::list<unsigned>& old_path, std::set<unsigned>& edges)
+void const_graph_visitort::graph_explore(event_grapht& egraph, event_idt next,
+  event_idt end, std::list<event_idt>& old_path, std::set<event_idt>& edges)
 {
   if(next == end) {
     /* inserts all the pos collected from old_path in edges */
-    std::list<unsigned>::const_iterator it=old_path.begin();
-    std::list<unsigned>::const_iterator next_it=it;
+    std::list<event_idt>::const_iterator it=old_path.begin();
+    std::list<event_idt>::const_iterator next_it=it;
     ++next_it;
     for(;next_it!=old_path.end() && it!=old_path.end(); ++it, ++next_it)
     {
@@ -43,7 +43,7 @@ void const_graph_visitort::graph_explore(event_grapht& egraph, unsigned next,
     /* this path is not connecting a to b => return */
   }
   else {
-    for(graph<abstract_eventt>::edgest::const_iterator
+    for(wmm_grapht::edgest::const_iterator
       next_it=egraph.po_out(next).begin();
       next_it!=egraph.po_out(next).end();
       ++next_it)
@@ -71,13 +71,13 @@ void const_graph_visitort::graph_explore(event_grapht& egraph, unsigned next,
 
 \*******************************************************************/
 
-void const_graph_visitort::const_graph_explore(event_grapht& egraph, unsigned next,
-  unsigned end, std::list<unsigned>& old_path)
+void const_graph_visitort::const_graph_explore(event_grapht& egraph, event_idt next,
+  event_idt end, std::list<event_idt>& old_path)
 {
   if(next == end) {
     /* inserts all the pos collected from old_path in edges */
-    std::list<unsigned>::const_iterator it=old_path.begin();
-    std::list<unsigned>::const_iterator next_it=it;
+    std::list<event_idt>::const_iterator it=old_path.begin();
+    std::list<event_idt>::const_iterator next_it=it;
     ++next_it;
     for(;next_it!=old_path.end() && it!=old_path.end(); ++it, ++next_it)
     {
@@ -90,7 +90,7 @@ void const_graph_visitort::const_graph_explore(event_grapht& egraph, unsigned ne
     /* this path is not connecting a to b => return */
   }
   else {
-    for(graph<abstract_eventt>::edgest::const_iterator
+    for(wmm_grapht::edgest::const_iterator
       next_it=egraph.po_out(next).begin();
       next_it!=egraph.po_out(next).end();
       ++next_it)
@@ -118,8 +118,8 @@ void const_graph_visitort::const_graph_explore(event_grapht& egraph, unsigned ne
 
 \*******************************************************************/
 
-void const_graph_visitort::graph_explore_BC(event_grapht& egraph, unsigned next,
-  std::list<unsigned>& old_path, std::set<unsigned>& edges, bool porw)
+void const_graph_visitort::graph_explore_BC(event_grapht& egraph, event_idt next,
+  std::list<event_idt>& old_path, std::set<event_idt>& edges, bool porw)
 {
   /* TODO: restricts to C_1 U ... U C_n for perf improvement */
   assert(old_path.size() > 0);
@@ -133,7 +133,7 @@ void const_graph_visitort::graph_explore_BC(event_grapht& egraph, unsigned next,
 
   /* if all the incoming pos were already visited, add */
   bool no_other_pos = true;
-  for(graph<abstract_eventt>::edgest::const_iterator it=
+  for(wmm_grapht::edgest::const_iterator it=
     egraph.po_out(next).begin();
     it!=egraph.po_out(next).end();
     ++it)
@@ -145,8 +145,8 @@ void const_graph_visitort::graph_explore_BC(event_grapht& egraph, unsigned next,
 
   if(egraph.po_out(next).size()==0 || no_other_pos) {
     /* inserts all the pos collected from old_path in edges */
-    std::list<unsigned>::const_iterator it=old_path.begin();
-    std::list<unsigned>::const_iterator next_it=it;
+    std::list<event_idt>::const_iterator it=old_path.begin();
+    std::list<event_idt>::const_iterator next_it=it;
     ++next_it;
     for(;next_it!=old_path.end() && it!=old_path.end(); ++it, ++next_it)
     {
@@ -159,7 +159,7 @@ void const_graph_visitort::graph_explore_BC(event_grapht& egraph, unsigned next,
     assert(it!=old_path.end());
   }
   else {
-    for(graph<abstract_eventt>::edgest::const_iterator
+    for(wmm_grapht::edgest::const_iterator
       next_it=egraph.po_out(next).begin();
       next_it!=egraph.po_out(next).end();
       ++next_it)
@@ -184,7 +184,7 @@ void const_graph_visitort::graph_explore_BC(event_grapht& egraph, unsigned next,
 \*******************************************************************/
 
 void const_graph_visitort::const_graph_explore_BC(event_grapht& egraph,
-  unsigned next, std::list<unsigned>& old_path)
+  event_idt next, std::list<event_idt>& old_path)
 {
   /* TODO: restricts to C_1 U ... U C_n */
   assert(old_path.size() > 0);
@@ -195,7 +195,7 @@ void const_graph_visitort::const_graph_explore_BC(event_grapht& egraph,
 
   /* if all the incoming pos were already visited, add */
   bool no_other_pos = true;
-  for(graph<abstract_eventt>::edgest::const_iterator it=
+  for(wmm_grapht::edgest::const_iterator it=
     egraph.po_out(next).begin();
     it!=egraph.po_out(next).end();
     ++it)
@@ -207,8 +207,8 @@ void const_graph_visitort::const_graph_explore_BC(event_grapht& egraph,
 
   if(egraph.po_out(next).size()==0 || no_other_pos) {
     /* inserts all the pos collected from old_path in edges */
-    std::list<unsigned>::const_iterator it=old_path.begin();
-    std::list<unsigned>::const_iterator next_it=it;
+    std::list<event_idt>::const_iterator it=old_path.begin();
+    std::list<event_idt>::const_iterator next_it=it;
     ++next_it;
     for(;next_it!=old_path.end() && it!=old_path.end(); ++it, ++next_it)
     {
@@ -222,7 +222,7 @@ void const_graph_visitort::const_graph_explore_BC(event_grapht& egraph,
     assert(it!=old_path.end());
   }
   else {
-    for(graph<abstract_eventt>::edgest::const_iterator
+    for(wmm_grapht::edgest::const_iterator
       next_it=egraph.po_out(next).begin();
       next_it!=egraph.po_out(next).end();
       ++next_it)
@@ -246,8 +246,8 @@ void const_graph_visitort::const_graph_explore_BC(event_grapht& egraph,
 
 \*******************************************************************/
 
-void const_graph_visitort::graph_explore_AC(event_grapht& egraph, unsigned next,
-  std::list<unsigned>& old_path, std::set<unsigned>& edges, bool porw)
+void const_graph_visitort::graph_explore_AC(event_grapht& egraph, event_idt next,
+  std::list<event_idt>& old_path, std::set<event_idt>& edges, bool porw)
 {
   /* TODO: restricts to C_1 U ... U C_n */
   assert(old_path.size() > 0);
@@ -261,7 +261,7 @@ void const_graph_visitort::graph_explore_AC(event_grapht& egraph, unsigned next,
 
   /* if all the incoming pos were already visited, add */
   bool no_other_pos = true;
-  for(graph<abstract_eventt>::edgest::const_iterator it=
+  for(wmm_grapht::edgest::const_iterator it=
     egraph.po_in(next).begin();
     it!=egraph.po_in(next).end();
     ++it)
@@ -273,8 +273,8 @@ void const_graph_visitort::graph_explore_AC(event_grapht& egraph, unsigned next,
 
   if(egraph.po_in(next).size()==0 || no_other_pos) {
     /* inserts all the pos collected from old_path in edges */
-    std::list<unsigned>::const_iterator it=old_path.begin();
-    std::list<unsigned>::const_iterator next_it=it;
+    std::list<event_idt>::const_iterator it=old_path.begin();
+    std::list<event_idt>::const_iterator next_it=it;
     ++next_it;
     for(;next_it!=old_path.end() && it!=old_path.end(); ++it, ++next_it)
     {
@@ -287,7 +287,7 @@ void const_graph_visitort::graph_explore_AC(event_grapht& egraph, unsigned next,
     assert(it!=old_path.end());
   }
   else {
-    for(graph<abstract_eventt>::edgest::const_iterator
+    for(wmm_grapht::edgest::const_iterator
       next_it=egraph.po_in(next).begin();
       next_it!=egraph.po_in(next).end();
       ++next_it)
@@ -312,7 +312,7 @@ void const_graph_visitort::graph_explore_AC(event_grapht& egraph, unsigned next,
 \*******************************************************************/
 
 void const_graph_visitort::const_graph_explore_AC(event_grapht& egraph,
-  unsigned next, std::list<unsigned>& old_path)
+  event_idt next, std::list<event_idt>& old_path)
 {
   /* TODO: restricts to C_1 U ... U C_n */
   assert(old_path.size() > 0);
@@ -323,7 +323,7 @@ void const_graph_visitort::const_graph_explore_AC(event_grapht& egraph,
 
   /* if all the incoming pos were already visited, add */
   bool no_other_pos = true;
-  for(graph<abstract_eventt>::edgest::const_iterator it=
+  for(wmm_grapht::edgest::const_iterator it=
     egraph.po_in(next).begin();
     it!=egraph.po_in(next).end();
     ++it)
@@ -336,8 +336,8 @@ void const_graph_visitort::const_graph_explore_AC(event_grapht& egraph,
   /* if beginning of the thread */
   if(egraph.po_in(next).size()==0 || no_other_pos) {
     /* inserts all the pos collected from old_path in edges */
-    std::list<unsigned>::const_iterator it=old_path.begin();
-    std::list<unsigned>::const_iterator next_it=it;
+    std::list<event_idt>::const_iterator it=old_path.begin();
+    std::list<event_idt>::const_iterator next_it=it;
     ++next_it;
     for(;next_it!=old_path.end() && it!=old_path.end(); ++it, ++next_it)
     {
@@ -351,7 +351,7 @@ void const_graph_visitort::const_graph_explore_AC(event_grapht& egraph,
     assert(it!=old_path.end());
   }
   else {
-    for(graph<abstract_eventt>::edgest::const_iterator
+    for(wmm_grapht::edgest::const_iterator
       next_it=egraph.po_in(next).begin();
       next_it!=egraph.po_in(next).end();
       ++next_it)
@@ -380,7 +380,7 @@ void const_graph_visitort::PT(const edget& e, std::set<unsigned>& edges) {
 
 //  if(!e.is_po) /* e is in po^+\po */ is_po is a flag set manually, do not
 //  use it for checks!!
-  const graph<abstract_eventt>::edgest& list_po_out=
+  const wmm_grapht::edgest& list_po_out=
     fence_inserter.instrumenter.egraph.po_out(e.first);
   if(list_po_out.find(e.second)==list_po_out.end())
   {
@@ -388,12 +388,12 @@ void const_graph_visitort::PT(const edget& e, std::set<unsigned>& edges) {
     event_grapht& egraph=fence_inserter.instrumenter.egraph;
 
     /* all the pos inbetween */
-    for(graph<abstract_eventt>::edgest::const_iterator
+    for(wmm_grapht::edgest::const_iterator
       next_it=egraph.po_out(e.first).begin();
       next_it!=egraph.po_out(e.first).end();
       ++next_it)
     {
-      std::list<unsigned> new_path;
+      std::list<event_idt> new_path;
       new_path.push_back(e.first);
       new_path.push_back(next_it->first);
       graph_explore(egraph, next_it->first, e.second, new_path, edges);
@@ -434,9 +434,9 @@ void const_graph_visitort::CT(const edget& edge, std::set<unsigned>& edges) {
   const abstract_eventt& test_second=egraph[edge.second];
   assert(test_first.operation!=test_second.operation);
 
-  const unsigned first=
+  const event_idt first=
     (test_first.operation==abstract_eventt::Write?edge.first:edge.second);
-  const unsigned second=
+  const event_idt second=
     (test_second.operation==abstract_eventt::Read?edge.second:edge.first);
 
   /* TODO: AC + restricts to C_1 U ... U C_n */
@@ -444,24 +444,24 @@ void const_graph_visitort::CT(const edget& edge, std::set<unsigned>& edges) {
 
   /* if one event only on this thread of the cycle, discard */
   if(egraph.po_in(first).size() > 0)
-    for(graph<abstract_eventt>::edgest::const_iterator
+    for(wmm_grapht::edgest::const_iterator
       next_it=egraph.po_in(first).begin();
       next_it!=egraph.po_in(first).end();
       ++next_it)
     {
-      std::list<unsigned> new_path;
+      std::list<event_idt> new_path;
       new_path.push_back(first);
       new_path.push_back(next_it->first);
       graph_explore_AC(egraph, next_it->first, new_path, edges);
     }
 
   if(egraph.po_out(second).size() > 0)
-    for(graph<abstract_eventt>::edgest::const_iterator
+    for(wmm_grapht::edgest::const_iterator
       next_it=egraph.po_out(second).begin();
       next_it!=egraph.po_out(second).end();
       ++next_it)
     {
-      std::list<unsigned> new_path;
+      std::list<event_idt> new_path;
       new_path.push_back(second);
       new_path.push_back(next_it->first);
       graph_explore_BC(egraph, next_it->first, new_path, edges);
@@ -490,33 +490,33 @@ void const_graph_visitort::CT_not_powr(const edget& edge,
   const abstract_eventt& test_second=egraph[edge.second];
   assert(test_first.operation!=test_second.operation);
 
-  const unsigned first=
+  const event_idt first=
     (test_first.operation==abstract_eventt::Write?edge.first:edge.second);
-  const unsigned second=
+  const event_idt second=
     (test_second.operation==abstract_eventt::Read?edge.second:edge.first);
 
   /* TODO: AC + restricts to C_1 U ... U C_n */
   visited_nodes.clear();
 
   if(egraph.po_in(first).size() > 0)
-    for(graph<abstract_eventt>::edgest::const_iterator
+    for(wmm_grapht::edgest::const_iterator
       next_it=egraph.po_in(first).begin();
       next_it!=egraph.po_in(first).end();
       ++next_it)
     {
-      std::list<unsigned> new_path;
+      std::list<event_idt> new_path;
       new_path.push_back(first);
       new_path.push_back(next_it->first);
       graph_explore_AC(egraph, next_it->first, new_path, edges, true);
     }
 
   if(egraph.po_out(second).size() > 0)
-    for(graph<abstract_eventt>::edgest::const_iterator
+    for(wmm_grapht::edgest::const_iterator
       next_it=egraph.po_out(second).begin();
       next_it!=egraph.po_out(second).end();
       ++next_it)
     {
-      std::list<unsigned> new_path;
+      std::list<event_idt> new_path;
       new_path.push_back(second);
       new_path.push_back(next_it->first);
       graph_explore_BC(egraph, next_it->first, new_path, edges, true);