- Seems to work again, but further testing is needed.

src/arachne.c

@@ -164,18 +164,30 @@ arachneDone ()
 void
 indentPrefixPrint (const int annotate, const int jumps)
 {
+  void counterPrint ()
+  {
+    if (switches.engine == ARACHNE_ENGINE)
+      {
+	statesFormat (sys->current_claim->states);
+	eprintf ("\t");
+      }
+    eprintf ("%i", annotate);
+    eprintf ("\t");
+  }
+
   if (switches.output == ATTACK && globalError == 0)
     {
       // Arachne, attack, not an error
       // We assume that means DOT output
-      eprintf ("// %i\t", annotate);
+      eprintf ("// ");
+      counterPrint ();
     }
   else
     {
       // If it is not to stdout, or it is not an attack...
       int i;
 
-      eprintf ("%i\t", annotate);
+      counterPrint ();
       for (i = 0; i < jumps; i++)
 	{
 	  if (i % 3 == 0)
@@ -763,6 +775,25 @@ getPriorityOfNeededKey (const System sys, const Term keyneeded)
   return prioritylevel;
 }
 
+//! Report failed binding
+void
+report_failed_binding (Binding b, int run, int index)
+{
+  if (switches.output == PROOF)
+    {
+      indentPrint ();
+      eprintf ("Failed to bind the binding at r%ii%i with term ", b->run_to,
+	       b->ev_to);
+      termPrint (b->term);
+      eprintf (" to the source r%ii%i because of orderings.\n", run, index);
+#ifdef DEBUG
+      if (DEBUGL (5))
+	{
+	  dependPrint ();
+	}
+#endif
+    }
+}
 
 //! Make a decryption chain from a binding to some run,index using the key list, and callback if this works.
 /**
@@ -781,6 +812,10 @@ createDecryptionChain (const Binding b, const int run, const int index,
 	  goal_unbind (b);
 	  return;
 	}
+      else
+	{
+	  report_failed_binding (b, run, index);
+	}
     }
   else
     {
@@ -858,6 +893,10 @@ createDecryptionChain (const Binding b, const int run, const int index,
 	    createDecryptionChain (bnew, run, index, keylist->next, callback);
 	    goal_unbind (b);
 	  }
+	else
+	  {
+	    report_failed_binding (b, smallrun, 2);
+	  }
 	/*
 	 * clean up
 	 */
@@ -908,17 +947,31 @@ bind_existing_to_goal (const Binding b, const int run, const int index)
 	  {
 	    int neworders;
 	    int allgood;
+	    Term tvar;
 
 	    // the idea is, that a substitution in run x with
 	    // something containing should be wrapped; this
 	    // occurs for all subterms of other runs.
-	    int makeDepend (Term t)
+	    int makeDepend (Term tsmall)
 	    {
-	      int r1, e1;
+	      Term tsubst;
 
-	      r1 = TermRunid (t);
-	      e1 = firstOccurrence (sys, r1, t, SEND);
-	      if (dependPushEvent (r1, e1, run, index))
+	      tsubst = deVar (tsmall);
+	      if (!realTermVariable (tsubst))
+		{
+		  // Only for non-variables (i.e. local constants)
+		  int r1, e1, r2, e2;
+
+		  r1 = TermRunid (tsubst);
+		  e1 = firstOccurrence (sys, r1, tsubst, SEND);
+		  if (e1 >= 0)
+		    {
+		      r2 = TermRunid (tvar);
+		      e2 = firstOccurrence (sys, r2, tsubst, READ);
+		      if (e2 >= 0)
+			{
+
+			  if (dependPushEvent (r1, e1, r2, e2))
 			    {
 			      neworders++;
 			      return true;
@@ -926,14 +979,27 @@ bind_existing_to_goal (const Binding b, const int run, const int index)
 			  else
 			    {
 			      allgood = false;
+			      if (switches.output == PROOF)
+				{
+				  indentPrint ();
+				  eprintf ("Substitution for ");
+				  termSubstPrint (sl->term);
+				  eprintf (" (subterm ");
+				  termPrint (tsmall);
+				  eprintf (") could not be safely bound.\n");
+				}
 			      return false;
 			    }
 			}
+		    }
+		}
+	      return true;
+	    }
 
 	    neworders = 0;
 	    allgood = true;
-	    iterateTermOther (run, sl->term, makeDepend);
-
+	    tvar = sl->term;
+	    iterateTermOther (run, tvar, makeDepend);
 	    if (allgood)
 	      {
 		wrapSubst (sl->next);

src/binding.c

@@ -230,25 +230,28 @@ goal_add (Term term, const int run, const int ev, const int level)
   else
     {
       // Determine whether we already had it
-      int nope;
+      int createnew;
 
       int testSame (void *data)
       {
 	Binding b;
 
 	b = (Binding) data;
-	if (isTermEqual (b->term, term) && run == b->run_to && ev == b->ev_to)
-	  {			// abort scan, report
-	    return false;
+	if (isTermEqual (b->term, term))
+	  {
+	    // binding of same term
+	    if (run == b->run_to && ev == b->ev_to)
+	      {
+		// identical binding 
+		createnew = false;
+	      }
 	  }
-	else
-	  {			// proceed with scan
 	return true;
       }
-      }
 
-      nope = list_iterate (sys->bindings, testSame);
-      if (nope)
+      createnew = true;
+      list_iterate (sys->bindings, testSame);
+      if (createnew)
 	{
 	  // Add a new binding
 	  Binding b;
@@ -436,5 +439,66 @@ unique_origination ()
 int
 bindings_c_minimal ()
 {
-  return unique_origination ();
+  if (!unique_origination ())
+    {
+      return false;
+    }
+
+  {
+    List bl;
+
+    // For all goals
+    bl = sys->bindings;
+    while (bl != NULL)
+      {
+	Binding b;
+
+	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))
+	  {
+	    int run;
+	    int node_from;
+
+	    // Find all preceding events
+	    for (run = 0; run < sys->maxruns; run++)
+	      {
+		int ev;
+
+		//!@todo hardcoded reference to step, should be length
+		for (ev = 0; ev < sys->runs[run].step; ev++)
+		  {
+		    if (isDependEvent (run, ev, b->run_from, b->ev_from))
+		      {
+			// this node is *before* the from node
+			Roledef rd;
+
+			rd = roledef_shift (sys->runs[run].start, ev);
+			if (termInTerm (rd->message, b->term))
+			  {
+			    // This term already occurs as interm in a previous node!
+#ifdef DEBUG
+			    if (DEBUGL (4))
+			      {
+				// Report this
+				indentPrint ();
+				eprintf ("Binding for ");
+				termPrint (b->term);
+				eprintf
+				  (" at r%i i%i is not c-minimal because it occurred before at r%i i%i in ",
+				   b->run_from, b->ev_from, run, ev);
+				termPrint (rd->message);
+				eprintf ("\n");
+			      }
+#endif
+			    return false;
+			  }
+		      }
+		  }
+	      }
+	  }
+	bl = bl->next;
+      }
+  }
+  return true;
 }

src/compiler.c

@@ -1420,6 +1420,11 @@ compute_prec_sets (const System sys)
 	  ev1++;
 	  rd = rd->next;
 	}
+      while (ev1 < sys->roleeventmax)
+	{
+	  eventlabels[index (r1, ev1)] = NULL;
+	  ev1++;
+	}
       //eprintf ("\n");
       r1++;
     }
@@ -1517,6 +1522,7 @@ compute_prec_sets (const System sys)
 	}
       while (r1 < sys->rolecount
 	     && !isTermEqual (label, eventlabels[index (r1, ev1)]));
+
       if (r1 == sys->rolecount)
 	{
 	  error

src/depend.c

@@ -98,6 +98,7 @@ dependPrint ()
     r1 = 0;
     o1 = 0;
     eprintf ("Printing dependency graph.\n");
+    eprintf ("Y axis nodes comes before X axis node.\n");
     for (n1 = 0; n1 < nodeCount (); n1++)
       {
 	int n2;

src/prune_theorems.c

@@ -47,7 +47,7 @@ correctLocalOrder (const System sys)
 		{
 		  indentPrint ();
 		  eprintf ("Pruned because ordering for term ");
-		  termPrint (t);
+		  termSubstPrint (t);
 		  eprintf
 		    (" cannot be correct: the first send r%ii%i occurs after the read r%ii%i.\n",
 		     r2, e2, r1, e1);
@@ -282,7 +282,10 @@ prune_theorems (const System sys)
   /*
    * Check for correct orderings involving local constants
    */
+  if (switches.experimental & 8 != 0)
+    {
       correctLocalOrder (sys);
+    }
 
   /**
    * Check whether the bindings are valid

src/switches.c

@@ -942,8 +942,6 @@ switcher (const int process, int index, int commandline)
       else
 	{
 	  switches.experimental = integer_argument ();
-	  eprintf ("Set experimental switch to %i.\n", switches.experimental);
-	  eprintf ("And 4 mask: %i.\n", switches.experimental & 4);
 	  return index;
 	}
     }

src/system.c

@@ -1595,7 +1595,7 @@ iterateEventsType (const System sys, const int run, const int evtype,
 // Iterate over all 'others': local variables of a run that are instantiated and contain some term of another run.
 int
 iterateLocalToOther (const System sys, const int myrun,
-		     int (*callback) (Term t))
+		     int (*callback) (Term tlocal))
 {
   Termlist tlo, tls;
 
@@ -1642,14 +1642,23 @@ firstOccurrence (const System sys, const int r, Term t, int evtype)
     return true;
   }
 
-  if (iterateEventsType (sys, r, evtype, checkOccurs))
+  firste = -1;
+  iterateEventsType (sys, r, evtype, checkOccurs);
+#ifdef DEBUG
+  if (DEBUGL (3))
+    {
+      if (firste == -1)
 	{
 	  globalError++;
-      eprintf ("Desired term ");
+	  eprintf ("Warning: Desired term ");
 	  termPrint (t);
-      eprintf (" does not occur.\n");
+	  eprintf (" does not occur");
+	  eprintf (" in run %i in event type %i.\n", r, evtype);
+	  runPrint (sys->runs[r].start);
+	  eprintf ("\n");
 	  globalError--;
-      error ("(in run %i in event type %i.)", r, evtype);
 	}
+    }
+#endif
   return firste;
 }

src/term.c

@@ -1428,6 +1428,27 @@ termHidelevel (const Term tsmall, Term tbig)
     }
 }
 
+//! Show a substitution of t
+void
+termSubstPrint (Term t)
+{
+  if (realTermVariable (t))
+    {
+      Term tbuf;
+
+      tbuf = t->subst;
+      t->subst = NULL;
+      termPrint (t);
+      t->subst = tbuf;
+      eprintf (":=");
+      termSubstPrint (t->subst);
+    }
+  else
+    {
+      termPrint (t);
+    }
+}
+
 // Iterate over subterm constants of other runs in a term
 // Callback should return true to progress. This is reported in the final thing.
 int

src/term.h

@@ -204,6 +204,7 @@ Term freshTermPrefix (Term prefixterm);
 int isTermFunctionName (Term t);
 Term getTermFunction (Term t);
 unsigned int termHidelevel (const Term tsmall, Term tbig);
+void termSubstPrint (Term t);
 
 int iterateTermOther (const int myrun, Term t, int (*callback) (Term t));