diff --git a/src/arachne.c b/src/arachne.c
index a26929f..db3527a 100644
--- a/src/arachne.c
+++ b/src/arachne.c
@@ -7,6 +7,7 @@
  *
  */
 
+#include <stdlib.h>
 #include <limits.h>
 #include <float.h>
 #ifdef DEBUG
@@ -48,6 +49,7 @@ static int attack_length;
 Protocol INTRUDER;		// Pointers, to be set by the Init
 Role I_M;			// Same here.
 Role I_RRS;
+Role I_RRSD;
 
 static int indentDepth;
 static int proofDepth;
@@ -125,6 +127,15 @@ arachneInit (const System mysys)
   add_event (SEND, NULL);
   I_RRS = add_role ("I_E: Encrypt");
 
+  add_event (READ, NULL);
+  add_event (READ, NULL);
+  add_event (SEND, NULL);
+  I_RRSD = add_role ("I_D: Decrypt");
+
+  num_regular_runs = 0;
+  num_intruder_runs = 0;
+  max_encryption_level = 0;
+
   return;
 }
 
@@ -621,9 +632,76 @@ iterate_role_sends (int (*func) ())
   return iterate_role_events (send_wrapper);
 }
 
+//! Create decryption role instance
+/**
+ * Note that this does not add any bindings for the reads.
+ *
+ *@param term	The term to be decrypted (implies decryption key)
+ *
+ *@returns The run id of the decryptor instance
+ */
+int
+create_decryptor (const Term term, const Term key)
+{
+  if (term != NULL && isTermEncrypt (term))
+    {
+      Roledef rd;
+      Term tempkey;
+      int run;
+
+      run = semiRunCreate (INTRUDER, I_RRSD);
+      rd = sys->runs[run].start;
+      rd->message = termDuplicateUV (term);
+      rd->next->message = termDuplicateUV (key);
+      rd->next->next->message = termDuplicateUV (TermOp (term));
+      sys->runs[run].step = 3;
+      proof_suppose_run (run, 0, 3);
+
+      return run;
+    }
+  else
+    {
+      globalError++;
+      printf ("Term for which a decryptor instance is requested: ");
+      termPrint (term);
+      printf ("\n");
+      error
+	("Trying to build a decryptor instance for a non-encrypted term.");
+    }
+}
+
+//! Get the priority level of a key that is needed for a term (typical pk/sk distinction)
+int
+getPriorityOfNeededKey (const System sys, const Term keyneeded)
+{
+  int prioritylevel;
+
+  /* Normally, a key gets higher priority, but unfortunately this is not propagated at the moment. Maybe later.
+   */
+  prioritylevel = 1;
+  if (realTermEncrypt (keyneeded))
+    {
+      /* the key is a construction itself */
+      if (inKnowledge (sys->know, TermKey (keyneeded)))
+	{
+	  /* the key is constructed by a public thing */
+	  /* typically, this is a public key, so we postpone it  */
+	  prioritylevel = -1;
+	}
+    }
+  return prioritylevel;
+}
+
 //! Try to bind a specific existing run to a goal.
 /**
  * The key goals are bound to the goal.
+ *
+ *@todo This is currently NOT correct. The point is that the key chain
+ * cannot uniquely define a path through a term in general, and
+ * a rewrite of termMguSubterm is needed. It should not yield the
+ * needed keys, but simply the path throught the term. This would enable
+ * reconstruction of the keys anyway. TODO
+ *      
  *@param subterm determines whether it is a subterm unification or not.
  */
 int
@@ -635,7 +713,7 @@ bind_existing_to_goal (const Binding b, const int run, const int index)
   int newgoals;
   int found;
 
-  int subterm_iterate (Termlist substlist, Termlist keylist)
+  int subterm_iterate (Termlist substlist, Termlist cryptlist)
   {
     int flag;
 
@@ -644,55 +722,148 @@ bind_existing_to_goal (const Binding b, const int run, const int index)
     /**
      * Now create the new bindings
      */
-    if (goal_bind (b, run, index))
+    int newgoals;
+    int newruns;
+    int stillvalid;
+
+    Binding smalltermbinding;
+
+    stillvalid = true;		// New stuff is valid (no cycles)
+    newgoals = 0;		// No new goals introduced (yet)
+    newruns = 0;		// New runs introduced
+    smalltermbinding = b;	// Start off with destination binding
+
+#ifdef DEBUG
+    if (DEBUGL (4))
       {
-	int newgoals;
-	Termlist tl;
-
-	proof_suppose_binding (b);
-	if (keylist != NULL && sys->output == PROOF)
-	  {
-	    indentPrint ();
-	    eprintf
-	      ("This introduces the obligation to produce the following keys: ");
-	    termlistPrint (keylist);
-	    eprintf ("\n");
-	  }
-	newgoals = 0;
-	tl = keylist;
-	while (tl != NULL)
-	  {
-	    int keyrun;
-	    int prioritylevel;
-
-	    /* normally, a key gets higher priority */
-	    prioritylevel = 1;
-	    if (realTermEncrypt (tl->term))
-	      {
-		/* the key is a construction itself */
-		if (inKnowledge (sys->know, TermKey (tl->term)))
-		  {
-		    /* the key is constructed by a public thing */
-		    /* typically, this is a public key, so we postpone it  */
-		    prioritylevel = -1;
-		  }
-	      }
-	    /* add the key as a goal */
-	    newgoals =
-	      newgoals + goal_add (tl->term, b->run_to, b->ev_to,
-				   prioritylevel);
-	    tl = tl->next;
-	  }
-
-	indentDepth++;
-	flag = flag && iterate ();
-	indentDepth--;
-
-	goal_remove_last (newgoals);
+	printf ("Trying to bind the small term ");
+	termPrint (b->term);
+	printf (" as coming from the big send ");
+	termPrint (rd->message);
+	printf (" , binding ");
+	termPrint (b->term);
+	printf ("\nCrypted list needed: ");
+	termlistPrint (cryptlist);
+	printf ("\n");
       }
-    else
+#endif
+    if (cryptlist != NULL && sys->output == PROOF)
       {
-	proof_cannot_bind (b, run, index);
+	indentPrint ();
+	eprintf
+	  ("This introduces the obligation to decrypted the following encrypted subterms: ");
+	termlistPrint (cryptlist);
+	eprintf ("\n");
+      }
+
+    /* The order of the cryptlist is inner -> outer */
+    while (stillvalid && cryptlist != NULL && smalltermbinding != NULL)
+      {
+	/*
+	 * Invariants:
+	 *
+	 * smalltermbinding     binding to be satisfied next (and for which a decryptor is needed)
+	 */
+	Term keyneeded;
+	int prioritylevel;
+	int smallrun;
+	int count;
+	Roledef rddecrypt;
+	Binding bnew;
+	int res;
+
+	/*
+	 * 1. Add decryptor
+	 */
+
+	keyneeded =
+	  inverseKey (sys->know->inverses, TermKey (cryptlist->term));
+	prioritylevel = getPriorityOfNeededKey (sys, keyneeded);
+	smallrun = create_decryptor (cryptlist->term, keyneeded);
+	rddecrypt = sys->runs[smallrun].start;
+	termDelete (keyneeded);
+	newruns++;
+
+	/*
+	 * 2. Add goal bindings
+	 */
+
+	count = goal_add (rddecrypt->message, smallrun, 0, 0);
+	newgoals = newgoals + count;
+	if (count >= 0)
+	  {
+	    if (count > 1)
+	      {
+		error
+		  ("Added more than one goal for decryptor goal 1, weird.");
+	      }
+	    else
+	      {
+		// This is the unique new goal then
+		bnew = (Binding) sys->bindings->data;
+	      }
+	  }
+	else
+	  {
+	    // No new binding? Weird, but fair enough
+	    bnew = NULL;
+	  }
+	newgoals =
+	  newgoals + goal_add (rddecrypt->next->message, smallrun, 1,
+			       prioritylevel);
+
+	/*
+	 * 3. Bind open goal to decryptor
+	 */
+
+	res = goal_bind (smalltermbinding, smallrun, 2);	// returns 0 iff invalid
+	if (res != 0)
+	  {
+	    // Allright, good binding, proceed with next
+	    smalltermbinding = bnew;
+	  }
+	else
+	  {
+	    stillvalid = false;
+	  }
+
+	/* progression */
+	cryptlist = cryptlist->next;
+      }
+
+    /*
+     * Decryptors for any nested keys have been added. Now we can fill the
+     * final binding.
+     */
+
+    if (stillvalid)
+      {
+	if (goal_bind (smalltermbinding, run, index))
+	  {
+	    proof_suppose_binding (b);
+#ifdef DEBUG
+	    if (DEBUGL (4))
+	      {
+		indentPrint ();
+		eprintf ("Added %i new goals, iterating.\n", newgoals);
+	      }
+#endif
+	    /* Iterate process */
+	    indentDepth++;
+	    flag = flag && iterate ();
+	    indentDepth--;
+	  }
+	else
+	  {
+	    proof_cannot_bind (b, run, index);
+	  }
+      }
+
+    goal_remove_last (newgoals);
+    while (newruns > 0)
+      {
+	semiRunDestroy ();
+	newruns--;
       }
     goal_unbind (b);
     return flag;
@@ -2754,7 +2925,8 @@ prune_claim_specifics ()
     {
       if (arachne_claim_niagree (sys, 0, sys->current_claim->ev))
 	{
-	  sys->current_claim->count = statesIncrease (sys->current_claim->count);
+	  sys->current_claim->count =
+	    statesIncrease (sys->current_claim->count);
 	  if (sys->output == PROOF)
 	    {
 	      indentPrint ();
@@ -2768,7 +2940,8 @@ prune_claim_specifics ()
     {
       if (arachne_claim_nisynch (sys, 0, sys->current_claim->ev))
 	{
-	  sys->current_claim->count = statesIncrease (sys->current_claim->count);
+	  sys->current_claim->count =
+	    statesIncrease (sys->current_claim->count);
 	  if (sys->output == PROOF)
 	    {
 	      indentPrint ();
diff --git a/src/binding.c b/src/binding.c
index a51fce7..08dd76a 100644
--- a/src/binding.c
+++ b/src/binding.c
@@ -47,7 +47,7 @@ binding_create (Term term, int run_to, int ev_to)
   b->ev_from = -1;
   b->run_to = run_to;
   b->ev_to = ev_to;
-  goal_graph_destroy();
+  goal_graph_destroy ();
   b->term = term;
   b->level = 0;
   return b;
@@ -104,15 +104,15 @@ goal_graph_destroy ()
       struct mallinfo mi_free;
       int mem_free;
 
-      mi_free = mallinfo();
+      mi_free = mallinfo ();
       mem_free = mi_free.uordblks;
 #endif
       memFree (graph, (nodes * nodes) * sizeof (int));
       graph = NULL;
 #ifdef DEBUG
-      mi_free = mallinfo();
+      mi_free = mallinfo ();
       if (mem_free - mi_free.uordblks != graph_uordblks)
-	  error ("Freeing gave a weird result.");
+	error ("Freeing gave a weird result.");
 #endif
       graph_uordblks = 0;
       nodes = 0;
@@ -132,211 +132,217 @@ goal_graph_create ()
   // Setup graph
   nodes = node_count ();
 
-    {
-      struct mallinfo create_mi;
-      int create_mem_before;
+  {
+    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;
-    }
+    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);
+    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;
+    // 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))
-	    {
+	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);
+	    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;
+	    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;
+	    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;
+		    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;
+			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;
+			    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;
+				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;
+					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;
+						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);
-								}
+							    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 (sys->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++;
-	}
-    }
+							    done = 1;
+							  }
+							else
+							  {
+							    // It doesn't occur first in a READ, which shouldn't be happening
+							    if (sys->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++;
+      }
+  }
 }
 
 
@@ -432,9 +438,6 @@ binding_print (const Binding b)
 int
 goal_add (Term term, const int run, const int ev, const int level)
 {
-  int sum;
-
-  sum = 0;
   term = deVar (term);
 #ifdef DEBUG
   if (term == NULL)
@@ -447,9 +450,8 @@ goal_add (Term term, const int run, const int ev, const int level)
 #endif
   if (realTermTuple (term))
     {
-      sum = sum + 
-	  goal_add (TermOp1 (term), run, ev, level) + 
-	  goal_add (TermOp2 (term), run, ev, level);
+      return goal_add (TermOp1 (term), run, ev, level) +
+	goal_add (TermOp2 (term), run, ev, level);
     }
   else
     {
@@ -479,24 +481,81 @@ goal_add (Term term, const int run, const int ev, const int level)
 	  b = binding_create (term, run, ev);
 	  b->level = level;
 	  sys->bindings = list_insert (sys->bindings, b);
-	  sum = sum + 1;
+#ifdef DEBUG
+	  if (DEBUGL (3))
+	    {
+	      eprintf ("Adding new binding for ");
+	      termPrint (term);
+	      eprintf (" to run %i, ev %i.\n", run, ev);
+	    }
+#endif
+	  return 1;
 	}
     }
-  return sum;
+  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)
 {
-  while (n > 0 && (sys->bindings != NULL))
+  while (n > 0)
     {
-      Binding b;
+      if (sys->bindings != NULL)
+	{
+	  Binding b;
 
-      b = (Binding) sys->bindings->data;
-      binding_destroy (b);
-      sys->bindings = list_delete (sys->bindings);
-      n--;
+	  b = (Binding) sys->bindings->data;
+	  binding_destroy (b);
+	  sys->bindings = list_delete (sys->bindings);
+	  n--;
+	}
+      else
+	{
+	  error
+	    ("goal_remove_last error: trying to remove %i too many bindings.",
+	     n);
+	}
     }
 }
 
@@ -522,6 +581,8 @@ goal_bind (const Binding b, const int run, const int ev)
     }
   else
     {
+      globalError++;
+      binding_print (b);
       error ("Trying to bind a bound goal again.");
     }
 }
@@ -545,7 +606,8 @@ goal_unbind (const Binding b)
 /**
  * Especially made for tuple expansion
  */
-int binding_block (Binding b)
+int
+binding_block (Binding b)
 {
   if (!b->blocked)
     {
@@ -559,7 +621,8 @@ int binding_block (Binding b)
 }
 
 //! Unblock a binding
-int binding_unblock (Binding b)
+int
+binding_unblock (Binding b)
 {
   if (b->blocked)
     {
@@ -630,12 +693,13 @@ labels_ordered (Termmap runs, Termlist labels)
 }
 
 //! Check whether the binding denotes a sensible thing such that we can use run_from and ev_from
-int valid_binding (Binding b)
+int
+valid_binding (Binding b)
 {
   if (b->done && !b->blocked)
-      return 1;
+    return 1;
   else
-      return 0;
+    return 0;
 }
 
 //! Prune invalid state w.r.t. <=C minimal requirement
@@ -656,7 +720,19 @@ bindings_c_minimal ()
       // Recompute closure; does that work?
       if (!warshall (graph, nodes))
 	{
-	  // Hmm, cycle
+	  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");
 	}
     }
@@ -669,7 +745,7 @@ bindings_c_minimal ()
 
       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))
+      if (valid_binding (b))
 	{
 	  int run;
 	  int node_from;
diff --git a/src/binding.h b/src/binding.h
index 5e9bc96..f1e1a25 100644
--- a/src/binding.h
+++ b/src/binding.h
@@ -43,6 +43,8 @@ int binding_print (Binding b);
 int valid_binding (Binding b);
 
 int goal_add (Term term, const int run, const int ev, const int level);
+int goal_add_fixed (Term term, const int run, const int ev, const int fromrun,
+		    const int fromev);
 void goal_remove_last (int n);
 int goal_bind (const Binding b, const int run, const int ev);
 void goal_unbind (const Binding b);
diff --git a/src/compiler.c b/src/compiler.c
index 540ef7b..4a83c9a 100644
--- a/src/compiler.c
+++ b/src/compiler.c
@@ -1018,9 +1018,13 @@ order_label_roles (const Claimlist cl)
       int scan_label (void *data)
       {
 	Labelinfo linfo;
+	Termlist tl;
 
 	linfo = (Labelinfo) data;
-	if (inTermlist (cl->prec, linfo->label))
+	if (linfo == NULL)
+	  return 1;
+	tl = cl->prec;
+	if (inTermlist (tl, linfo->label))
 	  {
 	    if (linfo->protocol == cl->protocol)
 	      {
diff --git a/src/mgu.c b/src/mgu.c
index 0529031..3654fbe 100644
--- a/src/mgu.c
+++ b/src/mgu.c
@@ -60,32 +60,32 @@ goodsubst (Term tvar, Term tsubst)
 {
   // function to test compatibility
   __inline__ int compatibleTypes ()
-    {
-      if (tvar->stype == NULL)
-	{
-	  // If the variable type is unspecified, anything goes
-	  return 1;
-	}
-      else
-	{
-	  // There are variable types.
-	  // At least one of them should match a type of the constant.
-	  Termlist tl;
+  {
+    if (tvar->stype == NULL)
+      {
+	// If the variable type is unspecified, anything goes
+	return 1;
+      }
+    else
+      {
+	// There are variable types.
+	// At least one of them should match a type of the constant.
+	Termlist tl;
 
-	  tl = tvar->stype;
-	  while (tl != NULL)
-	    {
-	      if (inTermlist (tsubst->stype, tl->term))
-		{
-		  // One type matches
-		  return 1;
-		}
-	      tl = tl->next;
-	    }
-	  // No matches
-	  return 0;
-	}
-    }
+	tl = tvar->stype;
+	while (tl != NULL)
+	  {
+	    if (inTermlist (tsubst->stype, tl->term))
+	      {
+		// One type matches
+		return 1;
+	      }
+	    tl = tl->next;
+	  }
+	// No matches
+	return 0;
+      }
+  }
 
   if (mgu_match == 2)
     {
@@ -104,8 +104,7 @@ goodsubst (Term tvar, Term tsubst)
       else
 	{
 	  // It's a leaf, but what type?
-	  if (mgu_match == 1
-	      || compatibleTypes ())
+	  if (mgu_match == 1 || compatibleTypes ())
 	    {
 	      return 1;
 	    }
@@ -305,68 +304,69 @@ termMguInTerm (Term t1, Term t2, int (*iterator) (Termlist))
   return flag;
 }
 
-//! Most general subterm unifiers of t1 subterm t2
+//! Most general subterm unifiers of smallterm subterm bigterm
 /**
  * Try to determine the most general subterm unifiers of two terms.
- *@returns Nothing. Iteration gets termlist of subst, and list of keys needed to decrypt.
+ *@returns Nothing. Iteration gets termlist of subst, and list of keys needed
+ *  to decrypt. This termlist does not need to be deleted, because it is handled
+ *  by the mguSubTerm itself.
  */
 int
-termMguSubTerm (Term t1, Term t2, int (*iterator) (Termlist, Termlist),
-		Termlist inverses, Termlist keylist)
+termMguSubTerm (Term smallterm, Term bigterm,
+		int (*iterator) (Termlist, Termlist), Termlist inverses,
+		Termlist cryptlist)
 {
   int flag;
 
   flag = 1;
-  t1 = deVar (t1);
-  t2 = deVar (t2);
-  if (t2 != NULL)
+  smallterm = deVar (smallterm);
+  bigterm = deVar (bigterm);
+  if (bigterm != NULL)
     {
       Termlist tl;
 
-      if (!realTermLeaf (t2))
+      if (!realTermLeaf (bigterm))
 	{
-	  if (realTermTuple (t2))
+	  if (realTermTuple (bigterm))
 	    {
 	      // 'simple' tuple
 	      flag =
-		flag && termMguSubTerm (t1, TermOp1 (t2), iterator, inverses,
-					keylist);
-	      flag =
-		flag && termMguSubTerm (t1, TermOp2 (t2), iterator, inverses,
-					keylist);
+		flag
+		&& termMguSubTerm (smallterm, TermOp1 (bigterm), iterator,
+				   inverses, cryptlist);
+	      flag = flag
+		&& termMguSubTerm (smallterm, TermOp2 (bigterm), iterator,
+				   inverses, cryptlist);
 	    }
 	  else
 	    {
 	      // Must be encryption
-	      // So, we need the key, and try to get the rest
-	      Term newkey;
+	      Term keyneeded;
 
-	      newkey = inverseKey (inverses, TermKey (t2));
+	      keyneeded = inverseKey (inverses, TermKey (bigterm));
 	      // We can never produce the TERM_Hidden key, thus, this is not a valid iteration.
-	      if (!isTermEqual (newkey, TERM_Hidden))
+	      if (!isTermEqual (keyneeded, TERM_Hidden))
 		{
-		  Termlist keylist_new;
-
-		  keylist_new = termlistShallow (keylist);
-		  keylist_new = termlistAdd (keylist_new, newkey);
+		  cryptlist = termlistAdd (cryptlist, bigterm);	// Append, so the last encrypted term in the list is the most 'inner' one, and the first is the outer one.
 
 		  // Recurse
 		  flag =
 		    flag
-		    && termMguSubTerm (t1, TermOp (t2), iterator, inverses,
-				       keylist_new);
+		    && termMguSubTerm (smallterm, TermOp (bigterm), iterator,
+				       inverses, cryptlist);
 
-		  termlistDelete (keylist_new);
+
+		  cryptlist = termlistDelTerm (cryptlist);
 		}
-	      termDelete (newkey);
+	      termDelete (keyneeded);
 	    }
 	}
       // simple clause or combined
-      tl = termMguTerm (t1, t2);
+      tl = termMguTerm (smallterm, bigterm);
       if (tl != MGUFAIL)
 	{
 	  // Iterate
-	  flag = flag && iterator (tl, keylist);
+	  flag = flag && iterator (tl, cryptlist);
 	  // Reset variables
 	  termlistSubstReset (tl);
 	  // Remove list
@@ -375,7 +375,7 @@ termMguSubTerm (Term t1, Term t2, int (*iterator) (Termlist, Termlist),
     }
   else
     {
-      if (t1 != NULL)
+      if (smallterm != NULL)
 	{
 	  flag = 0;
 	}
diff --git a/src/system.c b/src/system.c
index 45ebe77..3567085 100644
--- a/src/system.c
+++ b/src/system.c
@@ -101,6 +101,7 @@ systemInit ()
   sys->roleeventmax = 0;
   sys->claimlist = NULL;
   sys->labellist = NULL;
+  sys->match = 0;		// default matching
 
   /* matching CLP */
   sys->constraints = NULL;	// no initial constraints
diff --git a/src/term.c b/src/term.c
index ff60804..73ee898 100644
--- a/src/term.c
+++ b/src/term.c
@@ -683,7 +683,7 @@ tupleCount (Term tt)
 //! Yield the projection Pi(n) of a term.
 /**
  *@param tt Term
- *@param n The index in the tuple.
+ *@param n The index in the tuple [0..tupleCount-1]
  *@return Returns either a pointer to a term, or NULL if the index is out of range.
  *\sa tupleCount()
  */
@@ -1085,7 +1085,7 @@ term_encryption_level (const Term term)
     if (t == NULL)
       {
 #ifdef DEBUG
-	if (DEBUGL(2))
+	if (DEBUGL (2))
 	  {
 	    eprintf ("Warning: Term encryption level finds a NULL for term ");
 	    termPrint (term);
diff --git a/src/termlist.c b/src/termlist.c
index 8ed23ce..cc2a001 100644
--- a/src/termlist.c
+++ b/src/termlist.c
@@ -272,7 +272,8 @@ termlistConcat (Termlist tl1, Termlist tl2)
 
 //! Remove the pointed at element from the termlist.
 /**
- * Easier because of the double linked list.
+ * Easier because of the double linked list. Note: does not do termDelete on the term.
+ *
  *@param tl The pointer to the termlist node to be deleted from the list.
  *@return The possibly new head pointer to the termlist.
  */
@@ -667,8 +668,7 @@ termlistLocal (Termlist tl, const Termlist fromlist, const Termlist tolist)
 
   while (tl != NULL)
     {
-      newtl =
-	termlistAdd (newtl, termLocal (tl->term, fromlist, tolist));
+      newtl = termlistAdd (newtl, termLocal (tl->term, fromlist, tolist));
       tl = tl->next;
     }
   return newtl;