diff --git a/src/arachne.c b/src/arachne.c
index 551624f..9a37f14 100644
--- a/src/arachne.c
+++ b/src/arachne.c
@@ -39,6 +39,7 @@
 #include "prune_theorems.h"
 #include "arachne.h"
 #include "hidelevel.h"
+#include "depend.h"
 
 extern int *graph;
 extern int nodes;
@@ -700,9 +701,9 @@ create_decryptor (const Term term, const Term key)
   else
     {
       globalError++;
-      printf ("Term for which a decryptor instance is requested: ");
+      eprintf ("Term for which a decryptor instance is requested: ");
       termPrint (term);
-      printf ("\n");
+      eprintf ("\n");
       error
 	("Trying to build a decryptor instance for a non-encrypted term.");
     }
@@ -777,15 +778,15 @@ bind_existing_to_goal (const Binding b, const int run, const int index)
 #ifdef DEBUG
     if (DEBUGL (4))
       {
-	printf ("Trying to bind the small term ");
+	eprintf ("Trying to bind the small term ");
 	termPrint (b->term);
-	printf (" as coming from the big send ");
+	eprintf (" as coming from the big send ");
 	termPrint (rd->message);
-	printf (" , binding ");
+	eprintf (" , binding ");
 	termPrint (b->term);
-	printf ("\nCrypted list needed: ");
+	eprintf ("\nCrypted list needed: ");
 	termlistPrint (cryptlist);
-	printf ("\n");
+	eprintf ("\n");
       }
 #endif
     if (cryptlist != NULL && switches.output == PROOF)
@@ -893,6 +894,8 @@ bind_existing_to_goal (const Binding b, const int run, const int index)
 	    indentDepth++;
 	    flag = flag && iterate ();
 	    indentDepth--;
+
+	    goal_unbind (b);
 	  }
 	else
 	  {
@@ -906,7 +909,6 @@ bind_existing_to_goal (const Binding b, const int run, const int index)
 	semiRunDestroy ();
 	newruns--;
       }
-    goal_unbind (b);
 
     indentDepth--;
     return flag;
@@ -1099,17 +1101,17 @@ bind_old_goal (const Binding b_new)
 	  if (b_old->done && isTermEqual (b_new->term, b_old->term))
 	    {
 	      // Old is done and has the same term!
-	      // So we copy this binding, and fix it.
-	      b_new->run_from = b_old->run_from;
-	      b_new->ev_from = b_old->ev_from;
-	      b_new->done = 1;
-	      return 1;
+	      // So we try to copy this binding, and fix it.
+	      if (goal_bind (b_new, b_old->run_from, b_old->ev_from))
+		{
+		  return true;
+		}
 	    }
 	  bl = bl->next;
 	}
     }
   // No old binding to connect to
-  return 0;
+  return false;
 }
 
 //! Create a new intruder run to generate knowledge from m0
@@ -1154,12 +1156,12 @@ bind_goal_new_m0 (const Binding b)
 		    eprintf (" from the initial knowledge.\n");
 		  }
 		flag = flag && iterate ();
+		goal_unbind (b);
 	      }
 	    else
 	      {
 		proof_cannot_bind (b, run, 0);
 	      }
-	    goal_unbind (b);
 	    indentDepth--;
 	  }
 	  semiRunDestroy ();
@@ -1247,12 +1249,12 @@ bind_goal_new_encrypt (const Binding b)
 	    {
 	      proof_suppose_binding (b);
 	      flag = flag && iterate ();
+	      goal_unbind (b);
 	    }
 	  else
 	    {
 	      proof_cannot_bind (b, run, index);
 	    }
-	  goal_unbind (b);
 	  indentDepth--;
 	  goal_remove_last (newgoals);
 	  semiRunDestroy ();
@@ -1475,7 +1477,7 @@ bind_goal (const Binding b)
 	  flag = flag && iterate ();
 
 	  // Unbind again
-	  b->done = 0;
+	  goal_unbind (b);
 	  indentDepth--;
 	  return flag;
 	}
@@ -2215,7 +2217,6 @@ knowledgeAtArachne (const System sys, const int myrun, const int myindex,
   Knowledge know;
   int run;
 
-  goal_graph_create ();		// ensure a valid ordering graph
   know = knowledgeDuplicate (sys->know);	// duplicate initial knowledge
   run = 0;
   while (run < sys->maxruns)
@@ -2236,7 +2237,7 @@ knowledgeAtArachne (const System sys, const int myrun, const int myindex,
       while (rd != NULL && index < maxheight)
 	{
 	  // Check whether this event precedes myevent
-	  if (aftercomplete || isOrderedBefore (run, index, myrun, myindex))
+	  if (aftercomplete || isDependEvent (run, index, myrun, myindex))
 	    {
 	      // If it is a send (trivial) or a read (remarkable, but true
 	      // because of bindings) we can add the message and the agents to
diff --git a/src/attackminimize.c b/src/attackminimize.c
index 7be51af..bd186df 100644
--- a/src/attackminimize.c
+++ b/src/attackminimize.c
@@ -92,7 +92,7 @@ attackMinimize (const System sys, struct tracebuf *tb)
 	    }
 	  if (i == tb->length)
 	    {
-	      printf ("Some step error.\n");
+	      eprintf ("Some step error.\n");
 	      exit (1);
 	    }
 
@@ -119,7 +119,7 @@ attackMinimize (const System sys, struct tracebuf *tb)
 	    }
 	  if (i < 0)
 	    {
-	      printf ("Some i<0 error.\n");
+	      eprintf ("Some i<0 error.\n");
 	      exit (1);
 	    }
 
diff --git a/src/binding.c b/src/binding.c
index 49dce05..7ca250e 100644
--- a/src/binding.c
+++ b/src/binding.c
@@ -14,22 +14,14 @@
 #include "termmap.h"
 #include "arachne.h"
 #include "switches.h"
+#include "depend.h"
 #include <malloc.h>
 
 static System sys;		//!< local storage of system pointer
-int *graph = NULL;		//!< graph data
-int nodes = 0;			//!< number of nodes in the graph
-int graph_uordblks = 0;
 
 extern Protocol INTRUDER;	//!< The intruder protocol
 extern Role I_M;		//!< special role; precedes all other events always
 
-/*
- * Forward declarations
- */
-
-void goal_graph_destroy ();
-
 /*
  *
  * Assist stuff
@@ -43,13 +35,12 @@ binding_create (Term term, int run_to, int ev_to)
   Binding b;
 
   b = memAlloc (sizeof (struct binding));
-  b->done = 0;
-  b->blocked = 0;
+  b->done = false;
+  b->blocked = false;
   b->run_from = -1;
   b->ev_from = -1;
   b->run_to = run_to;
   b->ev_to = ev_to;
-  goal_graph_destroy ();
   b->term = term;
   b->level = 0;
   return b;
@@ -66,17 +57,6 @@ binding_destroy (Binding b)
   memFree (b, sizeof (struct binding));
 }
 
-//! Test whether one event is ordered before another
-/**
- * Is only guaranteed to yield trustworthy results after a new graph is created, using
- * goal_graph_create ()
- */
-int
-isOrderedBefore (const int run1, const int ev1, const int run2, const int ev2)
-{
-  return graph[graph_nodes (nodes, run2, ev2, run2, ev2)];
-}
-
 /*
  *
  * Main
@@ -89,9 +69,8 @@ bindingInit (const System mysys)
 {
   sys = mysys;
   sys->bindings = NULL;
-  graph = NULL;
-  nodes = 0;
-  graph_uordblks = 0;
+
+  dependInit (sys);
 }
 
 //! Close up
@@ -101,262 +80,12 @@ bindingDone ()
   int delete (Binding b)
   {
     binding_destroy (b);
-    return 1;
+    return true;
   }
   list_iterate (sys->bindings, delete);
   list_destroy (sys->bindings);
-}
 
-//! Destroy graph
-void
-goal_graph_destroy ()
-{
-  if (graph != NULL)
-    {
-#ifdef DEBUG
-      struct mallinfo mi_free;
-      int mem_free;
-
-      mi_free = mallinfo ();
-      mem_free = mi_free.uordblks;
-#endif
-      memFree (graph, (nodes * nodes) * sizeof (int));
-      graph = NULL;
-#ifdef DEBUG
-      mi_free = mallinfo ();
-      if (mem_free - mi_free.uordblks != graph_uordblks)
-	error ("Freeing gave a weird result.");
-#endif
-      graph_uordblks = 0;
-      nodes = 0;
-    }
-}
-
-//! Compute unclosed graph
-void
-goal_graph_create ()
-{
-  int run, ev;
-  int last_m;
-  List bl;
-
-  goal_graph_destroy ();
-
-  // Setup graph
-  nodes = node_count ();
-
-  {
-    struct mallinfo create_mi;
-    int create_mem_before;
-
-    if (graph_uordblks != 0)
-      error
-	("Trying to create graph stuff without 0 uordblks for it first, but it is %i.",
-	 graph_uordblks);
-    create_mi = mallinfo ();
-    create_mem_before = create_mi.uordblks;
-    graph = memAlloc ((nodes * nodes) * sizeof (int));
-    create_mi = mallinfo ();
-    graph_uordblks = create_mi.uordblks - create_mem_before;
-  }
-
-  {
-
-    graph_fill (graph, nodes, 0);
-
-    // Setup run order
-    run = 0;
-    last_m = -1;		// last I_M run
-    while (run < sys->maxruns)
-      {
-	ev = 1;
-	//!@todo This now reference to step, but we intend "length" as in Arachne.
-	while (ev < sys->runs[run].step)
-	  {
-	    graph[graph_nodes (nodes, run, ev - 1, run, ev)] = 1;
-	    ev++;
-	  }
-	// Enforce I_M ordering
-	if (sys->runs[run].protocol == INTRUDER && sys->runs[run].role == I_M)
-	  {
-	    if (last_m != -1)
-	      {
-		graph[graph_nodes (nodes, last_m, 0, run, 0)] = 1;
-	      }
-	    last_m = run;
-	  }
-	// Next
-	run++;
-      }
-    // Setup bindings order
-    bl = sys->bindings;
-    while (bl != NULL)
-      {
-	Binding b;
-
-	b = (Binding) bl->data;
-	if (valid_binding (b))
-	  {
-#ifdef DEBUG
-	    if (graph_nodes
-		(nodes, b->run_from, b->ev_from, b->run_to,
-		 b->ev_to) >= (nodes * nodes))
-	      error ("Node out of scope for %i,%i -> %i,%i.\n", b->run_from,
-		     b->ev_from, b->run_to, b->ev_to);
-#endif
-	    graph[graph_nodes
-		  (nodes, b->run_from, b->ev_from, b->run_to, b->ev_to)] = 1;
-	  }
-	bl = bl->next;
-      }
-    // Setup local constants order
-    run = 0;
-    while (run < sys->maxruns)
-      {
-	if (sys->runs[run].protocol != INTRUDER)
-	  {
-	    int run2;
-
-	    run2 = 0;
-	    while (run2 < sys->maxruns)
-	      {
-		if (sys->runs[run].protocol != INTRUDER && run != run2)
-		  {
-		    // For these two runs, we check whether run has any variables that are mapped
-		    // to constants from run2
-		    Termlist tl;
-
-		    tl = sys->runs[run].locals;
-		    while (tl != NULL)
-		      {
-			Term t;
-
-			t = tl->term;
-			if (t->type == VARIABLE && TermRunid (t) == run
-			    && t->subst != NULL)
-			  {
-			    // t is a variable of run
-			    Termlist tl2;
-
-			    tl2 = sys->runs[run2].locals;
-			    while (tl2 != NULL)
-			      {
-				Term t2;
-
-				t2 = tl2->term;
-				if (realTermLeaf (t2) && t2->type != VARIABLE
-				    && TermRunid (t2) == run2)
-				  {
-				    // t2 is a constant of run2
-				    if (isTermEqual (t, t2))
-				      {
-					// Indeed, run depends on the run2 constant t2. Thus we must store this order.
-					// The first send of t2 in run2 must be before the first (read) event in run with t2.
-					int ev2;
-					int done;
-					Roledef rd2;
-
-					done = 0;
-					ev2 = 0;
-					rd2 = sys->runs[run2].start;
-					while (!done
-					       && ev2 < sys->runs[run2].step)
-					  {
-					    if (rd2->type == SEND
-						&& termSubTerm (rd2->message,
-								t2))
-					      {
-						// Allright, we send it here at ev2 first
-						int ev;
-						Roledef rd;
-
-						ev = 0;
-						rd = sys->runs[run].start;
-						while (!done
-						       && ev <
-						       sys->runs[run].step)
-						  {
-						    if (termSubTerm
-							(rd->message, t2))
-						      {
-							// Term occurs here in run
-							if (rd->type == READ)
-							  {
-							    // It's read here first.
-							    // Order and be done with it.
-							    graph[graph_nodes
-								  (nodes,
-								   run2, ev2,
-								   run, ev)] =
-							      1;
-#ifdef DEBUG
-							    if (DEBUGL (5))
-							      {
-								eprintf
-								  ("* [local originator] term ");
-								termPrint
-								  (t2);
-								eprintf
-								  (" is bound using %i, %i before %i,%i\n",
-								   run2, ev2,
-								   run, ev);
-							      }
-#endif
-							    done = 1;
-							  }
-							else
-							  {
-							    // It doesn't occur first in a READ, which shouldn't be happening
-							    if (switches.
-								output ==
-								PROOF)
-							      {
-								eprintf
-								  ("Term ");
-								termPrint
-								  (t2);
-								eprintf
-								  (" from run %i occurs in run %i, term ",
-								   run2, run);
-								termPrint (t);
-								eprintf
-								  (" before it is read?\n");
-							      }
-							    // Thus, we create an artificial loop
-							    if (sys->runs[0].
-								step > 1)
-							      {
-								// This forces a loop, and thus prunes
-								graph
-								  [graph_nodes
-								   (nodes, 0,
-								    1, 0,
-								    0)] = 1;
-							      }
-							  }
-						      }
-						    rd = rd->next;
-						    ev++;
-						  }
-						done = 1;
-					      }
-					    rd2 = rd2->next;
-					    ev2++;
-					  }
-				      }
-				  }
-				tl2 = tl2->next;
-			      }
-			  }
-			tl = tl->next;
-		      }
-		  }
-		run2++;
-	      }
-	  }
-	run++;
-      }
-  }
+  dependDone (sys);
 }
 
 
@@ -366,67 +95,6 @@ goal_graph_create ()
  *
  */
 
-//! Yield node count
-int
-node_count ()
-{
-  int count;
-  int run;
-
-  count = 0;
-  for (run = 0; run < sys->maxruns; run++)
-    {
-      //!@todo This now reference to step, but we intend "length" as in Arachne.
-      count = count + sys->runs[run].step;
-    }
-  return count;
-}
-
-//! Yield node number given run, ev
-__inline__ int
-node_number (int run, int ev)
-{
-  int node;
-
-  node = ev;
-  while (run > 0)
-    {
-      run--;
-      //!@todo This now reference to step, but we intend "length" as in Arachne.
-      node = node + sys->runs[run].step;
-    }
-  return node;
-}
-
-//! Yield graph index, given node1, node2 numbers
-__inline__ int
-graph_index (const int node1, const int node2)
-{
-  return ((node1 * nodes) + node2);
-}
-
-//! Yield graph index, given (node1), (node2) tuples
-__inline__ int
-graph_nodes (const int nodes, const int run1, const int ev1, const int run2,
-	     const int ev2)
-{
-  int node1;
-  int node2;
-
-  node1 = node_number (run1, ev1);
-#ifdef DEBUG
-  if (node1 < 0 || node1 >= nodes)
-    error ("node_number %i out of scope %i for %i,%i.", node1, nodes, run1,
-	   ev1);
-#endif
-  node2 = node_number (run2, ev2);
-#ifdef DEBUG
-  if (node2 < 0 || node2 >= nodes)
-    error ("node_number %i out of scope %i for %i,%i.", node2, nodes, run2,
-	   ev2);
-#endif
-  return graph_index (node1, node2);
-}
 
 //! Print a binding (given a binding list pointer)
 int
@@ -440,7 +108,86 @@ binding_print (const Binding b)
   eprintf (" )->> (%i,%i)", b->run_to, b->ev_to);
   if (b->blocked)
     eprintf ("[blocked]");
-  return 1;
+  return true;
+}
+
+//! Bind a goal (true if success, false if it must be pruned)
+int
+goal_bind (const Binding b, const int run, const int ev)
+{
+  if (b->blocked)
+    {
+      error ("Trying to bind a blocked goal.");
+    }
+  if (!b->done)
+    {
+#ifdef DEBUG
+      if (run >= sys->maxruns || sys->runs[run].step <= ev)
+	error ("Trying to bind to something not yet in the semistate.");
+#endif
+      b->run_from = run;
+      b->ev_from = ev;
+      if (dependPushEvent (run, ev, b->run_to, b->ev_to))
+	{
+	  b->done = true;
+	  return true;
+	}
+    }
+  else
+    {
+      globalError++;
+      binding_print (b);
+      error ("Trying to bind a bound goal again.");
+    }
+  return false;
+}
+
+//! Unbind a goal
+void
+goal_unbind (const Binding b)
+{
+  if (b->done)
+    {
+      dependPopEvent ();
+      b->done = false;
+    }
+  else
+    {
+      error ("Trying to unbind an unbound goal again.");
+    }
+}
+
+//! Bind a goal as a dummy (block)
+/**
+ * Especially made for tuple expansion
+ */
+int
+binding_block (Binding b)
+{
+  if (!b->blocked)
+    {
+      b->blocked = true;
+      return true;
+    }
+  else
+    {
+      error ("Trying to block a goal again.");
+    }
+}
+
+//! Unblock a binding
+int
+binding_unblock (Binding b)
+{
+  if (b->blocked)
+    {
+      b->blocked = false;
+      return true;
+    }
+  else
+    {
+      error ("Trying to unblock a non-blocked goal.");
+    }
 }
 
 
@@ -448,6 +195,8 @@ binding_print (const Binding b)
 /**
  * The int parameter 'level' is just to store additional info. Here, it stores priorities for a goal.
  * Higher level goals will be selected first. Typically, a normal goal is level 0, a key is 1.
+ *
+ * Returns the number of added goals (sometimes unfolding tuples)
  */
 int
 goal_add (Term term, const int run, const int ev, const int level)
@@ -479,11 +228,11 @@ goal_add (Term term, const int run, const int ev, const int level)
 	b = (Binding) data;
 	if (isTermEqual (b->term, term) && run == b->run_to && ev == b->ev_to)
 	  {			// abort scan, report
-	    return 0;
+	    return false;
 	  }
 	else
 	  {			// proceed with scan
-	    return 1;
+	    return true;
 	  }
       }
 
@@ -509,46 +258,6 @@ goal_add (Term term, const int run, const int ev, const int level)
   return 0;
 }
 
-//! Add a goal, and bind it immediately.
-// If the result is negative, no goals will have been added, as the resulting state must be pruned (cycle) */
-int
-goal_add_fixed (Term term, const int run, const int ev, const int fromrun,
-		const int fromev)
-{
-  int newgoals, n;
-  List l;
-  int res;
-
-  newgoals = goal_add (term, run, ev, 0);
-  l = sys->bindings;
-  n = newgoals;
-  res = 1;
-  while (res != 0 && n > 0 && l != NULL)
-    {
-      Binding b;
-
-      b = (Binding) l->data;
-      if (b->done)
-	{
-	  globalError++;
-	  binding_print (b);
-	  error (" problem with new fixed binding!");
-	}
-      res = goal_bind (b, fromrun, fromev);	// returns 0 if it must be pruned
-      l = l->next;
-      n--;
-    }
-  if (res != 0)
-    {
-      return newgoals;
-    }
-  else
-    {
-      goal_remove_last (newgoals);
-      return -1;
-    }
-}
-
 //! Remove a goal
 void
 goal_remove_last (int n)
@@ -573,82 +282,6 @@ goal_remove_last (int n)
     }
 }
 
-//! Bind a goal (0 if it must be pruned)
-int
-goal_bind (const Binding b, const int run, const int ev)
-{
-  if (b->blocked)
-    {
-      error ("Trying to bind a blocked goal.");
-    }
-  if (!b->done)
-    {
-#ifdef DEBUG
-      if (run >= sys->maxruns || sys->runs[run].step <= ev)
-	error ("Trying to bind to something not yet in the semistate.");
-#endif
-      b->done = 1;
-      b->run_from = run;
-      b->ev_from = ev;
-      goal_graph_create ();
-      return warshall (graph, nodes);
-    }
-  else
-    {
-      globalError++;
-      binding_print (b);
-      error ("Trying to bind a bound goal again.");
-    }
-}
-
-//! Unbind a goal
-void
-goal_unbind (const Binding b)
-{
-  if (b->done)
-    {
-      goal_graph_destroy (b);
-      b->done = 0;
-    }
-  else
-    {
-      error ("Trying to unbind an unbound goal again.");
-    }
-}
-
-//! Bind a goal as a dummy (block)
-/**
- * Especially made for tuple expansion
- */
-int
-binding_block (Binding b)
-{
-  if (!b->blocked)
-    {
-      b->blocked = 1;
-      return 1;
-    }
-  else
-    {
-      error ("Trying to block a goal again.");
-    }
-}
-
-//! Unblock a binding
-int
-binding_unblock (Binding b)
-{
-  if (b->blocked)
-    {
-      b->blocked = 0;
-      return 1;
-    }
-  else
-    {
-      error ("Trying to unblock a non-blocked goal.");
-    }
-}
-
 //! Determine whether some label set is ordered w.r.t. send/read order.
 /**
  * Assumes all these labels exist in the system, within length etc, and that the run mappings are valid.
@@ -656,12 +289,6 @@ binding_unblock (Binding b)
 int
 labels_ordered (Termmap runs, Termlist labels)
 {
-  goal_graph_create ();
-  if (warshall (graph, nodes) == 0)
-    {
-      error ("Testing ordering of label set for a graph with a cycle.");
-    }
-
   while (labels != NULL)
     {
       // Given this label, and the mapping of runs, we want to know if the order is okay. Thus, we need to know sendrole and readrole
@@ -693,17 +320,16 @@ labels_ordered (Termmap runs, Termlist labels)
       read_run = termmapGet (runs, linfo->readrole);
       send_ev = get_index (send_run);
       read_ev = get_index (read_run);
-      if (graph[graph_nodes (nodes, send_run, send_ev, read_run, read_ev)] ==
-	  0)
+      if (!isDependEvent (send_run, send_ev, read_run, read_ev))
 	{
 	  // Not ordered; false
-	  return 0;
+	  return false;
 	}
 
       // Proceed
       labels = labels->next;
     }
-  return 1;
+  return true;
 }
 
 //! Check whether the binding denotes a sensible thing such that we can use run_from and ev_from
@@ -711,9 +337,9 @@ int
 valid_binding (Binding b)
 {
   if (b->done && !b->blocked)
-    return 1;
+    return true;
   else
-    return 0;
+    return false;
 }
 
 //! Check for unique origination
@@ -774,7 +400,7 @@ unique_origination ()
 			      b->ev_from != b2->ev_from)
 			    {
 			      // Not equal: thus no unique origination.
-			      return 0;
+			      return false;
 			    }
 			}
 		      termlistDelete (terms2);
@@ -787,7 +413,7 @@ unique_origination ()
 	}
       bl = bl->next;
     }
-  return 1;
+  return true;
 }
 
 //! Prune invalid state w.r.t. <=C minimal requirement
@@ -799,92 +425,5 @@ unique_origination ()
 int
 bindings_c_minimal ()
 {
-  List bl;
-
-  if (switches.experimental & 1 > 0)
-    {
-      if (unique_origination () == 0)
-	{
-	  return 0;
-	}
-    }
-
-  // Ensure a fresh state graph
-  goal_graph_create ();
-  // Recompute closure; does that work?
-  if (!warshall (graph, nodes))
-    {
-      List l;
-
-      globalError++;
-      l = sys->bindings;
-      while (l != NULL)
-	{
-	  Binding b;
-
-	  b = (Binding) l->data;
-	  binding_print (b);
-	  eprintf ("\n");
-	  l = l->next;
-	}
-      error ("Detected a cycle when testing for c-minimality");
-    }
-
-  // For all goals
-  bl = sys->bindings;
-  while (bl != NULL)
-    {
-      Binding b;
-
-      b = (Binding) bl->data;
-      // Check for a valid binding; it has to be 'done' and sensibly bound (not as in tuple expanded stuff)
-      if (valid_binding (b))
-	{
-	  int run;
-	  int node_from;
-
-	  node_from = node_number (b->run_from, b->ev_from);
-	  // Find all preceding events
-	  for (run = 0; run < sys->maxruns; run++)
-	    {
-	      int ev;
-
-	      //!@todo hardcoded reference to step, should be length
-	      for (ev = 0; ev < sys->runs[run].step; ev++)
-		{
-		  int node_comp;
-
-		  node_comp = node_number (run, ev);
-		  if (graph[graph_index (node_comp, node_from)] > 0)
-		    {
-		      // this node is *before* the from node
-		      Roledef rd;
-
-		      rd = roledef_shift (sys->runs[run].start, ev);
-		      if (termInTerm (rd->message, b->term))
-			{
-			  // This term already occurs as interm in a previous node!
-#ifdef DEBUG
-			  if (DEBUGL (4))
-			    {
-			      // Report this
-			      indentPrint ();
-			      eprintf ("Binding for ");
-			      termPrint (b->term);
-			      eprintf
-				(" at r%i i%i is not c-minimal because it occurred before at r%i i%i in ",
-				 b->run_from, b->ev_from, run, ev);
-			      termPrint (rd->message);
-			      eprintf ("\n");
-			    }
-#endif
-			  return 0;
-			}
-		    }
-		}
-	    }
-	}
-      bl = bl->next;
-    }
-  return 1;
+  return unique_origination ();
 }
diff --git a/src/binding.h b/src/binding.h
index ace1863..bff1da3 100644
--- a/src/binding.h
+++ b/src/binding.h
@@ -30,17 +30,6 @@ typedef struct binding *Binding;	//!< pointer to binding structure
 void bindingInit (const System mysys);
 void bindingDone ();
 
-int node_count ();
-int node_number (int run, int ev);
-__inline__ int graph_nodes (const int nodes, const int run1, const int ev1,
-			    const int run2, const int ev2);
-
-int isOrderedBefore (const int run1, const int ev1, const int run2,
-		     const int ev2);
-
-void goal_graph_create ();
-
-
 int binding_print (Binding b);
 int valid_binding (Binding b);
 
diff --git a/src/claim.c b/src/claim.c
index 025df48..b80f7d9 100644
--- a/src/claim.c
+++ b/src/claim.c
@@ -57,7 +57,7 @@ indact ()
   i = indac;
   while (i > 0)
     {
-      printf ("|   ");
+      eprintf ("|   ");
       i--;
     }
 }
@@ -136,10 +136,10 @@ oki_nisynch_full (const System sys, const Termmap label_to_index)
 	{
 #ifdef OKIDEBUG
 	  indact ();
-	  printf ("Incorrectly linked label at the end,");
-	  printf ("label: ");
+	  eprintf ("Incorrectly linked label at the end,");
+	  eprintf ("label: ");
 	  termPrint (label_to_index_scan->term);
-	  printf ("\n");
+	  eprintf ("\n");
 #endif
 	  return 0;
 	}
@@ -158,13 +158,13 @@ oki_nisynch_other (const System sys, const int trace_index,
 
 #ifdef OKIDEBUG
   indact ();
-  printf ("Exploring further assuming this (claim) run is not involved.\n");
+  eprintf ("Exploring further assuming this (claim) run is not involved.\n");
   indac++;
 #endif
   result = oki_nisynch (sys, trace_index - 1, role_to_run, label_to_index);
 #ifdef OKIDEBUG
   indact ();
-  printf (">%i<\n", result);
+  eprintf (">%i<\n", result);
   indac--;
 #endif
   return result;
@@ -202,7 +202,7 @@ oki_nisynch_read (const System sys, const int trace_index,
 		termmapSet (label_to_index_buf, rd->label, trace_index);
 #ifdef OKIDEBUG
 	      indact ();
-	      printf ("Exploring because this (read) run is involved.\n");
+	      eprintf ("Exploring because this (read) run is involved.\n");
 	      indac++;
 #endif
 	      result =
@@ -210,7 +210,7 @@ oki_nisynch_read (const System sys, const int trace_index,
 			     label_to_index_buf);
 #ifdef OKIDEBUG
 	      indact ();
-	      printf (">%i<\n", result);
+	      eprintf (">%i<\n", result);
 	      indac--;
 #endif
 	      termmapDelete (label_to_index_buf);
@@ -222,7 +222,7 @@ oki_nisynch_read (const System sys, const int trace_index,
   // Apparently not involved
 #ifdef OKIDEBUG
   indact ();
-  printf ("Exploring further assuming this (read) run is not involved.\n");
+  eprintf ("Exploring further assuming this (read) run is not involved.\n");
   indac++;
 #endif
   result = oki_nisynch (sys, trace_index - 1, role_to_run, label_to_index);
@@ -252,13 +252,14 @@ oki_nisynch_send (const System sys, const int trace_index,
   // 1. Assume that this run is not yet involved 
 #ifdef OKIDEBUG
   indact ();
-  printf ("Exploring further assuming (send) run %i is not involved.\n", rid);
+  eprintf ("Exploring further assuming (send) run %i is not involved.\n",
+	   rid);
   indac++;
 #endif
   result = oki_nisynch (sys, trace_index - 1, role_to_run, label_to_index);
 #ifdef OKIDEBUG
   indact ();
-  printf (">%i<\n", result);
+  eprintf (">%i<\n", result);
   indac--;
 #endif
   if (result)
@@ -266,7 +267,7 @@ oki_nisynch_send (const System sys, const int trace_index,
 
 #ifdef OKIDEBUG
   indact ();
-  printf ("Exploring when %i is involved.\n", rid);
+  eprintf ("Exploring when %i is involved.\n", rid);
 #endif
   // 2. It is involved. Then either already used for this role, or will be now.
   rolename = sys->runs[rid].role->nameterm;
@@ -289,9 +290,9 @@ oki_nisynch_send (const System sys, const int trace_index,
 
 #ifdef OKIDEBUG
 	      indact ();
-	      printf ("Matching messages found for label ");
+	      eprintf ("Matching messages found for label ");
 	      termPrint (rd->label);
-	      printf ("\n");
+	      eprintf ("\n");
 #endif
 	      /**
 	       *@todo Optimization can be done when old_run == rid, no copy of role_to_run needs to be made.
@@ -303,10 +304,10 @@ oki_nisynch_send (const System sys, const int trace_index,
 		termmapSet (label_to_index_buf, rd->label, LABEL_GOOD);
 #ifdef OKIDEBUG
 	      indact ();
-	      printf ("In NI-Synch scan, assuming %i run is involved.\n",
-		      rid);
+	      eprintf ("In NI-Synch scan, assuming %i run is involved.\n",
+		       rid);
 	      indact ();
-	      printf
+	      eprintf
 		("Exploring further assuming this matching, which worked.\n");
 	      indac++;
 #endif
@@ -315,7 +316,7 @@ oki_nisynch_send (const System sys, const int trace_index,
 			     label_to_index_buf);
 #ifdef OKIDEBUG
 	      indact ();
-	      printf (">%i<\n", result);
+	      eprintf (">%i<\n", result);
 	      indac--;
 #endif
 	      termmapDelete (label_to_index_buf);
@@ -348,10 +349,10 @@ oki_nisynch (const System sys, const int trace_index,
 
 #ifdef OKIDEBUG
   indact ();
-  printf ("Checking event %i", trace_index);
-  printf (" = #%i : ", sys->traceRun[trace_index]);
+  eprintf ("Checking event %i", trace_index);
+  eprintf (" = #%i : ", sys->traceRun[trace_index]);
   roledefPrint (sys->traceEvent[trace_index]);
-  printf ("\n");
+  eprintf ("\n");
 #endif
 
   type = sys->traceEvent[trace_index]->type;
@@ -471,16 +472,16 @@ check_claim_niagree (const System sys, const int i)
     {
 #ifdef DEBUG
       warning ("Claim has failed!");
-      printf ("To be exact, claim label ");
+      eprintf ("To be exact, claim label ");
       termPrint (cl->label);
-      printf (" with prec set ");
+      eprintf (" with prec set ");
       termlistPrint (cl->prec);
-      printf ("\n");
-      printf ("i: %i\nf: ", i);
+      eprintf ("\n");
+      eprintf ("i: %i\nf: ", i);
       termmapPrint (f);
-      printf ("\ng: ");
+      eprintf ("\ng: ");
       termmapPrint (g);
-      printf ("\n");
+      eprintf ("\n");
 #endif
 
     }
diff --git a/src/compiler.c b/src/compiler.c
index 571ce11..7a88bec 100644
--- a/src/compiler.c
+++ b/src/compiler.c
@@ -13,6 +13,7 @@
 #include "compiler.h"
 #include "switches.h"
 #include "specialterm.h"
+#include "warshall.h"
 #include "hidelevel.h"
 
 /*
@@ -1304,8 +1305,9 @@ void
 compute_prec_sets (const System sys)
 {
   Term *eventlabels;		// array: maps events to labels
-  int *prec;			// array: maps event*event to precedence
+  unsigned int *prec;		// array: maps event*event to precedence
   int size;			// temp constant: rolecount * roleeventmax
+  int rowsize;
   int r1, r2, ev1, ev2;		// some counters
   int i, j;
   Claimlist cl;
@@ -1316,11 +1318,6 @@ compute_prec_sets (const System sys)
     return r * sys->roleeventmax + lev;
   }
 
-  // Assist: compute matrix index from i*i
-  int index2 (int i1, int i2)
-  {
-    return i1 * size + i2;
-  }
   // Assist: yield roledef from r, lev
   Roledef roledef_re (int r, int lev)
   {
@@ -1382,7 +1379,8 @@ compute_prec_sets (const System sys)
 		while (ev2 < sys->roleeventmax)
 		  {
 		    eprintf ("%i ",
-			     prec[index2 (index (r2, ev2), index (r1, ev1))]);
+			     BIT (prec + rowsize * index (r2, ev2),
+				  index (r1, ev1)));
 		    ev2++;
 		  }
 		eprintf (" ");
@@ -1403,21 +1401,9 @@ compute_prec_sets (const System sys)
   //eprintf ("Rolecount: %i\n", sys->rolecount);
   //eprintf ("Maxevent : %i\n", sys->roleeventmax);
   size = sys->rolecount * sys->roleeventmax;
+  rowsize = WORDSIZE (size);
   eventlabels = memAlloc (size * sizeof (Term));
-  prec = memAlloc (size * size * sizeof (int));
-  // Clear tables
-  i = 0;
-  while (i < size)
-    {
-      eventlabels[i] = NULL;
-      j = 0;
-      while (j < size)
-	{
-	  prec[index2 (i, j)] = 0;
-	  j++;
-	}
-      i++;
-    }
+  prec = (unsigned int *) CALLOC (1, rowsize * size * sizeof (unsigned int));
   // Assign labels
   r1 = 0;
   while (r1 < sys->rolecount)
@@ -1444,7 +1430,7 @@ compute_prec_sets (const System sys)
       ev1 = 0;
       while (ev1 < (sys->roleeventmax - 1))
 	{
-	  prec[index2 (index (r1, ev1), index (r1, ev1 + 1))] = 1;
+	  SETBIT (prec + rowsize * index (r1, ev1), index (r1, ev1 + 1));
 	  ev1++;
 	}
       r1++;
@@ -1473,7 +1459,8 @@ compute_prec_sets (const System sys)
 		      if (rd2 != NULL && rd2->type == READ
 			  && isTermEqual (rd1->label, rd2->label))
 			{
-			  prec[index2 (index (r1, ev1), index (r2, ev2))] = 1;
+			  SETBIT (prec + rowsize * index (r1, ev1),
+				  index (r2, ev2));
 			}
 		      ev2++;
 		    }
@@ -1484,14 +1471,18 @@ compute_prec_sets (const System sys)
 	}
       r1++;
     }
-  //[x] show_matrix ();
 
   /*
    * Compute transitive closure (Warshall).
    */
-  warshall (prec, size);
+  transitive_closure (prec, size);
 
-  // [x] show_matrix ();
+#ifdef DEBUG
+  if (DEBUGL (5))
+    {
+      show_matrix ();
+    }
+#endif
 
   /*
    * Last phase: Process all individual claims
@@ -1550,7 +1541,7 @@ compute_prec_sets (const System sys)
 	  rd = roledef_re (r2, ev2);
 	  while (rd != NULL)
 	    {
-	      if (prec[index2 (index (r2, ev2), claim_index)] == 1)
+	      if (BIT (prec + rowsize * index (r2, ev2), claim_index))
 		{
 		  // This event precedes the claim
 
@@ -1620,8 +1611,9 @@ compute_prec_sets (const System sys)
 		  while (ev_scan < sys->roleeventmax)
 		    {
 		      // if this event preceds the claim, replace the label term
-		      if (prec[index2 (index (r_scan, ev_scan), claim_index)]
-			  == 1)
+		      if (BIT
+			  (prec + rowsize * index (r_scan, ev_scan),
+			   claim_index))
 			{
 			  Roledef rd;
 
@@ -1699,7 +1691,7 @@ compute_prec_sets (const System sys)
    * Cleanup
    */
   memFree (eventlabels, size * sizeof (Term));
-  memFree (prec, size * size * sizeof (int));
+  FREE (prec);
 
 #ifdef DEBUG
   if (DEBUGL (2))
diff --git a/src/constraint.c b/src/constraint.c
index b745c1d..ec407fe 100644
--- a/src/constraint.c
+++ b/src/constraint.c
@@ -173,7 +173,7 @@ constraintlistDelete (Constraintlist cl)
   if (cl->prev != NULL)
     {
       /* TODO maybe this should cause a warning? */
-      printf ("WARNING: clDelete with non-empty prev\n");
+      eprintf ("WARNING: clDelete with non-empty prev\n");
       cl->prev->next = NULL;
     }
   while (cl != NULL)
@@ -198,7 +198,7 @@ constraintlistDestroy (Constraintlist cl)
   if (cl->prev != NULL)
     {
       /* TODO maybe this should cause a warning? */
-      printf ("WARNING: clDestroy with non-empty prev\n");
+      eprintf ("WARNING: clDestroy with non-empty prev\n");
       cl->prev = NULL;
     }
   while (cl != NULL)
@@ -248,14 +248,14 @@ void
 constraintPrint (Constraint co)
 {
   indent ();
-  printf ("Constraint ");
+  eprintf ("Constraint ");
   if (co == NULL)
     {
-      printf ("[empty]\n");
+      eprintf ("[empty]\n");
       return;
     }
   termPrint (co->term);
-  printf (" :\n");
+  eprintf (" :\n");
   knowledgePrint (co->know);
 }
 
@@ -265,7 +265,7 @@ constraintlistPrint (Constraintlist cl)
   if (cl == NULL)
     {
       indent ();
-      printf ("[empty constraintlist]\n");
+      eprintf ("[empty constraintlist]\n");
       return;
     }
   while (cl != NULL)
diff --git a/src/depend.c b/src/depend.c
new file mode 100644
index 0000000..3878784
--- /dev/null
+++ b/src/depend.c
@@ -0,0 +1,491 @@
+/**
+ * @file depend.c
+ * \brief interface for graph code from the viewpoint of events.
+ *
+ */
+
+#include "depend.h"
+#include "term.h"
+#include "system.h"
+#include "binding.h"
+#include "warshall.h"
+#include "debug.h"
+#include "error.h"
+
+/*
+ * Generic structures
+ * ---------------------------------------------------------------
+ */
+//! Event dependency structure
+struct depeventgraph
+{
+  //! Flag denoting what it was made for (newrun|newbinding)
+  int fornewrun;
+  //! Number of runs;
+  int runs;
+  //! System where it derives from
+  System sys;
+  //! Number of nodes
+  int n;
+  //! Rowsize
+  int rowsize;
+  //! Graph structure
+  unsigned int *G;
+  //! Zombie dummy push
+  int zombie;
+  //! Previous graph
+  struct depeventgraph *prev;
+};
+
+//! Pointer shorthard
+typedef struct depeventgraph *Depeventgraph;
+
+/*
+ * Globals
+ * ---------------------------------------------------------------
+ */
+
+Depeventgraph currentdepgraph;
+
+/*
+ * Default code
+ * ---------------------------------------------------------------
+ */
+
+//! Default init
+void
+dependInit (const System sys)
+{
+  currentdepgraph = NULL;
+}
+
+//! Pring
+void
+dependPrint ()
+{
+  Depeventgraph dg;
+
+  eprintf ("Printing DependEvent stack, top first.\n\n");
+  for (dg = currentdepgraph; dg != NULL; dg = dg->prev)
+    {
+      eprintf ("%i nodes, %i rowsize, %i zombies, %i runs: created for new ",
+	       dg->n, dg->rowsize, dg->zombie, dg->runs);
+      if (dg->fornewrun)
+	{
+	  eprintf ("run");
+	}
+      else
+	{
+	  eprintf ("binding");
+	}
+      eprintf ("\n");
+    }
+  eprintf ("\n");
+#ifdef DEBUG
+  {
+    int n1;
+    int r1;
+    int o1;
+
+    r1 = 0;
+    o1 = 0;
+    eprintf ("Printing dependency graph.\n");
+    for (n1 = 0; n1 < nodeCount (); n1++)
+      {
+	int n2;
+	int r2;
+	int o2;
+
+	if ((n1 - o1) >= currentdepgraph->sys->runs[r1].rolelength)
+	  {
+	    o1 += currentdepgraph->sys->runs[r1].rolelength;
+	    r1++;
+	    eprintf ("\n");
+	  }
+	r2 = 0;
+	o2 = 0;
+	eprintf ("%5i : ", n1);
+	for (n2 = 0; n2 < nodeCount (); n2++)
+	  {
+	    if ((n2 - o2) >= currentdepgraph->sys->runs[r2].rolelength)
+	      {
+		o2 += currentdepgraph->sys->runs[r2].rolelength;
+		r2++;
+		eprintf (" ");
+	      }
+	    eprintf ("%i", getNode (n1, n2));
+	  }
+	eprintf ("\n");
+
+      }
+    eprintf ("\n");
+  }
+#endif
+}
+
+//! Default cleanup
+void
+dependDone (const System sys)
+{
+  if (currentdepgraph != NULL)
+    {
+      globalError++;
+      eprintf ("\n\n");
+      dependPrint ();
+      globalError--;
+      error
+	("depgraph stack (depend.c) not empty at dependDone, bad iteration?");
+    }
+}
+
+/*
+ * Libs
+ * ---------------------------------------------------------------
+ */
+
+//! Convert from event to node in a graph (given that sys is set)
+int
+eventtonode (const Depeventgraph dgx, const int r, const int e)
+{
+  int i;
+  int n;
+
+  n = 0;
+  for (i = 0; i < dgx->sys->maxruns; i++)
+    {
+      if (i == r)
+	{
+	  // this run
+#ifdef DEBUG
+	  if (dgx->sys->runs[i].rolelength <= e)
+	    {
+	      error ("Bad offset for eventtonode");
+	    }
+#endif
+	  return (n + e);
+	}
+      else
+	{
+	  // not this run, add offset
+	  n += dgx->sys->runs[i].rolelength;
+	}
+    }
+  error ("Bad offset (run number too high?) for eventtonode");
+  return 0;
+}
+
+//! Return the number of nodes in a graph
+int
+countnodes (const Depeventgraph dgx)
+{
+  int i;
+  int nodes;
+
+  nodes = 0;
+  for (i = 0; i < dgx->sys->maxruns; i++)
+    {
+      nodes += dgx->sys->runs[i].rolelength;
+    }
+  return nodes;
+}
+
+//! Graph size given the number of nodes
+unsigned int
+getGraphSize (const Depeventgraph dgx)
+{
+  return (dgx->n * dgx->rowsize);
+}
+
+//! Create graph from sys
+Depeventgraph
+dependCreate (const System sys)
+{
+  Depeventgraph dgnew;
+
+  dgnew = (Depeventgraph) MALLOC (sizeof (struct depeventgraph));
+  dgnew->sys = sys;
+  dgnew->fornewrun = true;
+  dgnew->runs = sys->maxruns;
+  dgnew->zombie = 0;
+  dgnew->prev = NULL;
+  dgnew->n = countnodes (dgnew);	// count nodes works on ->sys
+  dgnew->rowsize = WORDSIZE (dgnew->n);
+  dgnew->G = (unsigned int *) CALLOC (1, getGraphSize (dgnew) * sizeof (unsigned int));	// works on ->n and ->rowsize
+
+  return dgnew;
+}
+
+//! Copy graph from current one
+Depeventgraph
+dependCopy (const Depeventgraph dgold)
+{
+  Depeventgraph dgnew;
+
+  // Copy old to new
+  dgnew = (Depeventgraph) MALLOC (sizeof (struct depeventgraph));
+  memcpy ((void *) dgnew, (void *) dgold,
+	  (size_t) sizeof (struct depeventgraph));
+
+  // New copy
+  dgnew->fornewrun = false;
+  dgnew->zombie = 0;
+
+  // copy inner graph
+  dgnew->G =
+    (unsigned int *) MALLOC (getGraphSize (dgold) * sizeof (unsigned int));
+  memcpy ((void *) dgnew->G, (void *) dgold->G,
+	  getGraphSize (dgold) * sizeof (unsigned int));
+
+  return dgnew;
+}
+
+//! Destroy graph
+void
+dependDestroy (const Depeventgraph dgold)
+{
+  FREE (dgold->G);
+  FREE (dgold);
+}
+
+//! push graph to stack (generic)
+void
+dependPushGeneric (Depeventgraph dgnew)
+{
+  dgnew->prev = currentdepgraph;
+  currentdepgraph = dgnew;
+}
+
+//! restore graph from stack (generic)
+void
+dependPopGeneric (void)
+{
+  Depeventgraph dgprev;
+
+  dgprev = currentdepgraph->prev;
+  dependDestroy (currentdepgraph);
+  currentdepgraph = dgprev;
+}
+
+//! Construct graph dependencies from sys
+/**
+ * uses currentdepgraph->sys
+ */
+void
+dependFromSys (void)
+{
+  int r;
+  List bl;
+
+  // There are two types of orderings.
+  // 1. Role orderings (within runs)
+  for (r = 0; r < currentdepgraph->sys->maxruns; r++)
+    {
+      int e;
+
+      for (e = 1; e < currentdepgraph->sys->runs[r].rolelength; e++)
+	{
+	  setDependEvent (r, e - 1, r, e);
+	}
+    }
+
+  // 2. Binding orderings
+  // We implicitly assume these cause no cycles (by construction this is
+  // correct)
+  for (bl = currentdepgraph->sys->bindings; bl != NULL; bl = bl->next)
+    {
+      Binding b;
+
+      b = (Binding) bl->data;
+      if (valid_binding (b))
+	{
+	  int r1, e1, r2, e2;
+
+	  r1 = b->run_from;
+	  e1 = b->ev_from;
+	  r2 = b->run_to;
+	  e2 = b->ev_to;
+	  if (!((r1 == r2) && (e1 == e2)))
+	    {
+	      // Not a self-binding
+	      setDependEvent (r1, e1, r2, e2);
+	    }
+	}
+    }
+}
+
+//! Detect whether the graph has a cycle. If so, a node can get to itself (through the cycle)
+int
+hasCycle ()
+{
+  int n;
+
+  for (n = 0; n < currentdepgraph->n; n++)
+    {
+      if (getNode (n, n))
+	{
+	  return true;
+	}
+
+    }
+  return false;
+}
+
+/*
+ * Public Code
+ * ---------------------------------------------------------------
+ */
+
+//! get node
+int
+getNode (const int n1, const int n2)
+{
+  return BIT (currentdepgraph->G + currentdepgraph->rowsize * n1, n2);
+}
+
+//! set node
+void
+setNode (const int n1, const int n2)
+{
+  SETBIT (currentdepgraph->G + currentdepgraph->rowsize * n1, n2);
+}
+
+//! Count nodes
+int
+nodeCount (void)
+{
+  return countnodes (currentdepgraph);
+}
+
+/*
+ * Simple setting
+ */
+void
+setDependEvent (const int r1, const int e1, const int r2, const int e2)
+{
+  int n1, n2;
+
+  n1 = eventtonode (currentdepgraph, r1, e1);
+  n2 = eventtonode (currentdepgraph, r2, e2);
+  setNode (n1, n2);
+}
+
+/*
+ * Simple testing
+ */
+int
+isDependEvent (const int r1, const int e1, const int r2, const int e2)
+{
+  int n1, n2;
+
+  n1 = eventtonode (currentdepgraph, r1, e1);
+  n2 = eventtonode (currentdepgraph, r2, e2);
+  return getNode (n1, n2);
+}
+
+//! create new graph after adding runs or events (new number of nodes)
+void
+dependPushRun (const System sys)
+{
+  dependPushGeneric (dependCreate (sys));
+  dependFromSys ();
+}
+
+//! restore graph to state after previous run add
+void
+dependPopRun (void)
+{
+  if (!currentdepgraph->fornewrun)
+    {
+      globalError++;
+      dependPrint ();
+      globalError--;
+      error ("Trying to pop graph created for new binding.");
+    }
+  dependPopGeneric ();
+}
+
+//! create new graph by adding event bindings
+/*
+ * The push code returns true or false: if false, the operation fails because
+ * it there is now a cycle in the graph, and there is no need to pop the
+ * result.
+ */
+int
+dependPushEvent (const int r1, const int e1, const int r2, const int e2)
+{
+  if (isDependEvent (r2, e2, r1, e1))
+    {
+      // Adding would imply a cycle, so we won't do that.
+#ifdef DEBUG
+      if (DEBUGL (3))
+	{
+	  eprintf ("Cycle detected for binding %i,%i -> %i,%i.\n", r1, e1, r2,
+		   e2);
+	}
+      if (DEBUGL (5))
+	{
+	  dependPrint ();
+	}
+#endif
+      return false;
+    }
+  else
+    {
+      // No immediate cycle: new graph, return true TODO disabled
+      if ((1 == 0) && ((r1 == r2) && (e1 == e2))
+	  || isDependEvent (r1, e1, r2, e2))
+	{
+	  // if n->n or the binding already existed, no changes
+	  // no change: add zombie
+	  currentdepgraph->zombie += 1;
+	}
+      else
+	{
+	  // change: make new graph copy of the old one
+	  dependPushGeneric (dependCopy (currentdepgraph));
+	  // add new binding
+	  setDependEvent (r1, e1, r2, e2);
+	  // recompute closure
+	  transitive_closure (currentdepgraph->G, currentdepgraph->n);
+	  // check for cycles
+	  if (hasCycle ())
+	    {
+	      //warning ("Cycle slipped undetected by the reverse check.");
+	      // Closure introduced cycle, undo it
+	      dependPopEvent ();
+	      return false;
+	    }
+	}
+      return true;
+    }
+}
+
+//! restore graph to state before previous binding add
+void
+dependPopEvent (void)
+{
+  if (currentdepgraph->fornewrun)
+    {
+      globalError++;
+      dependPrint ();
+      globalError--;
+      error ("Trying to pop graph created for new run.");
+    }
+  if (currentdepgraph->zombie > 0)
+    {
+      // zombie pushed
+      currentdepgraph->zombie -= 1;
+    }
+  else
+    {
+      // real graph
+      dependPopGeneric ();
+    }
+}
+
+//! Current event to node
+int
+eventNode (const int r, const int e)
+{
+  return eventtonode (currentdepgraph, r, e);
+}
diff --git a/src/depend.h b/src/depend.h
new file mode 100644
index 0000000..4204631
--- /dev/null
+++ b/src/depend.h
@@ -0,0 +1,42 @@
+#ifndef DEPEND
+#define DEPEND
+
+#include "system.h"
+
+/*
+ * The code here mainly involves an interface for creating graphs etc., but
+ * most of it is implicit: we just add dependencies/runs and undo them again
+ * later.
+ */
+
+void dependInit (const System sys);
+void dependPrint ();
+void dependDone (const System sys);
+
+/*
+ * The push code returns true or false: if false, the operation fails because
+ * it there is now a cycle in the graph, and there is no need to pop the
+ * result.
+ */
+void dependPushRun (const System sys);
+void dependPopRun ();
+int dependPushEvent (const int r1, const int e1, const int r2, const int e2);
+void dependPopEvent ();
+
+/*
+ * Test/set
+ */
+
+int getNode (const int n1, const int n2);
+void setNode (const int n1, const int n2);
+int isDependEvent (const int r1, const int e1, const int r2, const int e2);
+void setDependEvent (const int r1, const int e1, const int r2, const int e2);
+
+/*
+ * Outside helpers
+ */
+int hasCycle ();
+int eventNode (const int r, const int e);
+int nodeCount (void);
+
+#endif
diff --git a/src/dotout.c b/src/dotout.c
index 764041d..7c59772 100644
--- a/src/dotout.c
+++ b/src/dotout.c
@@ -2,10 +2,8 @@
 #include "switches.h"
 #include "memory.h"
 #include "arachne.h"
-
-extern int *graph;
-extern int nodes;
-extern int graph_uordblks;
+#include "depend.h"
+#include <limits.h>
 
 extern Protocol INTRUDER;	// Pointers, to be set by the Init of arachne.c
 extern Role I_M;		// Same here.
@@ -17,6 +15,70 @@ extern Role I_RRSD;
 #define isBound(rd)	(rd->bound)
 #define length		step
 
+
+//! Determine ranks for all nodes
+/**
+ * Some crude algorithm I sketched on the blackboard.
+ */
+int
+graph_ranks (int *ranks, int nodes)
+{
+  int i;
+  int todo;
+  int rank;
+
+#ifdef DEBUG
+  if (hasCycle ())
+    {
+      error ("Graph ranks tried, but a cycle exists!");
+    }
+#endif
+
+  i = 0;
+  while (i < nodes)
+    {
+      ranks[i] = INT_MAX;
+      i++;
+    }
+
+  todo = nodes;
+  rank = 0;
+  while (todo > 0)
+    {
+      // There are still unassigned nodes
+      int n;
+
+      n = 0;
+      while (n < nodes)
+	{
+	  if (ranks[n] == INT_MAX)
+	    {
+	      // Does this node have incoming stuff from stuff with equal rank or higher?
+	      int refn;
+
+	      refn = 0;
+	      while (refn < nodes)
+		{
+		  if (ranks[refn] >= rank && getNode (refn, n))
+		    refn = nodes + 1;
+		  else
+		    refn++;
+		}
+	      if (refn == nodes)
+		{
+		  ranks[n] = rank;
+		  todo--;
+		}
+	    }
+	  n++;
+	}
+      rank++;
+    }
+  return rank;
+}
+
+
+
 //! Iterate over all events that have an incoming arrow to the current one (forgetting the intruder for a moment)
 void
 iterate_incoming_arrows (const System sys, void (*func) (), const int run,
@@ -42,7 +104,7 @@ iterate_incoming_arrows (const System sys, void (*func) (), const int run,
 	  while (found == 0 && ev2 > 0)
 	    {
 	      ev2--;
-	      if (graph[graph_nodes (nodes, run2, ev2, run, ev)] != 0)
+	      if (isDependEvent (run2, ev2, run, ev))
 		{
 		  found = 1;
 		}
@@ -72,12 +134,8 @@ iterate_incoming_arrows (const System sys, void (*func) (), const int run,
 		      ev3 = 0;
 		      while (other_route == 0 && ev3 < sys->runs[run3].length)
 			{
-			  if (graph
-			      [graph_nodes
-			       (nodes, run2, ev2, run3, ev3)] != 0
-			      &&
-			      graph[graph_nodes
-				    (nodes, run3, ev3, run, ev)] != 0)
+			  if (isDependEvent (run2, ev2, run3, ev3)
+			      && isDependEvent (run3, ev3, run, ev))
 			    {
 			      // other route found
 			      other_route = 1;
@@ -123,7 +181,7 @@ iterate_outgoing_arrows (const System sys, void (*func) (), const int run,
 	  ev2 = 0;
 	  while (found == 0 && ev2 < sys->runs[run2].length)
 	    {
-	      if (graph[graph_nodes (nodes, run, ev, run2, ev2)] != 0)
+	      if (isDependEvent (run, ev, run2, ev2))
 		{
 		  found = 1;
 		}
@@ -157,12 +215,8 @@ iterate_outgoing_arrows (const System sys, void (*func) (), const int run,
 		      ev3 = 0;
 		      while (other_route == 0 && ev3 < sys->runs[run3].length)
 			{
-			  if (graph
-			      [graph_nodes
-			       (nodes, run, ev, run3, ev3)] != 0
-			      &&
-			      graph[graph_nodes
-				    (nodes, run3, ev3, run2, ev2)] != 0)
+			  if (isDependEvent (run, ev, run3, ev3)
+			      && isDependEvent (run3, ev3, run2, ev2))
 			    {
 			      // other route found
 			      other_route = 1;
@@ -196,6 +250,7 @@ dotSemiState (const System sys)
   int *ranks;
   int maxrank;
   int from_intruder_count;
+  int nodes;
 
   void node (const int run, const int index)
   {
@@ -231,15 +286,10 @@ dotSemiState (const System sys)
   from_intruder_count = 0;	// number of terms that can come from the initial knowledge
 
   // Needed for the bindings later on: create graph
-  goal_graph_create ();		// create graph
-  if (warshall (graph, nodes) == 0)	// determine closure
-    {
-      eprintf
-	("// This graph was not completely closed transitively because it contains a cycle!\n");
-    }
 
+  nodes = nodeCount ();
   ranks = memAlloc (nodes * sizeof (int));
-  maxrank = graph_ranks (graph, ranks, nodes);	// determine ranks
+  maxrank = graph_ranks (ranks, nodes);	// determine ranks
 
 #ifdef DEBUG
   // For debugging purposes, we also display an ASCII version of some stuff in the comments
@@ -272,7 +322,7 @@ dotSemiState (const System sys)
 		ev2 = 0;
 		while (ev2 < sys->runs[run2].length)
 		  {
-		    if (graph[graph_nodes (nodes, run2, ev2, run, ev)] != 0)
+		    if (isDependEvent (run2, ev2, run, ev))
 		      {
 			if (notfirstev)
 			  eprintf (",");
@@ -518,6 +568,43 @@ dotSemiState (const System sys)
 	("\tintruder [label=\"Initial intruder knowledge\", color=red];\n");
     }
 
+  // For debugging we might add more stuff: full dependencies
+#ifdef DEBUG
+  {
+    int r1;
+
+    for (r1 = 0; r1 < sys->maxruns; r1++)
+      {
+	if (sys->runs[r1].protocol != INTRUDER)
+	  {
+	    int e1;
+
+	    for (e1 = 0; e1 < sys->runs[r1].step; e1++)
+	      {
+		int r2;
+
+		for (r2 = 0; r2 < sys->maxruns; r2++)
+		  {
+		    if (sys->runs[r2].protocol != INTRUDER)
+		      {
+			int e2;
+
+			for (e2 = 0; e2 < sys->runs[r2].step; e2++)
+			  {
+			    if (isDependEvent (r1, e1, r2, e2))
+			      {
+				eprintf ("\tr%ii%i -> r%ii%i [color=grey];\n",
+					 r1, e1, r2, e2);
+			      }
+			  }
+		      }
+		  }
+	      }
+	  }
+      }
+  }
+#endif
+
   // Fourth, all ranking info
   {
     int myrank;
@@ -555,7 +642,7 @@ dotSemiState (const System sys)
 		ev = 0;
 		while (ev < sys->runs[run].step)
 		  {
-		    if (myrank == ranks[node_number (run, ev)])
+		    if (myrank == ranks[eventNode (run, ev)])
 		      {
 			if (count == 0)
 			  eprintf ("\t{ rank = same; ");
@@ -573,6 +660,14 @@ dotSemiState (const System sys)
       }
   }
 
+#ifdef DEBUG
+  // Debug: print dependencies
+  if (DEBUGL (3))
+    {
+      dependPrint ();
+    }
+#endif
+
   // clean memory
   memFree (ranks, nodes * sizeof (int));	// ranks
 
diff --git a/src/heuristic.c b/src/heuristic.c
index b4eb842..e0cd43c 100644
--- a/src/heuristic.c
+++ b/src/heuristic.c
@@ -20,12 +20,12 @@ is_goal_selectable (const Binding b)
 {
   if (b != NULL)
     {
-      if (!b->blocked && !b->done)
+      if ((!b->blocked) && (!b->done))
 	{
-	  return 1;
+	  return true;
 	}
     }
-  return 0;
+  return false;
 }
 
 //! Count selectable goals
diff --git a/src/hidelevel.c b/src/hidelevel.c
index fd7950b..5541f86 100644
--- a/src/hidelevel.c
+++ b/src/hidelevel.c
@@ -80,9 +80,15 @@ hidelevelCompute (const System sys)
 
   sys->hidden = NULL;
   tl = sys->globalconstants;
-  eprintf ("Global constants: ");
-  termlistPrint (tl);
-  eprintf ("\n");
+
+#ifdef DEBUG
+  if (DEBUGL (4))
+    {
+      eprintf ("Global constants: ");
+      termlistPrint (tl);
+      eprintf ("\n");
+    }
+#endif
 
   while (tl != NULL)
     {
@@ -113,9 +119,12 @@ hidelevelCompute (const System sys)
 	  sys->hidden = ht;
 
 #ifdef DEBUG
-	  eprintf ("Added possibly interesting term: ");
-	  termPrint (tl->term);
-	  eprintf ("; know %i, prot %i\n", l1, l2);
+	  if (DEBUGL (5))
+	    {
+	      eprintf ("Added possibly interesting term: ");
+	      termPrint (tl->term);
+	      eprintf ("; know %i, prot %i\n", l1, l2);
+	    }
 #endif
 	}
 
diff --git a/src/latex.c b/src/latex.c
index fbada43..7cb9ce6 100644
--- a/src/latex.c
+++ b/src/latex.c
@@ -62,20 +62,20 @@ latexInit (const System sys, int argc, char **argv)
 {
   int i;
 
-  printf ("%%\n");
-  printf ("%% LaTeX output generated by %s\n", progname);
-  printf ("%% Input:\n");
+  eprintf ("%%\n");
+  eprintf ("%% LaTeX output generated by %s\n", progname);
+  eprintf ("%% Input:\n");
 
   /* print command line */
-  printf ("%% $");
+  eprintf ("%% $");
   for (i = 0; i < argc; i++)
-    printf (" %s", argv[i]);
-  printf ("\n");
+    eprintf (" %s", argv[i]);
+  eprintf ("\n");
 
-  printf ("%%\n");
+  eprintf ("%%\n");
 
   /* comment macro (used for debugging) */
-  printf ("\\newcommand{\\comment}[1]{}\n");
+  eprintf ("\\newcommand{\\comment}[1]{}\n");
 }
 
 //! Close up any LaTeX output.
@@ -102,7 +102,7 @@ latexTermPrint (Term term, Termlist highlight)
 {
   if (term == NULL)
     {
-      printf ("Empty term");
+      eprintf ("Empty term");
       return;
     }
 #ifdef DEBUG
@@ -116,27 +116,27 @@ latexTermPrint (Term term, Termlist highlight)
   if (realTermLeaf (term))
     {
       if (inTermlist (highlight, term))
-	printf ("\\mathbf{");
+	eprintf ("\\mathbf{");
       symbolPrint (TermSymb (term));
       if (realTermVariable (term))
-	printf ("V");
+	eprintf ("V");
       if (TermRunid (term) >= 0)
 	{
-	  printf ("\\sharp%i", TermRunid (term));
+	  eprintf ("\\sharp%i", TermRunid (term));
 	}
       if (term->subst != NULL)
 	{
-	  printf ("\\rightarrow");
+	  eprintf ("\\rightarrow");
 	  latexTermPrint (term->subst, highlight);
 	}
       if (inTermlist (highlight, term))
-	printf ("}");
+	eprintf ("}");
     }
   if (realTermTuple (term))
     {
-      printf ("(");
+      eprintf ("(");
       latexTermTuplePrint (term, highlight);
-      printf (")");
+      eprintf (")");
       return;
     }
   if (realTermEncrypt (term))
@@ -146,18 +146,18 @@ latexTermPrint (Term term, Termlist highlight)
 	{
 	  /* function application */
 	  latexTermPrint (TermKey (term), highlight);
-	  printf ("(");
+	  eprintf ("(");
 	  latexTermTuplePrint (TermOp (term), highlight);
-	  printf (")");
+	  eprintf (")");
 	}
       else
 	{
 	  /* normal encryption */
-	  printf ("\\{");
+	  eprintf ("\\{");
 	  latexTermTuplePrint (TermOp (term), highlight);
-	  printf ("\\}_{");
+	  eprintf ("\\}_{");
 	  latexTermPrint (TermKey (term), highlight);
-	  printf ("}");
+	  eprintf ("}");
 	}
     }
 }
@@ -173,7 +173,7 @@ latexTermTuplePrint (Term term, Termlist hl)
 {
   if (term == NULL)
     {
-      printf ("Empty term");
+      eprintf ("Empty term");
       return;
     }
   term = deVar (term);
@@ -181,7 +181,7 @@ latexTermTuplePrint (Term term, Termlist hl)
     {
       // To remove any brackets, change this into latexTermTuplePrint.
       latexTermPrint (TermOp1 (term), hl);
-      printf (",");
+      eprintf (",");
       term = deVar (TermOp2 (term));
     }
   latexTermPrint (term, hl);
@@ -201,7 +201,7 @@ latexTermlistPrint (Termlist tl, Termlist highlight)
 {
   if (tl == NULL)
     {
-      printf ("\\emptyset");
+      eprintf ("\\emptyset");
       return;
     }
   while (tl != NULL)
@@ -209,7 +209,7 @@ latexTermlistPrint (Termlist tl, Termlist highlight)
       latexTermPrint (tl->term, highlight);
       tl = tl->next;
       if (tl != NULL)
-	printf (", ");
+	eprintf (", ");
     }
 }
 
@@ -233,11 +233,11 @@ void
 latexMSCStart (Termlist protocolnames)
 {
   if (landscape)
-    printf ("\\begin{landscape}\n");
+    eprintf ("\\begin{landscape}\n");
 
-  printf ("\\begin{msc}{attack on $");
+  eprintf ("\\begin{msc}{attack on $");
   termlistPrint (protocolnames);
-  printf ("$}\n");
+  eprintf ("$}\n");
 }
 
 //! Close drawing MSC
@@ -245,10 +245,10 @@ latexMSCStart (Termlist protocolnames)
 void
 latexMSCEnd ()
 {
-  printf ("\\end{msc}\n");
+  eprintf ("\\end{msc}\n");
 
   if (landscape)
-    printf ("\\end{landscape}\n");
+    eprintf ("\\end{landscape}\n");
 
 }
 
@@ -272,43 +272,43 @@ latexDeclInst (const System sys, int run)
   myRole = sys->runs[run].role->nameterm;
   if (pass == 1)
     {
-      printf ("\\maxlength{\\maxmscinst}{");
+      eprintf ("\\maxlength{\\maxmscinst}{");
     }
   else
     {
-      printf ("\\declinst{run%i}{", run);
+      eprintf ("\\declinst{run%i}{", run);
     }
 
   /* display above assumptions */
   roles = sys->runs[run].protocol->rolenames;
   if (pass == 2)
     {
-      printf ("assumes $");
+      eprintf ("assumes $");
       first = 1;
       while (roles != NULL)
 	{
 	  if (!isTermEqual (myRole, roles->term))
 	    {
 	      if (!first)
-		printf (", ");
+		eprintf (", ");
 	      else
 		first = 0;
 	      termPrint (agentOfRunRole (sys, run, roles->term));
-	      printf (": ");
+	      eprintf (": ");
 	      termPrint (roles->term);
 	    }
 	  roles = roles->next;
 	}
-      printf ("$}{");
+      eprintf ("$}{");
     }
 
   /* display agent and role */
-  printf ("$\\mathbf{");
+  eprintf ("$\\mathbf{");
   termPrint (myAgent);
-  printf ("}: ");
+  eprintf ("}: ");
   termPrint (myRole);
 
-  printf ("$}\n");
+  eprintf ("$}\n");
 
   /* cleanup */
   termDelete (myAgent);
@@ -332,9 +332,9 @@ latexEventSpace (int amount)
       return;
     }
 
-  //printf("%% number of newlines: %d\n",amount);
+  //eprintf("%% number of newlines: %d\n",amount);
   for (i = 0; i < EVENTSPACE * amount; i++)
-    printf ("\\nextlevel\n");
+    eprintf ("\\nextlevel\n");
 }
 
 //! MSC message print.
@@ -371,36 +371,36 @@ latexMessagePrint (struct tracebuf *tb, int from, int to)
   if (from == -1 && to != -1)
     {
       /* message from intruder into system */
-      printf ("\\mess{$");
+      eprintf ("\\mess{$");
       termPrint (readTerm);
-      printf ("$}{eve}{run%d}\n", tb->run[to]);
+      eprintf ("$}{eve}{run%d}\n", tb->run[to]);
     }
   else if (from != -1 && to == -1)
     {
       /* message from system to intruder */
-      printf ("\\mess{$");
+      eprintf ("\\mess{$");
       termPrint (sendTerm);
-      printf ("$}{run%d}{eve}\n", tb->run[from]);
+      eprintf ("$}{run%d}{eve}\n", tb->run[from]);
     }
   else if (from != -1 && to != -1)
     {
       /* message from one agent to another, possibly transformed */
 
-      printf ("\\mess{$");
+      eprintf ("\\mess{$");
 
       termPrint (sendTerm);
 
       if (!isTermEqual (sendTerm, readTerm))
 	{
-	  printf ("\\rightarrow");
+	  eprintf ("\\rightarrow");
 	  termPrint (readTerm);
 	}
 
-      printf ("$}{run%d", tb->run[from]);
-      printf ("}{run%d}[%d]", tb->run[to],
-	      EVENTSPACE * (tinfo[to].position - tinfo[from].position));
+      eprintf ("$}{run%d", tb->run[from]);
+      eprintf ("}{run%d}[%d]", tb->run[to],
+	       EVENTSPACE * (tinfo[to].position - tinfo[from].position));
 
-      printf ("\n");
+      eprintf ("\n");
     }
 }
 
@@ -438,34 +438,34 @@ latexMessagePrintHighlight (struct tracebuf *tb, int from, int to,
   if (from == -1 && to != -1)
     {
       /* TODO redundant */
-      printf ("\\found{$");
+      eprintf ("\\found{$");
       latexTermPrint (readTerm, highlight);
-      printf ("$}{}{run%d}\n", tb->run[to]);
+      eprintf ("$}{}{run%d}\n", tb->run[to]);
     }
   else if (from != -1 && to == -1)
     {
-      printf ("\\mess{$");
+      eprintf ("\\mess{$");
       latexTermPrint (sendTerm, highlight);
-      printf ("$}{run%d}{eve}\n", tb->run[from]);
+      eprintf ("$}{run%d}{eve}\n", tb->run[from]);
     }
   else if (from != -1 && to != -1)
     {
 
-      printf ("\\mess{$");
+      eprintf ("\\mess{$");
 
       latexTermPrint (sendTerm, highlight);
 
       if (!isTermEqual (sendTerm, readTerm))
 	{
-	  printf ("\\rightarrow");
+	  eprintf ("\\rightarrow");
 	  latexTermPrint (readTerm, highlight);
 	}
 
-      printf ("$}{run%d", tb->run[from]);
-      printf ("}{run%d}[%d]", tb->run[to],
-	      EVENTSPACE * (tinfo[to].position - tinfo[from].position));
+      eprintf ("$}{run%d", tb->run[from]);
+      eprintf ("}{run%d}[%d]", tb->run[to],
+	       EVENTSPACE * (tinfo[to].position - tinfo[from].position));
 
-      printf ("\n");
+      eprintf ("\n");
     }
 }
 
@@ -479,22 +479,22 @@ latexClaim (struct tracebuf *tb, int run, Termlist tl)
 {
   if (pass == 1)
     {
-      printf ("\\maxlength{\\maxmsccondition}{");
+      eprintf ("\\maxlength{\\maxmsccondition}{");
     }
   else
     {
-      printf ("\\condition{");
+      eprintf ("\\condition{");
     }
-  printf ("$\\neg secret ");
+  eprintf ("$\\neg secret ");
   termlistPrint (tl);
-  printf ("$}");
+  eprintf ("$}");
   if (pass == 1)
     {
-      printf ("\n");
+      eprintf ("\n");
     }
   else
     {
-      printf ("{run%d}\n", run);
+      eprintf ("{run%d}\n", run);
     }
 }
 
@@ -547,7 +547,7 @@ latexCorrespondingSend (struct tracebuf *tb, int rd)
 	    {
 	      /* bingo! success on all matches */
 
-	      //printf("Found perfect match: %d\n", s);
+	      //eprintf("Found perfect match: %d\n", s);
 	      bestSendEvent = sendEvent;
 	      break;
 	    }
@@ -604,7 +604,7 @@ latexCorrespondingSend (struct tracebuf *tb, int rd)
 
   if (bestSendEvent == -1)
     {
-      printf ("%% Could not find a matching SEND\n");
+      eprintf ("%% Could not find a matching SEND\n");
     }
   return bestSendEvent;
 }
@@ -628,9 +628,9 @@ latexCorrespondingSend2 (struct tracebuf *tb, int readEvent)
 	  if (!inKnowledge (tb->know[u], tb->event[readEvent]->message))
 	    {
 	      /*
-	         printf("%% term[");
-	         printf("]#%d is introduced at traceEvent[%d] ",readEvent,u);
-	         printf("\n");
+	         eprintf("%% term[");
+	         eprintf("]#%d is introduced at traceEvent[%d] ",readEvent,u);
+	         eprintf("\n");
 	       */
 	      return u;
 	    }
@@ -650,7 +650,7 @@ knowledgePrintLatex (Knowledge know)
 
   if (know == NULL)
     {
-      printf ("\\emptyset");
+      eprintf ("\\emptyset");
     }
   else
     {
@@ -681,7 +681,7 @@ attackDisplayLatex (const System sys)
   tb = sys->attack;
   if (tb == NULL)
     {
-      printf ("Attack pointer empty: nothing to display.\n");
+      eprintf ("Attack pointer empty: nothing to display.\n");
       exit (1);
     }
   /* set variables */
@@ -692,49 +692,49 @@ attackDisplayLatex (const System sys)
   tracebufRebuildKnow (tb);
 
   /* Make a comment in which the trace is displayed, for debugging etc. */
-  printf ("\n\\comment{ TRACE\n\n");
-  printf ("Length: %i\n", tb->length);
-  printf ("Reallength: %i\n", tb->reallength);
-  printf ("\n");
+  eprintf ("\n\\comment{ TRACE\n\n");
+  eprintf ("Length: %i\n", tb->length);
+  eprintf ("Reallength: %i\n", tb->reallength);
+  eprintf ("\n");
   i = 0;
   while (i <= tb->length)
     {
-      printf ("Knowledge %i:\n", i);
+      eprintf ("Knowledge %i:\n", i);
       knowledgePrint (tb->know[i]);
-      printf (" [Inverses]: ");
+      eprintf (" [Inverses]: ");
       knowledgeInversesPrint (tb->know[i]);
-      printf ("\n\n");
+      eprintf ("\n\n");
       if (i < tb->length)
 	{
-	  printf ("Event %i\t[", i);
+	  eprintf ("Event %i\t[", i);
 	  switch (tb->status[i])
 	    {
 	    case S_UNK:
-	      printf ("?");
+	      eprintf ("?");
 	      break;
 	    case S_RED:
-	      printf ("redundant");
+	      eprintf ("redundant");
 	      break;
 	    case S_TOD:
-	      printf ("to do");
+	      eprintf ("to do");
 	      break;
 	    case S_OKE:
-	      printf ("okay");
+	      eprintf ("okay");
 	      break;
 	    default:
-	      printf ("illegal status code");
+	      eprintf ("illegal status code");
 	      break;
 	    }
-	  printf ("]\t");
+	  eprintf ("]\t");
 	  termPrint (tb->event[i]->message);
-	  printf ("\t#%i", tb->run[i]);
-	  printf ("\n");
+	  eprintf ("\t#%i", tb->run[i]);
+	  eprintf ("\n");
 	  roledefPrint (tb->event[i]);
-	  printf ("\n\n");
+	  eprintf ("\n\n");
 	}
       i++;
     }
-  printf ("}\n\n");
+  eprintf ("}\n\n");
 
   tinfo =
     (struct traceinfo *) memAlloc ((tb->length + 1) *
@@ -786,7 +786,7 @@ attackDisplayLatex (const System sys)
 	  if (tb->event[i]->type == READ && !tb->event[i]->internal)
 	    {
 	      bestSend = latexCorrespondingSend2 (tb, i);
-	      printf ("%% match: %d <-> %d\n", i, bestSend);
+	      eprintf ("%% match: %d <-> %d\n", i, bestSend);
 	      if (bestSend == -1)
 		continue;	// TODO major ugliness
 
@@ -801,9 +801,9 @@ attackDisplayLatex (const System sys)
 	    }
 	}
     }
-  printf ("\\comment{ claimDetails :\n");
+  eprintf ("\\comment{ claimDetails :\n");
   termlistPrint (claimDetails);
-  printf ("\n}\n");
+  eprintf ("\n}\n");
 
   // landscape = (width > 4);         // not for the time being
 
@@ -844,16 +844,16 @@ attackDisplayLatex (const System sys)
 		      if (runPosition[currRun] <= tinfo[tb->link[i]].position
 			  && currRun != tb->run[tb->link[i]])
 			{
-			  printf ("\\comment{\n");
+			  eprintf ("\\comment{\n");
 			  termPrint (tb->event[i]->message);
-			  printf ("\n");
+			  eprintf ("\n");
 			  termPrint (tb->event[tb->link[i]]->message);
-			  printf ("\n");
-			  printf ("%% termDistance: %f\n",
-				  termDistance (tb->event[i]->message,
-						tb->event[tb->link[i]]->
-						message));
-			  printf ("}\n");
+			  eprintf ("\n");
+			  eprintf ("%% termDistance: %f\n",
+				   termDistance (tb->event[i]->message,
+						 tb->event[tb->link[i]]->
+						 message));
+			  eprintf ("}\n");
 			  tinfo[i].position = tinfo[tb->link[i]].position;
 			  eventSize = 0;
 			}
@@ -879,7 +879,7 @@ attackDisplayLatex (const System sys)
 	    }
 	  if (!(tb->event[i]->type == READ && tb->event[i]->internal))
 	    runPosition[currRun] = tinfo[i].position + eventSize;
-	  /* printf("%% Event %d at %d\n", i, position); */
+	  /* eprintf("%% Event %d at %d\n", i, position); */
 	  position += eventSize;
 	}
     }
@@ -896,12 +896,12 @@ attackDisplayLatex (const System sys)
 
   for (pass = 1; pass <= 2; pass++)
     {
-      printf ("%% Pass %i\n\n", pass);
+      eprintf ("%% Pass %i\n\n", pass);
 
       if (pass == 1)
 	{
-	  printf ("\\maxlength{\\maxmscaction}{knows}\n");
-	  printf ("\\maxlength{\\maxmscaction}{creates}\n");
+	  eprintf ("\\maxlength{\\maxmscaction}{knows}\n");
+	  eprintf ("\\maxlength{\\maxmscaction}{creates}\n");
 	}
       else
 	{
@@ -909,18 +909,18 @@ attackDisplayLatex (const System sys)
 	  Term pname;
 
 	  /* slightly stretch measurements */
-	  printf ("\\addtolength{\\maxmscall}{2\\mscspacer}\n");
-	  printf ("\\addtolength{\\maxmscaction}{\\mscspacer}\n");
-	  printf ("\\addtolength{\\maxmscinst}{\\mscspacer}\n");
-	  printf ("\\addtolength{\\maxmsccondition}{\\mscspacer}\n");
+	  eprintf ("\\addtolength{\\maxmscall}{2\\mscspacer}\n");
+	  eprintf ("\\addtolength{\\maxmscaction}{\\mscspacer}\n");
+	  eprintf ("\\addtolength{\\maxmscinst}{\\mscspacer}\n");
+	  eprintf ("\\addtolength{\\maxmsccondition}{\\mscspacer}\n");
 
 	  /* put out computed widths */
 
-	  printf ("\\setlength{\\envinstdist}{0.7\\maxmscall}\n");
-	  printf ("\\setlength{\\instdist}{\\maxmscall}\n");
-	  printf ("\\setlength{\\actionwidth}{\\maxmscaction}\n");
-	  printf ("\\setlength{\\instwidth}{\\maxmscinst}\n");
-	  printf ("\\setlength{\\conditionoverlap}{0.5\\maxmsccondition}\n");
+	  eprintf ("\\setlength{\\envinstdist}{0.7\\maxmscall}\n");
+	  eprintf ("\\setlength{\\instdist}{\\maxmscall}\n");
+	  eprintf ("\\setlength{\\actionwidth}{\\maxmscaction}\n");
+	  eprintf ("\\setlength{\\instwidth}{\\maxmscinst}\n");
+	  eprintf ("\\setlength{\\conditionoverlap}{0.5\\maxmsccondition}\n");
 
 	  /* create MSC title, involving protocol names and such. */
 
@@ -949,10 +949,10 @@ attackDisplayLatex (const System sys)
 	}
       /* Add the intruder instance */
       if (pass == 2)
-	printf ("\\declinst{eve}{}{");
+	eprintf ("\\declinst{eve}{}{");
       else
-	printf ("\\maxlength{\\maxmscinst}{");
-      printf ("{\\bf Eve}: Intruder}\n\n");
+	eprintf ("\\maxlength{\\maxmscinst}{");
+      eprintf ("{\\bf Eve}: Intruder}\n\n");
 
       /* Print the local constants for each instance */
 
@@ -971,14 +971,14 @@ attackDisplayLatex (const System sys)
 		      if (first)
 			{
 			  if (pass == 1)
-			    printf ("\\maxlength{\\maxmscaction}{$");
+			    eprintf ("\\maxlength{\\maxmscaction}{$");
 			  else
-			    printf ("\\ActionBox{creates \\\\\n$");
+			    eprintf ("\\ActionBox{creates \\\\\n$");
 			  first = 0;
 			}
 		      else
 			{
-			  printf (", ");
+			  eprintf (", ");
 			}
 		      termPrint (tl->term);
 		    }
@@ -987,9 +987,9 @@ attackDisplayLatex (const System sys)
 	      if (!first)
 		{
 		  if (pass == 1)
-		    printf ("$}\n");
+		    eprintf ("$}\n");
 		  else
-		    printf ("$}{run%i}\n", i);
+		    eprintf ("$}{run%i}\n", i);
 		}
 	    }
 	}
@@ -998,13 +998,13 @@ attackDisplayLatex (const System sys)
 
       if (pass == 2)
 	{
-	  printf ("\\ActionBox{");
-	  printf ("knows \\\\\n$");
+	  eprintf ("\\ActionBox{");
+	  eprintf ("knows \\\\\n$");
 	  knowledgePrintLatex (tb->know[0]);
-	  printf ("$}");
-	  printf ("{eve}\n");
-	  printf ("\\nextlevel[3]\n");
-	  printf ("\n");
+	  eprintf ("$}");
+	  eprintf ("{eve}\n");
+	  eprintf ("\\nextlevel[3]\n");
+	  eprintf ("\n");
 	}
 
       /* print the events in the attack */
@@ -1059,25 +1059,25 @@ attackDisplayLatex (const System sys)
 
 		      if (pass == 1)
 			{
-			  printf ("\\maxlength{\\maxmscaction}{");
+			  eprintf ("\\maxlength{\\maxmscaction}{");
 			}
 		      else
 			{
-			  printf ("\\nextlevel[1]\n");
-			  printf ("\\ActionBox{learns \\\\\n");
+			  eprintf ("\\nextlevel[1]\n");
+			  eprintf ("\\ActionBox{learns \\\\\n");
 			}
-		      printf ("$");
+		      eprintf ("$");
 		      cKnowledge++;
 		      latexTermlistPrint (newtl, highlights);
-		      printf ("$}");
+		      eprintf ("$}");
 		      if (pass == 1)
 			{
-			  printf ("\n");
+			  eprintf ("\n");
 			}
 		      else
 			{
-			  printf ("{eve}\n");
-			  printf ("\\nextlevel[2]\n");
+			  eprintf ("{eve}\n");
+			  eprintf ("\\nextlevel[2]\n");
 			}
 		    }
 
diff --git a/src/main.c b/src/main.c
index 5e16eba..0404c07 100644
--- a/src/main.c
+++ b/src/main.c
@@ -267,7 +267,6 @@ main (int argc, char **argv)
   if (switches.engine == ARACHNE_ENGINE)
     {
       arachneDone ();
-      bindingDone ();
     }
   knowledgeDestroy (sys->know);
   systemDone (sys);
diff --git a/src/mgu.c b/src/mgu.c
index 714b267..a057455 100644
--- a/src/mgu.c
+++ b/src/mgu.c
@@ -40,24 +40,24 @@ showSubst (Term t)
     return;
 
   indent ();
-  printf ("Substituting ");
+  eprintf ("Substituting ");
   termPrint (t);
-  printf (", typed ");
+  eprintf (", typed ");
   termlistPrint (t->stype);
   if (realTermLeaf (t->subst))
     {
-      printf ("->");
+      eprintf ("->");
       termlistPrint (t->subst->stype);
     }
   else
     {
-      printf (", composite term");
+      eprintf (", composite term");
     }
   if (t->type != VARIABLE)
     {
-      printf (" (bound roleconstant)");
+      eprintf (" (bound roleconstant)");
     }
-  printf ("\n");
+  eprintf ("\n");
 #endif
 }
 
diff --git a/src/system.c b/src/system.c
index f19ddc0..30f17e3 100644
--- a/src/system.c
+++ b/src/system.c
@@ -18,6 +18,7 @@
 #include "mgu.h"
 #include "switches.h"
 #include "binding.h"
+#include "depend.h"
 #include "specialterm.h"
 
 //! Global flag that signals LaTeX output.
@@ -195,6 +196,13 @@ systemDone (const System sys)
       roleInstanceDestroy (sys);
     }
 
+  /* undo bindings (for arachne) */
+
+  if (switches.engine == ARACHNE_ENGINE)
+    {
+      bindingDone ();
+    }
+
   /* clear substructures */
   termlistDestroy (sys->secrets);
 
@@ -812,6 +820,12 @@ roleInstanceArachne (const System sys, const Protocol protocol,
 
   /* erase any substitutions in the role definition, as they are now copied */
   termlistSubstReset (role->variables);
+
+  /* length */
+  runs[rid].rolelength = roledef_length (runs[rid].start);
+
+  /* new graph to create */
+  dependPushRun (sys);
 }
 
 
@@ -949,6 +963,9 @@ roleInstanceModelchecker (const System sys, const Protocol protocol,
       /* Determine first read with variables besides agents */
       runs[rid].firstNonAgentRead = firstNonAgentRead (sys, rid);	// symmetry reduction type II
     }
+
+  /* length */
+  runs[rid].rolelength = roledef_length (runs[rid].start);
 }
 
 //! Instantiate a role by making a new run
@@ -989,6 +1006,12 @@ roleInstanceDestroy (const System sys)
       runid = sys->maxruns - 1;
       myrun = sys->runs[runid];
 
+      // Reset graph
+      if (switches.engine == ARACHNE_ENGINE)
+	{
+	  dependPopRun ();
+	}
+
       // Destroy roledef
       roledefDestroy (myrun.start);
 
diff --git a/src/system.h b/src/system.h
index cf06b02..4d5db0a 100644
--- a/src/system.h
+++ b/src/system.h
@@ -44,6 +44,7 @@ struct run
   Role role;			//!< Role of this run.
   Termlist agents;		//!< Agents involved in this run.
   int step;			//!< Current execution point in the run (integer)
+  int rolelength;		//!< Length of role
   Roledef index;		//!< Current execution point in the run (roledef pointer)
   Roledef start;		//!< Head of the run definition.
   Knowledge know;		//!< Current knowledge of the run.
diff --git a/src/todo.txt b/src/todo.txt
index 10df0d9..2f0f623 100644
--- a/src/todo.txt
+++ b/src/todo.txt
@@ -1,3 +1,8 @@
+- Old version enforced some extra orders:
+  1. M_0 roles were ordered before any other roles.
+  2. Local constants order: if a run has a local variable instantiated by
+  somebody else's variable, that should occur then after the initial sending
+  of that value...
 - Test 'sk(x)' in goals, somewhere before assessing a state (dus at the
   beginning of iterate), immediately reduce to 'sk(Eve)'. Test with
   --experimental. To that end, reintroduce a state-reporting switch.
@@ -7,24 +12,6 @@
   this requires some work at instantiation, because instantiated term
   couples should be added to the inverses list, and removed at
   descruction.
-- Warshall is taking a third of the time running.
-  - Make 'dirty' flag.
-  - Make a push-graph structure, where old graphs are simply remembered?
-    Does this help at all?
-  - Improve the speed of the thing by finally moving to a bit-thing.
-  Required interface:
-  * Abstract graph (node relations)
-    - make_empty_graph of size n (with ->cycle=0)
-    - destroy graph
-    - get_transitive_relation (g,n1,n2) (enforces closure)
-    - set_transitive_relation (g,n1,n2) (sets dirty flag, checks cycle)
-    - has_cycle (g)
-  * High-level (event dependencies)
-    - make_deps for current sys (make_empty+fill), returning cycle flag
-    - destroy_deps(G)
-    - set_deps (G,r1,s1,r2,s2), returning cycle flag
-    - get_deps (G,r1,s1,r2,s2)
-    - get_cycle_flag (G)
 - Simple timestamps could be added by prefixing send message before the
   role, sending any timestamp constants out first to the intruder. These
   should of course be hidden in the output somehow.
diff --git a/src/warshall.c b/src/warshall.c
index d181a1c..4ee3842 100644
--- a/src/warshall.c
+++ b/src/warshall.c
@@ -1,168 +1,85 @@
-/**
- *@file warshall.c
- *
- * Warshall's algorithm for transitive closure computation.
- *
- * Currently this is the slow integer-instead-of-bit olde slowe version.
- */
+// @file warshall.c
+/* Based on public-domain code from Berkeley Yacc */
 
-#include <limits.h>
 #include "warshall.h"
-#include "debug.h"
 
-//! fill the graph with some value
 void
-graph_fill (int *graph, int nodes, int value)
+transitive_closure (unsigned int *R, int n)
 {
-  int node;
+  register int rowsize;
+  register unsigned mask;
+  register unsigned *rowj;
+  register unsigned *rp;
+  register unsigned *rend;
+  register unsigned *ccol;
+  register unsigned *relend;
+  register unsigned *cword;
+  register unsigned *rowi;
 
-  node = 0;
-  while (node < (nodes * nodes))
+  rowsize = WORDSIZE (n);
+  relend = R + n * rowsize;
+
+  cword = R;
+  mask = 1;
+  rowi = R;
+  while (rowi < relend)
     {
-      graph[node] = value;
-      node++;
+      ccol = cword;
+      rowj = R;
+
+      while (rowj < relend)
+	{
+	  if (*ccol & mask)
+	    {
+	      rp = rowi;
+	      rend = rowj + rowsize;
+	      while (rowj < rend)
+		*rowj++ |= *rp++;
+	    }
+	  else
+	    {
+	      rowj += rowsize;
+	    }
+
+	  ccol += rowsize;
+	}
+
+      mask <<= 1;
+      if (mask == 0)
+	{
+	  mask = 1;
+	  cword++;
+	}
+
+      rowi += rowsize;
     }
 }
 
-//! Show a graph
 void
-graph_display (int *graph, int nodes)
+reflexive_transitive_closure (unsigned int *R, int n)
 {
-  int i;
+  register int rowsize;
+  register unsigned mask;
+  register unsigned *rp;
+  register unsigned *relend;
 
-  int index (const int i, const int j)
-  {
-    return (i * nodes + j);
-  }
+  transitive_closure (R, n);
 
-  i = 0;
-  while (i < nodes)
+  rowsize = WORDSIZE (n);
+  relend = R + n * rowsize;
+
+  mask = 1;
+  rp = R;
+  while (rp < relend)
     {
-      int j;
-      j = 0;
-      while (j < nodes)
+      *rp |= mask;
+      mask <<= 1;
+      if (mask == 0)
 	{
-	  eprintf ("%i ", graph[index (i, j)]);
-	  j++;
+	  mask = 1;
+	  rp++;
 	}
-      eprintf ("\n");
-      i++;
+
+      rp += rowsize;
     }
 }
-
-
-//! Apply warshall's algorithm to determine the closure of a graph
-/**
- * If j<i and k<j, then k<i.
- * Could be done more efficiently but that is irrelevant here.
- *
- *@param graph A pointer to the integer array of nodes*nodes elements.
- *@param nodes The number of nodes in the graph.
- *@Returns 0 if there is a cycle; and the algorithm aborts, 1 if there is no cycle and the result is okay.
- */
-int
-warshall (int *graph, int nodes)
-{
-  int k;
-
-  int index (const int x, const int y)
-  {
-    return (x * nodes + y);
-  }
-
-  k = 0;
-  while (k < nodes)
-    {
-      int i;
-
-      i = 0;
-      while (i < nodes)
-	{
-	  if (graph[index (i, k)] == 1)
-	    {
-	      int j;
-
-	      j = 0;
-	      while (j < nodes)
-		{
-		  if (graph[index (k, j)] == 1)
-		    {
-		      if (i == j)
-			{
-			  // Oh no! A cycle.
-			  graph[index (i, j)] = 2;
-#ifdef DEBUG
-			  if (DEBUGL (5))
-			    {
-			      graph_display (graph, nodes);
-			    }
-#endif
-			  return 0;
-			}
-		      graph[index (i, j)] = 1;
-		    }
-		  j++;
-		}
-	    }
-	  i++;
-	}
-      k++;
-    }
-  return 1;
-}
-
-
-//! Determine ranks for all nodes
-/**
- * Some crude algorithm I sketched on the blackboard.
- */
-int
-graph_ranks (int *graph, int *ranks, int nodes)
-{
-  int i;
-  int todo;
-  int rank;
-
-  i = 0;
-  while (i < nodes)
-    {
-      ranks[i] = INT_MAX;
-      i++;
-    }
-
-  todo = nodes;
-  rank = 0;
-  while (todo > 0)
-    {
-      // There are still unassigned nodes
-      int n;
-
-      n = 0;
-      while (n < nodes)
-	{
-	  if (ranks[n] == INT_MAX)
-	    {
-	      // Does this node have incoming stuff from stuff with equal rank or higher?
-	      int refn;
-
-	      refn = 0;
-	      while (refn < nodes)
-		{
-		  if (ranks[refn] >= rank
-		      && graph[graph_index (refn, n)] != 0)
-		    refn = nodes + 1;
-		  else
-		    refn++;
-		}
-	      if (refn == nodes)
-		{
-		  ranks[n] = rank;
-		  todo--;
-		}
-	    }
-	  n++;
-	}
-      rank++;
-    }
-  return rank;
-}
diff --git a/src/warshall.h b/src/warshall.h
index d4f963b..3473919 100644
--- a/src/warshall.h
+++ b/src/warshall.h
@@ -1,5 +1,48 @@
-// Header file for warshall.c
+/***********************************************************************/
+/* Based on public-domain code from Berkeley Yacc */
 
-void graph_fill (int *graph, int nodes, int value);
-int warshall (int *graph, int nodes);
-int graph_ranks (int *graph, int *ranks, int nodes);
+#include <assert.h>
+#include <ctype.h>
+#include <errno.h>
+#include <limits.h>
+#include <stdio.h>
+#include <stdlib.h>
+
+/*  machine-dependent definitions                              */
+/*  the following definitions are for the Tahoe                */
+/*  they might have to be changed for other machines           */
+
+/*  MAXCHAR is the largest unsigned character value            */
+/*  MAXSHORT is the largest value of a C short                 */
+/*  MINSHORT is the most negative value of a C short           */
+/*  MAXTABLE is the maximum table size                         */
+/*  BITS_PER_WORD is the number of bits in a C unsigned        */
+/*  WORDSIZE computes the number of words needed to            */
+/*        store n bits                                         */
+/*  BIT returns the value of the n-th bit starting             */
+/*        from r (0-indexed)                                   */
+/*  SETBIT sets the n-th bit starting from r                   */
+
+#define        MAXCHAR                UCHAR_MAX
+#define        MAXSHORT        SHRT_MAX
+#define MINSHORT        SHRT_MIN
+#define MAXTABLE        32500
+
+#define BITS_PER_WORD        (8*sizeof(unsigned))
+#define        WORDSIZE(n)        (((n)+(BITS_PER_WORD-1))/BITS_PER_WORD)
+#define        BIT(r, n)        ((((r)[(n)/BITS_PER_WORD])>>((n)%BITS_PER_WORD))&1)
+#define        SETBIT(r, n)        ((r)[(n)/BITS_PER_WORD]|=(1<<((n)%BITS_PER_WORD)))
+
+/*  storage allocation macros  */
+
+#define CALLOC(k,n)      (calloc((unsigned)(k),(unsigned)(n)))
+#define FREE(x)          (free((char*)(x)))
+#define MALLOC(n)        (malloc((unsigned)(n)))
+#define NEW(t)           ((t*)allocate(sizeof(t)))
+#define NEW2(n,t)        ((t*)allocate((unsigned)((n)*sizeof(t))))
+#define REALLOC(p,n)     (realloc((char*)(p),(unsigned)(n)))
+
+/* actual functions */
+
+void transitive_closure (unsigned int *R, int n);
+void reflexive_transitive_closure (unsigned int *R, int n);