diff --git a/src/arachne.c b/src/arachne.c
index f5ed91f..d90bfec 100644
--- a/src/arachne.c
+++ b/src/arachne.c
@@ -400,7 +400,7 @@ add_read_goals (const int run, const int old, const int new)
 
       sys->runs[run].height = new;
       i = old;
-      rd = roledef_shift (sys->runs[run].start, i);
+      rd = eventRoledef (sys, run, i);
       count = 0;
       while (i < new && rd != NULL)
 	{
@@ -432,54 +432,6 @@ add_read_goals (const int run, const int old, const int new)
     }
 }
 
-//! Determine the run that follows from a substitution.
-/**
- * After an Arachne unification, stuff might go wrong w.r.t. nonce instantiation.
- * This function determines the run that is implied by a substitution list.
- * @returns >= 0: a run, -1 for invalid, -2 for any run.
- */
-int
-determine_unification_run (Termlist tl)
-{
-  int run;
-
-  run = -2;
-  while (tl != NULL)
-    {
-      //! Again, hardcoded reference to compiler.c. Level -3 means a local constant for a role.
-      if (tl->term->type != VARIABLE && TermRunid (tl->term) == -3)
-	{
-	  Term t;
-
-	  t = tl->term->subst;
-
-	  // It is required that it is actually a leaf, because we construct it.
-	  if (!realTermLeaf (t))
-	    {
-	      return -1;
-	    }
-	  else
-	    {
-	      if (run == -2)
-		{
-		  // Any run
-		  run = TermRunid (t);
-		}
-	      else
-		{
-		  // Specific run: compare
-		  if (run != TermRunid (t))
-		    {
-		      return -1;
-		    }
-		}
-	    }
-	}
-      tl = tl->next;
-    }
-  return run;
-}
-
 //! Determine trace length
 int
 get_semitrace_length ()
@@ -1915,9 +1867,11 @@ makeTraceClass (const System sys, Termlist varlist)
       Term var;
 
       var = tl->term;
-      deleteNewTerm (var->subst);
-      var->subst = NULL;
-
+      if (realTermVariable (var))
+	{
+	  deleteNewTerm (var->subst);
+	  var->subst = NULL;
+	}
       tl = tl->next;
     }
   termlistDelete (varlist);
@@ -2067,34 +2021,39 @@ iterate ()
 		{
 		  /* Substitution or something resulted in a tuple goal: we immediately split them into compounds.
 		   */
-		  int count;
-		  Term tupletermbuffer;
+		  Term tuple;
 
-		  tupletermbuffer = btup->term;
-
-		  /*
-		   * We solve this by replacing the tuple goal by the left term, and adding a goal for the right term.
-		   */
-		  btup->term = TermOp1 (tupletermbuffer);
-		  count =
-		    goal_add (TermOp2 (tupletermbuffer), btup->run_to,
-			      btup->ev_to, btup->level);
-
-		  // Show this in output
-		  if (switches.output == PROOF)
+		  tuple = deVar (btup->term);
+		  if (realTermTuple (tuple))
 		    {
-		      indentPrint ();
-		      eprintf ("Expanding tuple goal ");
-		      termPrint (tupletermbuffer);
-		      eprintf (" into %i subgoals.\n", count);
+		      int count;
+		      Term tupletermbuffer;
+
+		      tupletermbuffer = btup->term;
+		      /*
+		       * We solve this by replacing the tuple goal by the left term, and adding a goal for the right term.
+		       */
+		      btup->term = TermOp1 (tuple);
+		      count =
+			goal_add (TermOp2 (tuple), btup->run_to,
+				  btup->ev_to, btup->level);
+
+		      // Show this in output
+		      if (switches.output == PROOF)
+			{
+			  indentPrint ();
+			  eprintf ("Expanding tuple goal ");
+			  termPrint (tupletermbuffer);
+			  eprintf (" into %i subgoals.\n", count);
+			}
+
+		      // iterate
+		      flag = iterate ();
+
+		      // undo
+		      goal_remove_last (count);
+		      btup->term = tupletermbuffer;
 		    }
-
-		  // iterate
-		  flag = iterate ();
-
-		  // undo
-		  goal_remove_last (count);
-		  btup->term = tupletermbuffer;
 		}
 	      else
 		{
diff --git a/src/binding.c b/src/binding.c
index 5509c41..6b3be70 100644
--- a/src/binding.c
+++ b/src/binding.c
@@ -220,7 +220,14 @@ goal_add (Term term, const int run, const int ev, const int level)
   term = deVar (term);
 #ifdef DEBUG
   if (term == NULL)
-    error ("Trying to add an emtpy goal term");
+    {
+      globalError++;
+      roledefPrint (eventRoledef (sys, run, ev));
+      eprintf ("\n");
+      globalError--;
+      error ("Trying to add an emtpy goal term to r%ii%i, with level %i.",
+	     run, ev, level);
+    }
   if (run >= sys->maxruns)
     error ("Trying to add a goal for a run that does not exist.");
   if (ev >= sys->runs[run].step)
diff --git a/src/system.c b/src/system.c
index 1f0f0e9..32f5a67 100644
--- a/src/system.c
+++ b/src/system.c
@@ -234,6 +234,9 @@ ensureValidRun (const System sys, int run)
       myrun.index = NULL;
       myrun.start = NULL;
 
+      myrun.rho = NULL;
+      myrun.sigma = NULL;
+      myrun.constants = NULL;
       myrun.locals = NULL;
       myrun.artefacts = NULL;
       myrun.substitutions = NULL;
@@ -589,6 +592,9 @@ roleInstanceArachne (const System sys, const Protocol protocol,
   Termlist fromlist = NULL;	// deleted at the end
   Termlist tolist = NULL;	// -> .locals
   Termlist artefacts = NULL;	// -> .artefacts
+  Termlist rho = NULL;		// -> .rho
+  Termlist sigma = NULL;	// -> .sigma
+  Termlist constants = NULL;	// -> .constants
   Term extterm = NULL;		// construction thing (will go to artefacts)
 
   /* claim runid, allocate space */
diff --git a/src/system.h b/src/system.h
index ef6645a..92e3f9d 100644
--- a/src/system.h
+++ b/src/system.h
@@ -47,7 +47,10 @@ struct run
   Roledef index;		//!< Current execution point in the run (roledef pointer)
   Roledef start;		//!< Head of the run definition.
   Knowledge know;		//!< Current knowledge of the run.
-  Termlist locals;		//!< Locals of the run.
+  Termlist rho;			//!< As in semantics (copies in artefacts)
+  Termlist sigma;		//!< As in semantics (copies in artefacts)
+  Termlist constants;		//!< As in semantics (copies in artefacts)
+  Termlist locals;		//!< Locals of the run (will be deprecated eventually)
   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.