diff --git a/src/arachne.c b/src/arachne.c
index e1600b6..d56e249 100644
--- a/src/arachne.c
+++ b/src/arachne.c
@@ -258,7 +258,7 @@ create_intruder_goal (Term t)
   int run;
   Roledef rd;
 
-  roleInstance (sys, INTRUDER, I_GOAL, NULL);
+  roleInstance (sys, INTRUDER, I_GOAL, NULL, NULL);
   run = sys->maxruns - 1;
   rd = sys->runs[run].start;
   sys->runs[run].length = 1;
@@ -300,9 +300,12 @@ add_intruder_goal_iterate (Goal goal)
 }
 
 //! Bind a goal to an existing regular run, if possible
+/**
+ *@todo Currently we don't use subterm. This interm binds, which is much different from subterm binding.
+ */
 int
 bind_existing_run (const Goal goal, const Protocol p, const Role r,
-		   const int index, const int forced_run)
+		   const int index, const int forced_run, const int subterm)
 {
   int run, flag;
 
@@ -342,13 +345,16 @@ bind_existing_run (const Goal goal, const Protocol p, const Role r,
 		  explanation = "Bind existing run";
 		  e_run = run;
 		  e_term1 = goal.rd->message;
+		  e_term2 = rd->message;
 		}
 #endif
 	      if (binding_add (run, index, goal.run, goal.index))
 		{
-		  flag = (flag
-			  && termMguInTerm (goal.rd->message, rd->message,
-					    mgu_iterate));
+		  {
+		    flag = (flag
+			    && termMguInTerm (goal.rd->message, rd->message,
+					      mgu_iterate));
+		  }
 		}
 	      else
 		{
@@ -367,13 +373,13 @@ bind_existing_run (const Goal goal, const Protocol p, const Role r,
 //! Bind a goal to a new run
 int
 bind_new_run (const Goal goal, const Protocol p, const Role r,
-	      const int index)
+	      const int index, Termlist substlist)
 {
   int run;
   int flag;
   Roledef rd;
 
-  roleInstance (sys, p, r, NULL);
+  roleInstance (sys, p, r, NULL, substlist);
   run = sys->maxruns - 1;
   sys->runs[run].length = index + 1;
   if (binding_add (run, index, goal.run, goal.index))
@@ -386,6 +392,7 @@ bind_new_run (const Goal goal, const Protocol p, const Role r,
 	  e_term1 = r->nameterm;
 	  rd = roledef_shift (sys->runs[run].start, index);
 	  e_term2 = rd->message;
+	  e_term3 = goal.rd->message;
 	}
 #endif
 
@@ -411,12 +418,12 @@ printSemiState ()
   List bl;
 
   int binding_indent_print (void *data)
-    {
-      indentPrint ();
-      eprintf ("!! ");
-      binding_print (data);
-      return 1;
-    }
+  {
+    indentPrint ();
+    eprintf ("!! ");
+    binding_print (data);
+    return 1;
+  }
 
   indentPrint ();
   eprintf ("!! --=[ Semistate ]=--\n");
@@ -547,9 +554,9 @@ bind_goal_regular (const Goal goal)
       flag = 1;
       if (run == -2)
 	{
-	  flag = flag && bind_new_run (goal, p, r, index);
+	  flag = flag && bind_new_run (goal, p, r, index, substlist);
 	}
-      return (flag && bind_existing_run (goal, p, r, index, run));
+      return (flag && bind_existing_run (goal, p, r, index, run, 0));
     }
 
     if (p == INTRUDER)
@@ -635,9 +642,9 @@ bind_intruder_to_regular (Goal goal)
       flag = 1;
       if (run == -2)
 	{
-	  flag = flag && bind_new_run (goal, p, r, index);
+	  flag = flag && bind_new_run (goal, p, r, index, substlist);
 	}
-      flag = flag && bind_existing_run (goal, p, r, index, run);
+      flag = flag && bind_existing_run (goal, p, r, index, run, 1);
 
       /**
        * deconstruct key list goals
@@ -1030,7 +1037,7 @@ arachne ()
 	    }
 #endif
 
-	  roleInstance (sys, p, r, NULL);
+	  roleInstance (sys, p, r, NULL, NULL);
 	  sys->runs[0].length = cl->ev + 1;
 
 	  /**
diff --git a/src/compiler.c b/src/compiler.c
index fd3fbee..594652a 100644
--- a/src/compiler.c
+++ b/src/compiler.c
@@ -652,7 +652,7 @@ runInstanceCreate (Tac tc)
     }
 
   /* equal numbers, so it seems to be safe */
-  roleInstance (sys, p, r, instParams);	// technically, we don't need to do this for Arachne [fix later]
+  roleInstance (sys, p, r, instParams, NULL);	// technically, we don't need to do this for Arachne [fix later]
 
   /* after creation analysis */
   /* AC1: untrusted agents */
diff --git a/src/system.c b/src/system.c
index f71f14f..ce3186f 100644
--- a/src/system.c
+++ b/src/system.c
@@ -485,7 +485,7 @@ firstNonAgentRead (const System sys, int rid)
 
 void
 roleInstance (const System sys, const Protocol protocol, const Role role,
-	      const Termlist paramlist)
+	      const Termlist paramlist, Termlist substlist)
 {
   int rid;
   Run runs;
@@ -671,6 +671,20 @@ roleInstance (const System sys, const Protocol protocol, const Role role,
       rd->message = termLocal (rd->message, fromlist, tolist, rid);
       rd = rd->next;
     }
+
+  runs[rid].substitutions = NULL;
+  while (substlist != NULL)
+    {
+      Term t;
+
+      t = substlist->term;
+      if (t->subst != NULL)
+	{
+	  t->subst = termLocal (t->subst, fromlist, tolist, rid);
+	  runs[rid].substitutions = termlistAdd (runs[rid].substitutions, t);
+	}
+      substlist = substlist->next;
+    }
   termlistDelete (fromlist);
   runs[rid].locals = tolist;
   runs[rid].artefacts = artefacts;
@@ -700,6 +714,7 @@ roleInstanceDestroy (const System sys)
     {
       int runid;
       struct run myrun;
+      Termlist substlist;
 
       runid = sys->maxruns - 1;
       myrun = sys->runs[runid];
@@ -723,6 +738,24 @@ roleInstanceDestroy (const System sys)
 	      artefacts = artefacts->next;
 	    }
 	}
+
+      /**
+       * Undo the local copies of the substitutions. We cannot restore them however, so this might
+       * prove a problem. We assume that the substlist fixes this at roleInstance time; it should be exact.
+       */
+      substlist = myrun.substitutions;
+      while (substlist != NULL)
+	{
+	  Term t;
+
+	  t = substlist->term;
+	  if (t->subst != NULL)
+	    {
+	      termDelete (t->subst);
+	      t->subst = NULL;
+	    }
+	  substlist = substlist->next;
+	}
       termlistDelete (myrun.artefacts);
       termlistDelete (myrun.locals);
       termlistDelete (myrun.agents);
diff --git a/src/system.h b/src/system.h
index cf4b3fc..49a728b 100644
--- a/src/system.h
+++ b/src/system.h
@@ -49,6 +49,7 @@ struct run
   Knowledge know;		//!< Current knowledge of the run.
   Termlist locals;		//!< Locals of the run.
   Termlist artefacts;		//!< Stuff created especially for this run.
+  Termlist substitutions;	//!< The substitutions as they came from the roledef unifier
   int prevSymmRun;		//!< Used for symmetry reduction. Either -1, or the previous run with the same role def and at least a single parameter.
   int firstNonAgentRead;	//!< Used for symmetry reductions for equal agents runs; -1 if there is no candidate.
   int firstReal;		//!< 1 if a choose was inserted, otherwise 0
@@ -214,7 +215,7 @@ void runsPrint (const System sys);
 Term agentOfRunRole (const System sys, const int run, const Term role);
 Term agentOfRun (const System sys, const int run);
 void roleInstance (const System sys, const Protocol protocol, const Role role,
-		   const Termlist tolist);
+		   const Termlist paramlist, Termlist substlist);
 void roleInstanceDestroy (const System sys);
 void systemStart (const System sys);
 void indentActivate ();