- MakeTraceConcrete now yields nicer choices, e.g. "Agent1" or "Nonce2".

src/arachne.c

@@ -1706,7 +1706,7 @@ createNewTermGeneric (Termlist tl, Term t)
   Term newterm;
 
   /* Determine first free number */
-  freenumber = 0;
+  freenumber = sys->maxruns;
   tlscan = tl;
   while (tlscan != NULL)
     {
@@ -1832,6 +1832,8 @@ deleteNewTerm (Term t)
  * People find reading variables in attack outputs difficult.
  * Thus, we instantiate them in a sensible way to make things more readable.
  *
+ * This happens after sys->maxruns is fixed. Intruder constants thus are numbered from sys->maxruns onwards.
+ *
  * \sa makeTraceClass
  */
 Termlist

src/dotout.c

@@ -67,6 +67,9 @@ printVisualRun (int rid)
   int displayr;
   int display;
 
+  if (rid < sys->maxruns)
+    {
+      // < sys->maxruns means normal thing (not from makeTraceConcrete)
       displayi = 0;
       displayr = 0;
       for (run = 0; run < rid; run++)
@@ -90,6 +93,12 @@ printVisualRun (int rid)
 	}
       eprintf ("#%i", display);
     }
+  else
+    {
+      // >= sys->maxruns means intruder choice
+      eprintf ("%i", (rid - sys->maxruns + 1));
+    }
+}
 
 //! Remap term stuff
 void