- Fixed the very annoying bug! The problem was in roleInstance for

Arachne. When a subst was carried out by an Rolename->compoundTerm
  substitution, the compound term was not duplicated, and this caused
  problems at roledef destruction.

src/arachne.c

@@ -278,10 +278,11 @@ bind_new_run (const Goal goal, const Protocol p, const Role r,
   e_term2 = rd->message;
 #endif
 
-  iterate ();
+  flag = iterate ();
 
   goal.rd->bind_run = old_run;
   goal.rd->bind_index = old_index;
+
   roleInstanceDestroy (sys);
   return flag;
 }

src/mgu.c

@@ -208,46 +208,49 @@ termMguSubTerm (Term t1, Term t2, int (*iterator) (),
 
   flag = 1;
   t2 = deVar (t2);
-  if (t2 != NULL && !isTermLeaf (t2))
+  if (t2 != NULL)
     {
-      if (isTermTuple (t2))
+      if (!isTermLeaf (t2))
 	{
-	  // 'simple' tuple
+	  if (isTermTuple (t2))
-	  flag =
+	    {
-	    flag && termMguSubTerm (t1, t2->left.op1, iterator, inverses,
+	      // 'simple' tuple
-				   keylist);
+	      flag =
-	  flag =
+		flag && termMguSubTerm (t1, t2->left.op1, iterator, inverses,
-	    flag && termMguSubTerm (t1, t2->right.op2, iterator, inverses,
+					keylist);
-				   keylist);
+	      flag =
+		flag && termMguSubTerm (t1, t2->right.op2, iterator, inverses,
+					keylist);
+	    }
+	  else
+	    {
+	      // Must be encryption
+	      // So, we need the key, and try to get the rest
+	      Termlist keylist_new;
+	      Term newkey;
+
+	      keylist_new = termlistShallow (keylist);
+	      newkey = inverseKey (inverses, t2->right.key);
+	      keylist_new = termlistAdd (keylist_new, newkey);
+
+	      // Recurse
+	      flag =
+		flag && termMguSubTerm (t1, t2->left.op, iterator, inverses,
+					keylist_new);
+
+	      termlistDelete (keylist_new);
+	      termDelete (newkey);
+	    }
 	}
-      else
+      // simple clause or combined
+      tl = termMguTerm (t1, t2);
+      if (tl != MGUFAIL)
 	{
-	  // Must be encryption
+	  // Iterate
-	  // So, we need the key, and try to get the rest
+	  flag = flag && iterator (tl, keylist);
-	  Termlist keylist_new;
+	  // Reset variables
-	  Term newkey;
+	  termlistSubstReset (tl);
-
-	  keylist_new = termlistShallow (keylist);
-	  newkey = inverseKey (inverses, t2->right.key);
-	  keylist_new = termlistAdd (keylist_new, newkey);
-
-	  // Recurse
-	  flag =
-	    flag && termMguSubTerm (t1, t2->left.op, iterator, inverses,
-				    keylist_new);
-
-	  termlistDelete (keylist_new);
-	  termDelete (newkey);
 	}
     }
-  // simple clause or combined
-  tl = termMguTerm (t1, t2);
-  if (tl != MGUFAIL)
-    {
-      // Iterate
-      flag = flag && iterator (tl, keylist);
-      // Reset variables
-      termlistSubstReset (tl);
-    }
   return flag;
 }

src/system.c

@@ -591,11 +591,12 @@ roleInstance (const System sys, const Protocol protocol, const Role role,
 	  Term newt, oldt;
 
 	  oldt = scanfrom->term;
-	  newt = deVar (oldt);
+	  newt = oldt;
 	  if (realTermVariable (newt))
 	    {
 	      // Make new var for this run
 	      newt = makeTermType (VARIABLE, newt->left.symb, rid);
+	      newt->subst = oldt->subst;
 	      artefacts = termlistAdd (artefacts, newt);
 	    }
 	  // Add to agent list, possibly
@@ -689,13 +690,12 @@ roleInstance (const System sys, const Protocol protocol, const Role role,
 void
 roleInstanceDestroy (const System sys)
 {
-  int runid;
+  if (sys->maxruns > 0)
-
-  runid = sys->maxruns - 1;
-  if (runid >= 0)
     {
+      int runid;
       struct run myrun;
 
+      runid = sys->maxruns - 1;
       myrun = sys->runs[runid];
 
       // Destroy roledef