- Matching method propagation was wrong in new switch code.

- Some fixes for protocols that do not include matching send/read
  combo's. In particular, the max encryption level method ranged over
  the sends; now over all events. Maybe it can range over read events
  only?

src/arachne.c

@@ -562,13 +562,13 @@ proof_suppose_binding (Binding b)
 // Sub
 //------------------------------------------------------------------------
 
-//! Iterate over all send types in the roles (including the intruder ones)
+//! Iterate over all events in the roles (including the intruder ones)
 /**
  * Function is called with (protocol pointer, role pointer, roledef pointer, index)
  * and returns an integer. If it is false, iteration aborts.
  */
 int
-iterate_role_sends (int (*func) ())
+iterate_role_events (int (*func) ())
 {
   Protocol p;
 
@@ -586,12 +586,9 @@ iterate_role_sends (int (*func) ())
 	  rd = r->roledef;
 	  index = 0;
 	  while (rd != NULL)
-	    {
-	      if (rd->type == SEND)
 	    {
 	      if (!func (p, r, rd, index))
 		return 0;
-		}
 	      index++;
 	      rd = rd->next;
 	    }
@@ -602,6 +599,29 @@ iterate_role_sends (int (*func) ())
   return 1;
 }
 
+//! Iterate over all send types in the roles (including the intruder ones)
+/**
+ * Function is called with (protocol pointer, role pointer, roledef pointer, index)
+ * and returns an integer. If it is false, iteration aborts.
+ */
+int
+iterate_role_sends (int (*func) ())
+{
+  int send_wrapper (Protocol p, Role r, Roledef rd, int i)
+    {
+      if (rd->type == SEND)
+	{
+	  return func (p,r,rd,i);
+	}
+      else
+	{
+	  return 1;
+	}
+    }
+
+  return iterate_role_events (send_wrapper);
+}
+
 //! Try to bind a specific existing run to a goal.
 /**
  * The key goals are bound to the goal.
@@ -2971,6 +2991,14 @@ arachne ()
     int tlevel;
 	
     tlevel = term_encryption_level (rd->message);
+#ifdef DEBUG
+    if (DEBUGL(3))
+      {
+	eprintf ("Encryption level %i found for term ", tlevel);
+	termPrint (rd->message);
+	eprintf ("\n");
+      }
+#endif
     if (tlevel > max_encryption_level)
       max_encryption_level = tlevel;
     return 1;
@@ -2995,18 +3023,16 @@ arachne ()
   num_intruder_runs = 0;
 
   max_encryption_level = 0;
-  iterate_role_sends (determine_encrypt_max);
+  iterate_role_events (determine_encrypt_max);
-
-  fixAgentKeylevels ();
-
 #ifdef DEBUG
   if (DEBUGL (1))
     {
       eprintf ("Maximum encryption level: %i\n", max_encryption_level);
-      iterate_role_sends (print_send);
     }
 #endif
 
+  fixAgentKeylevels ();
+
   indentDepth = 0;
   proofDepth = 0;
   cl = sys->claimlist;

src/switches.c

@@ -12,10 +12,10 @@
 #include "timer.h"
 
 extern System sys;
+extern int mgu_match;
 
 extern struct tacnode *spdltac;
 extern Term TERM_Claim;
-extern int mgu_match;
 
 const char *progname = "scyther";
 const char *releasetag = SVNVERSION;
@@ -219,6 +219,7 @@ switcher (const int process, const System sys, int index)
       else
 	{
 	  sys->match = integer_argument ();
+	  mgu_match = sys->match;
 	  return index;
 	}
     }

src/term.c

@@ -1079,21 +1079,33 @@ term_rolelocals_are_variables ()
 int
 term_encryption_level (const Term term)
 {
-  int iter_maxencrypt (Term term)
+  int iter_maxencrypt (Term t)
   {
-    term = deVar (term);
+    t = deVar (t);
-    if (realTermLeaf (term))
+    if (t == NULL)
+      {
+#ifdef DEBUG
+	if (DEBUGL(2))
+	  {
+	    eprintf ("Warning: Term encryption level finds a NULL for term ");
+	    termPrint (term);
+	    eprintf ("\n");
+	  }
+#endif
+	return 0;
+      }
+    if (realTermLeaf (t))
       {
 	return 0;
       }
     else
       {
-	if (realTermTuple (term))
+	if (realTermTuple (t))
 	  {
 	    int l, r;
 
-	    l = iter_maxencrypt (TermOp1 (term));
+	    l = iter_maxencrypt (TermOp1 (t));
-	    r = iter_maxencrypt (TermOp2 (term));
+	    r = iter_maxencrypt (TermOp2 (t));
 	    if (l > r)
 	      return l;
 	    else
@@ -1102,7 +1114,7 @@ term_encryption_level (const Term term)
 	else
 	  {
 	    // encrypt
-	    return 1 + iter_maxencrypt (TermOp (term));
+	    return 1 + iter_maxencrypt (TermOp (t));
 	  }
       }
   }

src/termlist.c

@@ -109,19 +109,17 @@ termlistDestroy (Termlist tl)
 
 //! Determine whether a term is an element of a termlist.
 /**
- * Term must be non-null.
+ * The NULL term is not an element of any list. (Not even of the NULL list)
  *
  *@return True iff the term is an element of the termlist.
  */
 __inline__ int
 inTermlist (Termlist tl, const Term term)
 {
-#ifdef DEBUG
   if (term == NULL)
     {
-      error ("Trying to do inTermlist for a NULL term.");
+      return 0;
     }
-#endif
   while (tl != NULL)
     {
       if (isTermEqual (tl->term, term))