diff --git a/src/attackminimize.c b/src/attackminimize.c
index 79cbb1e..7be51af 100644
--- a/src/attackminimize.c
+++ b/src/attackminimize.c
@@ -14,127 +14,129 @@ int cTod = 0;
  *@param tb The attack buffer.
  *@param ev The reference event index.
  */
-void markback(const System sys, struct tracebuf *tb, int ev)
+void
+markback (const System sys, struct tracebuf *tb, int ev)
 {
-	int run = tb->run[ev];
+  int run = tb->run[ev];
 
-	while (ev >= 0)
+  while (ev >= 0)
+    {
+      if (tb->run[ev] == run)
 	{
-		if (tb->run[ev] == run)
+	  switch (tb->event[ev]->type)
+	    {
+	    case READ:
+	      switch (tb->status[ev])
 		{
-			switch (tb->event[ev]->type)
-			{
-				case READ:
-					switch (tb->status[ev])
-					{
-						case S_UNK:
-							cUnk--;
-						case S_RED:
-							tb->status[ev] = S_TOD;
-							cTod++;
-							break;
-						case S_TOD:
-						case S_OKE:
-							break;
-					}
-					break;
-				case SEND:
-				case CLAIM:
-					if (tb->status[ev] == S_UNK)
-					{
-					    cUnk--;
-					}
-					tb->status[ev] = S_OKE;
-					break;
-			}
+		case S_UNK:
+		  cUnk--;
+		case S_RED:
+		  tb->status[ev] = S_TOD;
+		  cTod++;
+		  break;
+		case S_TOD:
+		case S_OKE:
+		  break;
 		}
-		ev--;
+	      break;
+	    case SEND:
+	    case CLAIM:
+	      if (tb->status[ev] == S_UNK)
+		{
+		  cUnk--;
+		}
+	      tb->status[ev] = S_OKE;
+	      break;
+	    }
 	}
+      ev--;
+    }
 }
 
 //! Minimize the attack.
-void attackMinimize(const System sys, struct tracebuf *tb)
+void
+attackMinimize (const System sys, struct tracebuf *tb)
 {
-	int i;
-	int j;
+  int i;
+  int j;
 
-	cUnk = 0;
-	cTod = 0;
+  cUnk = 0;
+  cTod = 0;
 
-	for (i=0; i < tb->length; i++)
+  for (i = 0; i < tb->length; i++)
+    {
+      switch (tb->status[i])
 	{
-		switch (tb->status[i])
-		{
-		case S_UNK:
-		    cUnk++;
-		    break;
-		case S_TOD:
-		    cTod++;
-		    break;
-		default:
-		    break;
-		}
+	case S_UNK:
+	  cUnk++;
+	  break;
+	case S_TOD:
+	  cTod++;
+	  break;
+	default:
+	  break;
 	}
-	
-	markback(sys, tb, tb->violatedclaim);
+    }
 
-	while (cUnk + cTod > 0)
+  markback (sys, tb, tb->violatedclaim);
+
+  while (cUnk + cTod > 0)
+    {
+      while (cTod > 0)
 	{
-		while (cTod > 0)
-		{
-			for (i = 0; i < tb->length; i++)
-				// kies een i; laten we de eerste maar pakken
-			{
-				if (tb->status[i] == S_TOD)
-					break;
-			}
-			if (i == tb->length)
-			  {
-			        printf("Some step error.\n");
-				exit(1);
-			  }
-			
-			j = i;
-			while (j >= 0 && inKnowledge(tb->know[j], tb->event[i]->message))
-			{
-			    // zoek waar m in de kennis komt
-			    j--;
-			}
-			tb->status[i] = S_OKE;
-			cTod--;
-			if (j>=0)
-			{
-			    markback(sys,tb,j);
-			}
-		}
-		while (cTod == 0 && cUnk > 0)
-		{
-			for (i = tb->length-1; i>=0; i--)
-				// pak laatste i
-			{
-				if (tb->status[i] == S_UNK)
-					break;
-			}
-			if (i < 0)
-			  {
-			        printf("Some i<0 error.\n");
-				exit(1);
-			  }
-			
-			tb->status[i] = S_RED;
-			cUnk--;
-			tb->reallength--;
+	  for (i = 0; i < tb->length; i++)
+	    // kies een i; laten we de eerste maar pakken
+	    {
+	      if (tb->status[i] == S_TOD)
+		break;
+	    }
+	  if (i == tb->length)
+	    {
+	      printf ("Some step error.\n");
+	      exit (1);
+	    }
 
-			j = tracebufRebuildKnow(tb);
-			if (j>-1)
-			{
-			  	tb->reallength++;
-				markback(sys,tb,i);
-				if (j < tb->length)
-				{
-					tb->link[j] = (tb->link[j] > i ? tb->link[j] : i);
-				}
-			}
-		}
+	  j = i;
+	  while (j >= 0 && inKnowledge (tb->know[j], tb->event[i]->message))
+	    {
+	      // zoek waar m in de kennis komt
+	      j--;
+	    }
+	  tb->status[i] = S_OKE;
+	  cTod--;
+	  if (j >= 0)
+	    {
+	      markback (sys, tb, j);
+	    }
 	}
+      while (cTod == 0 && cUnk > 0)
+	{
+	  for (i = tb->length - 1; i >= 0; i--)
+	    // pak laatste i
+	    {
+	      if (tb->status[i] == S_UNK)
+		break;
+	    }
+	  if (i < 0)
+	    {
+	      printf ("Some i<0 error.\n");
+	      exit (1);
+	    }
+
+	  tb->status[i] = S_RED;
+	  cUnk--;
+	  tb->reallength--;
+
+	  j = tracebufRebuildKnow (tb);
+	  if (j > -1)
+	    {
+	      tb->reallength++;
+	      markback (sys, tb, i);
+	      if (j < tb->length)
+		{
+		  tb->link[j] = (tb->link[j] > i ? tb->link[j] : i);
+		}
+	    }
+	}
+    }
 }
diff --git a/src/attackminimize.h b/src/attackminimize.h
index efca999..79fa64a 100644
--- a/src/attackminimize.h
+++ b/src/attackminimize.h
@@ -1 +1 @@
-void attackMinimize(const System sys, struct tracebuf *tb);
+void attackMinimize (const System sys, struct tracebuf *tb);
diff --git a/src/claim.c b/src/claim.c
index c000d5c..3b509b5 100644
--- a/src/claim.c
+++ b/src/claim.c
@@ -20,7 +20,8 @@
 #ifdef OKIDEBUG
 int indac = 0;
 
-void indact ()
+void
+indact ()
 {
   int i;
 
@@ -44,26 +45,25 @@ events_match (const System sys, const int i, const int j)
 
   rdi = sys->traceEvent[i];
   rdj = sys->traceEvent[j];
-  if (isTermEqual (rdi->message, rdj->message) && 
-      isTermEqual (rdi->from,    rdj->from) &&
-      isTermEqual (rdi->to,      rdj->to) && 
-      isTermEqual (rdi->label,   rdj->label) &&
-      !(rdi->internal || rdj->internal)
-      )
+  if (isTermEqual (rdi->message, rdj->message) &&
+      isTermEqual (rdi->from, rdj->from) &&
+      isTermEqual (rdi->to, rdj->to) &&
+      isTermEqual (rdi->label, rdj->label) &&
+      !(rdi->internal || rdj->internal))
     {
       if (rdi->type == SEND && rdj->type == READ)
 	{
-	  if (i<j)
-	      return MATCH_ORDER;
+	  if (i < j)
+	    return MATCH_ORDER;
 	  else
-	      return MATCH_REVERSE;
+	    return MATCH_REVERSE;
 	}
       if (rdi->type == READ && rdj->type == SEND)
 	{
-	  if (i>j)
-	      return MATCH_ORDER;
+	  if (i > j)
+	    return MATCH_ORDER;
 	  else
-	      return MATCH_REVERSE;
+	    return MATCH_REVERSE;
 	}
     }
   return MATCH_NONE;
@@ -99,7 +99,8 @@ oki_nisynch_full (const System sys, const Termmap label_to_index)
 
 //! Evaluate claims or internal reads (chooses)
 __inline__ int
-oki_nisynch_other (const System sys, const int trace_index, const Termmap role_to_run, const Termmap label_to_index)
+oki_nisynch_other (const System sys, const int trace_index,
+		   const Termmap role_to_run, const Termmap label_to_index)
 {
   int result;
 
@@ -108,7 +109,7 @@ oki_nisynch_other (const System sys, const int trace_index, const Termmap role_t
   printf ("Exploring further assuming this (claim) run is not involved.\n");
   indac++;
 #endif
-  result =  oki_nisynch (sys, trace_index-1, role_to_run, label_to_index);
+  result = oki_nisynch (sys, trace_index - 1, role_to_run, label_to_index);
 #ifdef OKIDEBUG
   indact ();
   printf (">%i<\n", result);
@@ -119,7 +120,8 @@ oki_nisynch_other (const System sys, const int trace_index, const Termmap role_t
 
 //! Evaluate reads
 __inline__ int
-oki_nisynch_read (const System sys, const int trace_index, const Termmap role_to_run, const Termmap label_to_index)
+oki_nisynch_read (const System sys, const int trace_index,
+		  const Termmap role_to_run, const Termmap label_to_index)
 {
   /*
    * Read is only relevant for already involved runs, and labels in prec
@@ -144,13 +146,16 @@ oki_nisynch_read (const System sys, const int trace_index, const Termmap role_to
 	      int result;
 
 	      label_to_index_buf = termmapDuplicate (label_to_index);
-	      label_to_index_buf = termmapSet (label_to_index_buf, rd->label, trace_index);
+	      label_to_index_buf =
+		termmapSet (label_to_index_buf, rd->label, trace_index);
 #ifdef OKIDEBUG
 	      indact ();
 	      printf ("Exploring because this (read) run is involved.\n");
 	      indac++;
 #endif
-	      result = oki_nisynch (sys, trace_index-1, role_to_run, label_to_index_buf);
+	      result =
+		oki_nisynch (sys, trace_index - 1, role_to_run,
+			     label_to_index_buf);
 #ifdef OKIDEBUG
 	      indact ();
 	      printf (">%i<\n", result);
@@ -168,7 +173,7 @@ oki_nisynch_read (const System sys, const int trace_index, const Termmap role_to
   printf ("Exploring further assuming this (read) run is not involved.\n");
   indac++;
 #endif
-  result = oki_nisynch (sys, trace_index-1, role_to_run, label_to_index);
+  result = oki_nisynch (sys, trace_index - 1, role_to_run, label_to_index);
 #ifdef OKIDEBUG
   indac--;
 #endif
@@ -178,7 +183,8 @@ oki_nisynch_read (const System sys, const int trace_index, const Termmap role_to
 
 //! Evaluate sends
 __inline__ int
-oki_nisynch_send (const System sys, const int trace_index, const Termmap role_to_run, const Termmap label_to_index)
+oki_nisynch_send (const System sys, const int trace_index,
+		  const Termmap role_to_run, const Termmap label_to_index)
 {
   Roledef rd;
   int rid;
@@ -197,14 +203,14 @@ oki_nisynch_send (const System sys, const int trace_index, const Termmap role_to
   printf ("Exploring further assuming (send) run %i is not involved.\n", rid);
   indac++;
 #endif
-  result = oki_nisynch (sys, trace_index-1, role_to_run, label_to_index);
+  result = oki_nisynch (sys, trace_index - 1, role_to_run, label_to_index);
 #ifdef OKIDEBUG
   indact ();
   printf (">%i<\n", result);
   indac--;
 #endif
   if (result)
-      return 1;
+    return 1;
 
 #ifdef OKIDEBUG
   indact ();
@@ -241,15 +247,20 @@ oki_nisynch_send (const System sys, const int trace_index, const Termmap role_to
 	      role_to_run_buf = termmapDuplicate (role_to_run);
 	      role_to_run_buf = termmapSet (role_to_run_buf, rolename, rid);
 	      label_to_index_buf = termmapDuplicate (label_to_index);
-	      label_to_index_buf = termmapSet (label_to_index_buf, rd->label, LABEL_GOOD);
+	      label_to_index_buf =
+		termmapSet (label_to_index_buf, rd->label, LABEL_GOOD);
 #ifdef OKIDEBUG
 	      indact ();
-	      printf ("In NI-Synch scan, assuming %i run is involved.\n", rid);
+	      printf ("In NI-Synch scan, assuming %i run is involved.\n",
+		      rid);
 	      indact ();
-	      printf ("Exploring further assuming this matching, which worked.\n");
+	      printf
+		("Exploring further assuming this matching, which worked.\n");
 	      indac++;
 #endif
-	      result = oki_nisynch (sys, trace_index-1, role_to_run_buf, label_to_index_buf);
+	      result =
+		oki_nisynch (sys, trace_index - 1, role_to_run_buf,
+			     label_to_index_buf);
 #ifdef OKIDEBUG
 	      indact ();
 	      printf (">%i<\n", result);
@@ -274,13 +285,14 @@ oki_nisynch_send (const System sys, const int trace_index, const Termmap role_to
  *@returns 1 iff the claim is allright, 0 iff it is violated.
  */
 int
-oki_nisynch (const System sys, const int trace_index, const Termmap role_to_run, const Termmap label_to_index)
+oki_nisynch (const System sys, const int trace_index,
+	     const Termmap role_to_run, const Termmap label_to_index)
 {
   int type;
 
   // Check for completed trace
   if (trace_index < 0)
-      return oki_nisynch_full (sys, label_to_index);
+    return oki_nisynch_full (sys, label_to_index);
 
 #ifdef OKIDEBUG
   indact ();
@@ -293,11 +305,11 @@ oki_nisynch (const System sys, const int trace_index, const Termmap role_to_run,
   type = sys->traceEvent[trace_index]->type;
 
   if (type == CLAIM || sys->traceEvent[trace_index]->internal)
-      return oki_nisynch_other (sys, trace_index, role_to_run, label_to_index);
+    return oki_nisynch_other (sys, trace_index, role_to_run, label_to_index);
   if (type == READ)
-      return oki_nisynch_read (sys, trace_index, role_to_run, label_to_index);
+    return oki_nisynch_read (sys, trace_index, role_to_run, label_to_index);
   if (type == SEND)
-      return oki_nisynch_send (sys, trace_index, role_to_run, label_to_index);
+    return oki_nisynch_send (sys, trace_index, role_to_run, label_to_index);
   /*
    * Exception: no claim, no send, no read, what is it?
    */
@@ -318,7 +330,7 @@ check_claim_nisynch (const System sys, const int i)
   Roledef rd;
   int result;
   int rid;
-  Termmap f,g;
+  Termmap f, g;
   Term label;
   Claimlist cl;
   Termlist tl;
@@ -342,12 +354,12 @@ check_claim_nisynch (const System sys, const int i)
   /*
    * Check claim
    */
-  result = oki_nisynch(sys, i, f, g);
+  result = oki_nisynch (sys, i, f, g);
   if (!result)
     {
       cl->failed = statesIncrease (cl->failed);
 
-#ifdef DEBUG 
+#ifdef DEBUG
       globalError++;
       warning ("Claim has failed!");
       eprintf ("To be exact, claim label ");
@@ -355,7 +367,7 @@ check_claim_nisynch (const System sys, const int i)
       eprintf (" with prec set ");
       termlistPrint (cl->prec);
       eprintf ("\n");
-      eprintf ("i: %i\nf: ",i);
+      eprintf ("i: %i\nf: ", i);
       termmapPrint (f);
       eprintf ("\ng: ");
       termmapPrint (g);
@@ -380,7 +392,7 @@ check_claim_niagree (const System sys, const int i)
   Roledef rd;
   int result;
   int rid;
-  Termmap f,g;
+  Termmap f, g;
   Term label;
   Claimlist cl;
   Termlist tl;
@@ -404,7 +416,7 @@ check_claim_niagree (const System sys, const int i)
   /*
    * Check claim
    */
-  result = oki_nisynch(sys, i, f, g);
+  result = oki_nisynch (sys, i, f, g);
   if (!result)
     {
       cl->failed = statesIncrease (cl->failed);
@@ -416,7 +428,7 @@ check_claim_niagree (const System sys, const int i)
       printf (" with prec set ");
       termlistPrint (cl->prec);
       printf ("\n");
-      printf ("i: %i\nf: ",i);
+      printf ("i: %i\nf: ", i);
       termmapPrint (f);
       printf ("\ng: ");
       termmapPrint (g);
@@ -428,4 +440,3 @@ check_claim_niagree (const System sys, const int i)
   termmapDelete (g);
   return result;
 }
-
diff --git a/src/compiler.c b/src/compiler.c
index 2f29d50..f748949 100644
--- a/src/compiler.c
+++ b/src/compiler.c
@@ -243,7 +243,8 @@ symbolFind (Symbol s)
 }
 
 //! Yield a basic global constant term (we suppose it exists) or NULL, given a string
-Term findGlobalConstant (const char *s)
+Term
+findGlobalConstant (const char *s)
 {
   return levelFind (lookup (s), 0);
 }
@@ -286,7 +287,9 @@ defineUsertype (Tac tcdu)
 	  else
 	    {
 	      /* that's not right! */
-	      error ("Conflicting definitions in usertype definition on line %i.", tc->lineno);
+	      error
+		("Conflicting definitions in usertype definition on line %i.",
+		 tc->lineno);
 	    }
 	}
       tc = tc->next;
@@ -303,7 +306,8 @@ levelTacDeclaration (Tac tc, int isVar)
   tscan = tc->t2.tac;
   if (!isVar && tscan->next != NULL)
     {
-      error ("Multiple type definition for constant on line %i.", tscan->lineno);
+      error ("Multiple type definition for constant on line %i.",
+	     tscan->lineno);
     }
   while (tscan != NULL && tscan->op == TAC_STRING)
     {
@@ -313,13 +317,14 @@ levelTacDeclaration (Tac tc, int isVar)
       if (t == NULL)
 	{
 	  /* not declared, that is unacceptable. */
-          error ("Undeclared type on line %i.", tscan->lineno);
+	  error ("Undeclared type on line %i.", tscan->lineno);
 	}
       else
 	{
 	  if (!inTermlist (t->stype, TERM_Type))
 	    {
-              error ("Non-type constant in type declaration on line %i.", tscan->lineno);
+	      error ("Non-type constant in type declaration on line %i.",
+		     tscan->lineno);
 	    }
 	}
       typetl = termlistAdd (typetl, t);
@@ -373,7 +378,7 @@ commEvent (int event, Tac tc)
       /* now parse triplet info */
       if (trip == NULL || trip->next == NULL || trip->next->next == NULL)
 	{
-          error ("Problem with %i event on line %i.", event, tc->lineno);
+	  error ("Problem with %i event on line %i.", event, tc->lineno);
 	}
       fromrole = tacTerm (trip);
       torole = tacTerm (trip->next);
@@ -385,7 +390,8 @@ commEvent (int event, Tac tc)
       /* now parse tuple info */
       if (trip == NULL || trip->next == NULL)
 	{
-          error ("Problem with claim %i event on line %i.", event, tc->lineno);
+	  error ("Problem with claim %i event on line %i.", event,
+		 tc->lineno);
 	}
       fromrole = tacTerm (trip);
       claimbig = tacTerm (tacTuple ((trip->next)));
@@ -394,8 +400,7 @@ commEvent (int event, Tac tc)
       torole = claim;
 
       /* check for ignored claim types */
-      if (sys->switchClaimToCheck != NULL &&
-	  sys->switchClaimToCheck != claim)
+      if (sys->switchClaimToCheck != NULL && sys->switchClaimToCheck != claim)
 	{
 	  /* abort the construction of the node */
 	  return;
@@ -404,7 +409,7 @@ commEvent (int event, Tac tc)
       /* check for obvious flaws */
       if (claim == NULL)
 	{
-          error ("Invalid claim specification on line %i.", tc->lineno);
+	  error ("Invalid claim specification on line %i.", tc->lineno);
 	}
       if (!inTermlist (claim->stype, TERM_Claim))
 	{
@@ -426,12 +431,13 @@ commEvent (int event, Tac tc)
 	  msg = deVar (claimbig)->right.op2;
 	  if (tupleCount (msg) != n)
 	    {
-	      error ("Problem with claim tuple unfolding at line %i.", trip->next->lineno);
+	      error ("Problem with claim tuple unfolding at line %i.",
+		     trip->next->lineno);
 	    }
 	}
 
       /* store claim in claim list */
-      
+
       // First check whether label is unique
       cl = sys->claimlist;
       while (cl != NULL)
@@ -441,7 +447,7 @@ commEvent (int event, Tac tc)
 	      /**
 	       *@todo This should not error exit, but automatically generate a fresh claim label.
 	       */
-	      error ("Claim label is not unique at line %i.",tc->lineno);
+	      error ("Claim label is not unique at line %i.", tc->lineno);
 	    }
 	  cl = cl->next;
 	}
@@ -462,7 +468,9 @@ commEvent (int event, Tac tc)
 	{
 	  if (n == 0)
 	    {
-	      error ("Secrecy claim requires a list of terms to be secret on line %i.",trip->next->lineno);
+	      error
+		("Secrecy claim requires a list of terms to be secret on line %i.",
+		 trip->next->lineno);
 	    }
 	  break;
 	}
@@ -470,7 +478,8 @@ commEvent (int event, Tac tc)
 	{
 	  if (n != 0)
 	    {
-	      error ("NISYNCH claim requires no parameters at line %i.", trip->next->lineno);
+	      error ("NISYNCH claim requires no parameters at line %i.",
+		     trip->next->lineno);
 	    }
 	  break;
 	}
@@ -478,7 +487,8 @@ commEvent (int event, Tac tc)
 	{
 	  if (n != 0)
 	    {
-	      error ("NIAGREE claim requires no parameters at line %i.", trip->next->lineno);
+	      error ("NIAGREE claim requires no parameters at line %i.",
+		     trip->next->lineno);
 	    }
 	  break;
 	}
@@ -518,7 +528,8 @@ normalDeclaration (Tac tc)
       knowledgeAddTermlist (sys->know, tacTermlist (tc->t1.tac));
       break;
     case TAC_INVERSEKEYS:
-      knowledgeAddInverse (sys->know, tacTerm (tc->t1.tac), tacTerm (tc->t2.tac));
+      knowledgeAddInverse (sys->know, tacTerm (tc->t1.tac),
+			   tacTerm (tc->t2.tac));
       break;
     default:
       /* abort with false */
@@ -799,111 +810,108 @@ tacTermlist (Tac tc)
 void
 compute_prec_sets (const System sys)
 {
-  Term *eventlabels;	// array: maps events to labels
-  int *prec;		// array: maps event*event to precedence
-  int size;		// temp constant: rolecount * roleeventmax
-  int r1,r2,ev1,ev2;	// some counters
-  int i,j;
+  Term *eventlabels;		// array: maps events to labels
+  int *prec;			// array: maps event*event to precedence
+  int size;			// temp constant: rolecount * roleeventmax
+  int r1, r2, ev1, ev2;		// some counters
+  int i, j;
   Claimlist cl;
 
   // Assist: compute index from role, lev
-  int
-  index (int r, int lev)
-    {
-      return r * sys->roleeventmax + lev;
-    }
+  int index (int r, int lev)
+  {
+    return r * sys->roleeventmax + lev;
+  }
 
   // Assist: compute matrix index from i*i
-  int
-  index2 (int i1, int i2)
-    {
-      return i1 * size + i2;
-    }
+  int index2 (int i1, int i2)
+  {
+    return i1 * size + i2;
+  }
   // Assist: yield roledef from r, lev
-  Roledef
-  roledef_re (int r, int lev)
-    {
-      Protocol pr;
-      Role ro;
-      Roledef rd;
+  Roledef roledef_re (int r, int lev)
+  {
+    Protocol pr;
+    Role ro;
+    Roledef rd;
 
-      pr = sys->protocols;
-      ro = pr->roles;
-      while (r > 0 && ro != NULL)
-	{
-	  ro = ro->next;
-	  if (ro == NULL)
-	    {
-	      pr = pr->next;
-	      if (pr != NULL)
-		{
-	      	  ro = pr->roles;
-		}
-	      else
-		{
-		  ro = NULL;
-		}
-	    }
-	  r--;
-	}
-      if (ro != NULL)
-	{
-	  rd = ro->roledef;
-	  while (lev > 0 && rd != NULL)
-	    {
-	      rd = rd->next;
-	      lev--;
-	    }
-	  return rd;
-	}
-      else
-	{
-	  return NULL;
-	}
-    }
+    pr = sys->protocols;
+    ro = pr->roles;
+    while (r > 0 && ro != NULL)
+      {
+	ro = ro->next;
+	if (ro == NULL)
+	  {
+	    pr = pr->next;
+	    if (pr != NULL)
+	      {
+		ro = pr->roles;
+	      }
+	    else
+	      {
+		ro = NULL;
+	      }
+	  }
+	r--;
+      }
+    if (ro != NULL)
+      {
+	rd = ro->roledef;
+	while (lev > 0 && rd != NULL)
+	  {
+	    rd = rd->next;
+	    lev--;
+	  }
+	return rd;
+      }
+    else
+      {
+	return NULL;
+      }
+  }
 
   // Assist: print matrix
-  void
-  show_matrix (void)
-    {
-      int r1, r2, ev1, ev2;
+  void show_matrix (void)
+  {
+    int r1, r2, ev1, ev2;
+
+    r1 = 0;
+    while (r1 < sys->rolecount)
+      {
+	ev1 = 0;
+	while (ev1 < sys->roleeventmax)
+	  {
+	    printf ("prec %i,%i:  ", r1, ev1);
+	    r2 = 0;
+	    while (r2 < sys->rolecount)
+	      {
+		ev2 = 0;
+		while (ev2 < sys->roleeventmax)
+		  {
+		    printf ("%i ",
+			    prec[index2 (index (r2, ev2), index (r1, ev1))]);
+		    ev2++;
+		  }
+		printf (" ");
+		r2++;
+	      }
+	    printf ("\n");
+	    ev1++;
+	  }
+	printf ("\n");
+	r1++;
+      }
+    printf ("\n");
+  }
 
-      r1 = 0;
-      while (r1 < sys->rolecount)
-	{
-	  ev1 = 0;
-	  while (ev1 < sys->roleeventmax)
-	    {
-              printf ("prec %i,%i:  ", r1,ev1);
-	      r2 = 0;
-	      while (r2 < sys->rolecount)
-		{
-		  ev2 = 0;
-		  while (ev2 < sys->roleeventmax)
-		    {
-		      printf ("%i ", prec[index2 (index (r2,ev2), index (r1, ev1))]);
-		      ev2++;
-		    }
-		  printf (" ");
-		  r2++;
-		}
-              printf ("\n");
-	      ev1++;
-	    }
-          printf ("\n");
-	  r1++;
-	}
-       printf ("\n");
-    }
-  
   /*
    * Phase 1: Allocate structures and map to labels
    */
   //printf ("Rolecount: %i\n", sys->rolecount);
   //printf ("Maxevent : %i\n", sys->roleeventmax);
   size = sys->rolecount * sys->roleeventmax;
-  eventlabels = memAlloc (size * sizeof(Term));
-  prec = memAlloc (size * size * sizeof(int));
+  eventlabels = memAlloc (size * sizeof (Term));
+  prec = memAlloc (size * size * sizeof (int));
   // Clear tables
   i = 0;
   while (i < size)
@@ -912,7 +920,7 @@ compute_prec_sets (const System sys)
       j = 0;
       while (j < size)
 	{
-	  prec[index2(i,j)] = 0;
+	  prec[index2 (i, j)] = 0;
 	  j++;
 	}
       i++;
@@ -927,7 +935,7 @@ compute_prec_sets (const System sys)
       rd = roledef_re (r1, ev1);
       while (rd != NULL)
 	{
-	  eventlabels[index(r1,ev1)] = rd->label;
+	  eventlabels[index (r1, ev1)] = rd->label;
 	  //termPrint (rd->label);
 	  //printf ("\t");
 	  ev1++;
@@ -942,8 +950,8 @@ compute_prec_sets (const System sys)
     {
       ev1 = 0;
       while (ev1 < (sys->roleeventmax - 1))
-	{ 
-	  prec[index2 (index (r1,ev1),index (r1,ev1+1))] = 1;
+	{
+	  prec[index2 (index (r1, ev1), index (r1, ev1 + 1))] = 1;
 	  ev1++;
 	}
       r1++;
@@ -957,7 +965,7 @@ compute_prec_sets (const System sys)
 	{
 	  Roledef rd1;
 
-	  rd1 = roledef_re(r1,ev1);
+	  rd1 = roledef_re (r1, ev1);
 	  if (rd1 != NULL && rd1->type == SEND)
 	    {
 	      r2 = 0;
@@ -968,10 +976,11 @@ compute_prec_sets (const System sys)
 		    {
 		      Roledef rd2;
 
-		      rd2 = roledef_re(r2,ev2);
-		      if (rd2 != NULL && rd2->type == READ && isTermEqual(rd1->label, rd2->label))
+		      rd2 = roledef_re (r2, ev2);
+		      if (rd2 != NULL && rd2->type == READ
+			  && isTermEqual (rd1->label, rd2->label))
 			{
-			  prec[index2(index(r1,ev1),index(r2,ev2))] = 1;
+			  prec[index2 (index (r1, ev1), index (r2, ev2))] = 1;
 			}
 		      ev2++;
 		    }
@@ -995,16 +1004,16 @@ compute_prec_sets (const System sys)
       j = 0;
       while (j < size)
 	{
-	  if (prec[index2 (j,i)] == 1)
+	  if (prec[index2 (j, i)] == 1)
 	    {
 	      int k;
 
 	      k = 0;
 	      while (k < size)
 		{
-		  if (prec[index2 (k,j)] == 1)
+		  if (prec[index2 (k, j)] == 1)
 		    {
-		      prec[index2 (k,i)] = 1;
+		      prec[index2 (k, i)] = 1;
 		    }
 		  k++;
 		}
@@ -1039,15 +1048,18 @@ compute_prec_sets (const System sys)
 	      r1++;
 	    }
 	}
-      while (r1 < sys->rolecount && !isTermEqual (label, eventlabels[index(r1,ev1)]));
+      while (r1 < sys->rolecount
+	     && !isTermEqual (label, eventlabels[index (r1, ev1)]));
       if (r1 == sys->rolecount)
 	{
-	  error ("Prec() setup: Could not find the event corresponding to a claim label.");
+	  error
+	    ("Prec() setup: Could not find the event corresponding to a claim label.");
 	}
-      rd = roledef_re (r1,ev1);
+      rd = roledef_re (r1, ev1);
       if (rd->type != CLAIM)
 	{
-	  error ("Prec() setup: First event with claim label doesn't seem to be a claim.");
+	  error
+	    ("Prec() setup: First event with claim label doesn't seem to be a claim.");
 	}
       // Store in claimlist structure
       cl->r = r1;
@@ -1057,21 +1069,21 @@ compute_prec_sets (const System sys)
        * Now we compute the preceding label set
        */
       cl->prec = NULL;		// clear first
-      claim_index = index (r1,ev1);
+      claim_index = index (r1, ev1);
       r2 = 0;
       while (r2 < sys->rolecount)
 	{
 	  Roledef rd2;
 
 	  ev2 = 0;
-	  rd = roledef_re (r2,ev2);
+	  rd = roledef_re (r2, ev2);
 	  while (rd != NULL)
 	    {
-	      if (prec[index2 (index (r2,ev2),claim_index)] == 1)
+	      if (prec[index2 (index (r2, ev2), claim_index)] == 1)
 		{
 		  // This event precedes the claim
-		  
-                  if (rd->type == READ)
+
+		  if (rd->type == READ)
 		    {
 		      // Only store read labels (but send would work as well)
 		      cl->prec = termlistAdd (cl->prec, rd->label);
@@ -1096,7 +1108,8 @@ compute_prec_sets (const System sys)
 	  tl_scan = cl->prec;
 	  while (tl_scan != NULL)
 	    {
-	      sys->synchronising_labels = termlistAddNew (sys->synchronising_labels, tl_scan->term);
+	      sys->synchronising_labels =
+		termlistAddNew (sys->synchronising_labels, tl_scan->term);
 	      tl_scan = tl_scan->next;
 	    }
 	}
@@ -1125,11 +1138,12 @@ compute_prec_sets (const System sys)
 		  while (ev_scan < sys->roleeventmax)
 		    {
 		      // if this event preceds the claim, replace the label term
-		      if (prec[index2 (index (r_scan, ev_scan), claim_index)] == 1)
+		      if (prec[index2 (index (r_scan, ev_scan), claim_index)]
+			  == 1)
 			{
 			  Roledef rd;
 
-	  		  rd = roledef_re (r_scan,ev_scan);
+			  rd = roledef_re (r_scan, ev_scan);
 			  if (rd->label != NULL)
 			    {
 			      t_buf = rd->label;
@@ -1140,7 +1154,8 @@ compute_prec_sets (const System sys)
 		  // Store only the last label
 		  if (t_buf != NULL)
 		    {
-		      sys->synchronising_labels = termlistAddNew(sys->synchronising_labels, t_buf);
+		      sys->synchronising_labels =
+			termlistAddNew (sys->synchronising_labels, t_buf);
 		    }
 		}
 	      r_scan++;
@@ -1153,15 +1168,17 @@ compute_prec_sets (const System sys)
 	{
 	  termlistDelete (sys->synchronising_labels);
 	  sys->synchronising_labels = NULL;
-	  warning ("Emptied synchronising labels set manually because --pp=100.");
+	  warning
+	    ("Emptied synchronising labels set manually because --pp=100.");
 	}
 #endif
       // Check for empty stuff
       //@todo This is for debugging, mainly.
       if (cl->prec == NULL)
 	{
-	  fprintf (stderr, "Warning: claim with empty prec() set at r:%i, ev:%i\n",
-		   r1,ev1);
+	  fprintf (stderr,
+		   "Warning: claim with empty prec() set at r:%i, ev:%i\n",
+		   r1, ev1);
 	}
       else
 	{
@@ -1177,11 +1194,11 @@ compute_prec_sets (const System sys)
   /*
    * Cleanup
    */
-  memFree (eventlabels, size * sizeof(Term));
-  memFree (prec, size * size * sizeof(int));
+  memFree (eventlabels, size * sizeof (Term));
+  memFree (prec, size * size * sizeof (int));
 
 #ifdef DEBUG
-  if (DEBUGL(2))
+  if (DEBUGL (2))
     {
       printf ("Synchronising labels set: ");
       termlistPrint (sys->synchronising_labels);
@@ -1192,16 +1209,16 @@ compute_prec_sets (const System sys)
 }
 
 //! Preprocess after system compilation
-void 
+void
 preprocess (const System sys)
 {
   /*
    * init some counters
    */
-  sys->rolecount = compute_rolecount(sys);
-  sys->roleeventmax = compute_roleeventmax(sys);
+  sys->rolecount = compute_rolecount (sys);
+  sys->roleeventmax = compute_roleeventmax (sys);
   /*
    * compute preceding label sets
    */
-  compute_prec_sets(sys);
+  compute_prec_sets (sys);
 }
diff --git a/src/error.c b/src/error.c
index 913e00e..7b29ef8 100644
--- a/src/error.c
+++ b/src/error.c
@@ -6,7 +6,7 @@
 void
 error_die (void)
 {
-  exit(1);
+  exit (1);
 }
 
 //! Print error message header
@@ -26,7 +26,7 @@ error_pre (void)
  * Input is comparable to printf, only end of line is not required.
  */
 void
-error_post (char *fmt, ... )
+error_post (char *fmt, ...)
 {
   va_list args;
 
@@ -34,7 +34,7 @@ error_post (char *fmt, ... )
   vfprintf (stderr, fmt, args);
   fprintf (stderr, "\n");
   va_end (args);
-  exit(1);
+  exit (1);
 }
 
 //! Print error message and die.
@@ -43,7 +43,7 @@ error_post (char *fmt, ... )
  * Input is comparable to printf, only end of line is not required.
  */
 void
-error (char *fmt, ... )
+error (char *fmt, ...)
 {
   va_list args;
 
@@ -60,7 +60,7 @@ error (char *fmt, ... )
  * Input is comparable to printf, only end of line is not required.
  */
 void
-warning (char *fmt, ... )
+warning (char *fmt, ...)
 {
   va_list args;
 
diff --git a/src/error.h b/src/error.h
index 85216de..7218a6f 100644
--- a/src/error.h
+++ b/src/error.h
@@ -3,8 +3,8 @@
 
 void error_die (void);
 void error_pre (void);
-void error_post (char *fmt, ... );
-void error (char *fmt, ... );
-void warning (char *fmt, ... );
+void error_post (char *fmt, ...);
+void error (char *fmt, ...);
+void warning (char *fmt, ...);
 
 #endif
diff --git a/src/knowledge.c b/src/knowledge.c
index d4b518e..fe3a2eb 100644
--- a/src/knowledge.c
+++ b/src/knowledge.c
@@ -285,7 +285,8 @@ inKnowledge (const Knowledge know, Term term)
   if (term->type == ENCRYPT)
     {
       return inTermlist (know->encrypt, term) ||
-	(inKnowledge (know, term->right.key) && inKnowledge (know, term->left.op));
+	(inKnowledge (know, term->right.key)
+	 && inKnowledge (know, term->left.op));
     }
   if (term->type == TUPLE)
     {
@@ -354,9 +355,9 @@ knowledgePrintShort (const Knowledge know)
     {
       termlistPrint (know->basic);
       if (know->encrypt != NULL);
-	{
-	  eprintf (", ");
-	}
+      {
+	eprintf (", ");
+      }
     }
   if (know->encrypt != NULL)
     {
@@ -440,7 +441,8 @@ knowledgeGetInverses (const Knowledge know)
 __inline__ Termlist
 knowledgeGetBasics (const Knowledge know)
 {
-  return termlistAddBasics (termlistAddBasics(NULL, know->basic), know->encrypt);
+  return termlistAddBasics (termlistAddBasics (NULL, know->basic),
+			    know->encrypt);
 }
 
 //! check whether any substitutions where made in a knowledge set.
@@ -540,7 +542,7 @@ knowledgeNew (const Knowledge oldk, const Knowledge newk)
 	tl = tl->next;
       }
   }
-  
+
   newtl = NULL;
   addNewStuff (newk->basic);
   addNewStuff (newk->encrypt);
diff --git a/src/latex.c b/src/latex.c
index f83f58c..ec03bee 100644
--- a/src/latex.c
+++ b/src/latex.c
@@ -176,15 +176,15 @@ latexTermTuplePrint (Term term, Termlist hl)
       printf ("Empty term");
       return;
     }
-  term = deVar(term);
+  term = deVar (term);
   while (realTermTuple (term))
     {
       // To remove any brackets, change this into latexTermTuplePrint.
       latexTermPrint (term->left.op1, hl);
       printf (",");
-      term = deVar(term->right.op2);
+      term = deVar (term->right.op2);
     }
-  latexTermPrint(term, hl);
+  latexTermPrint (term, hl);
   return;
 }
 
@@ -290,11 +290,11 @@ latexDeclInst (const System sys, int run)
 	  if (!isTermEqual (myRole, roles->term))
 	    {
 	      if (!first)
-		  printf (", ");
+		printf (", ");
 	      else
-		  first = 0;
-	      termPrint (agentOfRunRole(sys,run,roles->term));
-	      printf(": ");
+		first = 0;
+	      termPrint (agentOfRunRole (sys, run, roles->term));
+	      printf (": ");
 	      termPrint (roles->term);
 	    }
 	  roles = roles->next;
@@ -305,9 +305,9 @@ latexDeclInst (const System sys, int run)
   /* display agent and role */
   printf ("$\\mathbf{");
   termPrint (myAgent);
-  printf("}: ");
+  printf ("}: ");
   termPrint (myRole);
-  
+
   printf ("$}\n");
 
   /* cleanup */
@@ -896,7 +896,7 @@ attackDisplayLatex (const System sys)
 
   for (pass = 1; pass <= 2; pass++)
     {
-      printf ("%% Pass %i\n\n",pass);
+      printf ("%% Pass %i\n\n", pass);
 
       if (pass == 1)
 	{
@@ -915,7 +915,7 @@ attackDisplayLatex (const System sys)
 	  printf ("\\addtolength{\\maxmsccondition}{\\mscspacer}\n");
 
 	  /* put out computed widths */
-	  
+
 	  printf ("\\setlength{\\envinstdist}{0.7\\maxmscall}\n");
 	  printf ("\\setlength{\\instdist}{\\maxmscall}\n");
 	  printf ("\\setlength{\\actionwidth}{\\maxmscaction}\n");
@@ -949,9 +949,9 @@ attackDisplayLatex (const System sys)
 	}
       /* Add the intruder instance */
       if (pass == 2)
-	  printf ("\\declinst{eve}{}{");
+	printf ("\\declinst{eve}{}{");
       else
-	  printf ("\\maxlength{\\maxmscinst}{");
+	printf ("\\maxlength{\\maxmscinst}{");
       printf ("{\\bf Eve}: Intruder}\n\n");
 
       /* Print the local constants for each instance */
@@ -971,9 +971,9 @@ attackDisplayLatex (const System sys)
 		      if (first)
 			{
 			  if (pass == 1)
-			      printf ("\\maxlength{\\maxmscaction}{$");
+			    printf ("\\maxlength{\\maxmscaction}{$");
 			  else
-			      printf ("\\ActionBox{creates \\\\\n$");
+			    printf ("\\ActionBox{creates \\\\\n$");
 			  first = 0;
 			}
 		      else
@@ -987,9 +987,9 @@ attackDisplayLatex (const System sys)
 	      if (!first)
 		{
 		  if (pass == 1)
-		      printf ("$}\n");
+		    printf ("$}\n");
 		  else
-		      printf ("$}{run%i}\n", i);
+		    printf ("$}{run%i}\n", i);
 		}
 	    }
 	}
@@ -999,12 +999,12 @@ attackDisplayLatex (const System sys)
       if (pass == 2)
 	{
 	  printf ("\\ActionBox{");
-          printf ("knows \\\\\n$");
-          knowledgePrintLatex (tb->know[0]);
-          printf ("$}");
+	  printf ("knows \\\\\n$");
+	  knowledgePrintLatex (tb->know[0]);
+	  printf ("$}");
 	  printf ("{eve}\n");
-          printf ("\\nextlevel[3]\n");
-          printf ("\n");
+	  printf ("\\nextlevel[3]\n");
+	  printf ("\n");
 	}
 
       /* print the events in the attack */
@@ -1044,7 +1044,8 @@ attackDisplayLatex (const System sys)
 
 		  if (tb->link[i] != -1 && i < tb->length)
 		    {
-		      latexMessagePrintHighlight (tb, i, tb->link[i], highlights);
+		      latexMessagePrintHighlight (tb, i, tb->link[i],
+						  highlights);
 		    }
 		  else
 		    {
@@ -1062,8 +1063,8 @@ attackDisplayLatex (const System sys)
 			}
 		      else
 			{
-		          printf ("\\nextlevel[1]\n");
-		          printf ("\\ActionBox{learns \\\\\n");
+			  printf ("\\nextlevel[1]\n");
+			  printf ("\\ActionBox{learns \\\\\n");
 			}
 		      printf ("$");
 		      cKnowledge++;
@@ -1076,7 +1077,7 @@ attackDisplayLatex (const System sys)
 		      else
 			{
 			  printf ("{eve}\n");
-		      	  printf ("\\nextlevel[2]\n");
+			  printf ("\\nextlevel[2]\n");
 			}
 		    }
 
@@ -1099,7 +1100,7 @@ attackDisplayLatex (const System sys)
 		    }
 		  break;
 		default:
-		  break;		//kannie!
+		  break;	//kannie!
 		}
 	    }
 	}
diff --git a/src/latex.h b/src/latex.h
index 7dab51e..413acb9 100644
--- a/src/latex.h
+++ b/src/latex.h
@@ -7,14 +7,14 @@
 
 #include "system.h"
 
-void latexInit(const System sys, int argc, char **argv);
-void latexDone(const System sys);
-void latexTimers(const System sys);
-void latexMSCStart();
-void latexMSCEnd();
-void latexLearnComment(const System sys, Termlist tl);
-void latexTracePrint(const System sys);
-void attackDisplayLatex(const System sys);
+void latexInit (const System sys, int argc, char **argv);
+void latexDone (const System sys);
+void latexTimers (const System sys);
+void latexMSCStart ();
+void latexMSCEnd ();
+void latexLearnComment (const System sys, Termlist tl);
+void latexTracePrint (const System sys);
+void attackDisplayLatex (const System sys);
 void latexTermPrint (Term term, Termlist hl);
 void latexTermTuplePrint (Term term, Termlist hl);
 
diff --git a/src/main.c b/src/main.c
index 2f4fbfe..5be03a4 100644
--- a/src/main.c
+++ b/src/main.c
@@ -82,47 +82,67 @@ main (int argc, char **argv)
 {
   System sys;
 
-  struct arg_file *infile  = arg_file0(NULL,NULL,"FILE",    "input file ('-' for stdin)");
-  struct arg_file *outfile = arg_file0("o","output","FILE", "output file (default is stdout)");
-  struct arg_str *switch_check = arg_str0(NULL,"check","CLAIM","claim type to check (default is all)");
-  struct arg_int *switch_scenario =
-      arg_int0 ("s", "scenario", NULL, "select a scenario instance 1-n (-1 to count)");
-  struct arg_int *switch_scenario_size =
-      arg_int0 ("S", "scenario-size", NULL, "scenario size (fixed trace prefix length)");
+  struct arg_file *infile =
+    arg_file0 (NULL, NULL, "FILE", "input file ('-' for stdin)");
+  struct arg_file *outfile = arg_file0 ("o", "output", "FILE",
+					"output file (default is stdout)");
+  struct arg_str *switch_check = arg_str0 (NULL, "check", "CLAIM",
+					   "claim type to check (default is all)");
+  struct arg_int *switch_scenario = arg_int0 ("s", "scenario", NULL,
+					      "select a scenario instance 1-n (-1 to count)");
+  struct arg_int *switch_scenario_size = arg_int0 ("S", "scenario-size", NULL,
+						   "scenario size (fixed trace prefix length)");
   struct arg_int *switch_traversal_method = arg_int0 ("t", "traverse", NULL,
-					"set traversal method, partial order reduction (default is 12)");
+						      "set traversal method, partial order reduction (default is 12)");
   struct arg_int *switch_match_method =
     arg_int0 ("m", "match", NULL, "matching method (default is 0)");
   struct arg_lit *switch_clp =
     arg_lit0 ("c", "cl", "use constraint logic, non-associative");
   struct arg_int *switch_pruning_method = arg_int0 ("p", "prune", NULL,
-				    "pruning method (default is 2)");
-  struct arg_int *switch_prune_trace_length = arg_int0 ("l", "max-length", NULL,
-					"prune traces longer than <int> events");
-  struct arg_lit *switch_incremental_trace_length = arg_lit0 (NULL, "increment-traces",
-					"incremental search using the length of the traces.");
+						    "pruning method (default is 2)");
+  struct arg_int *switch_prune_trace_length =
+    arg_int0 ("l", "max-length", NULL,
+	      "prune traces longer than <int> events");
+  struct arg_lit *switch_incremental_trace_length =
+    arg_lit0 (NULL, "increment-traces",
+	      "incremental search using the length of the traces.");
   struct arg_int *switch_maximum_runs =
     arg_int0 ("r", "max-runs", NULL, "create at most <int> runs");
   struct arg_lit *switch_incremental_runs = arg_lit0 (NULL, "increment-runs",
-				      "incremental search using the number of runs");
-  struct arg_lit *switch_latex_output = arg_lit0 (NULL, "latex", "output attacks in LaTeX format");
+						      "incremental search using the number of runs");
+  struct arg_lit *switch_latex_output =
+    arg_lit0 (NULL, "latex", "output attacks in LaTeX format");
   struct arg_lit *switch_empty =
     arg_lit0 ("e", "empty", "do not generate output");
-  struct arg_lit *switch_progress_bar = arg_lit0 ("b", "progress-bar", "show progress bar");
-  struct arg_lit *switch_state_space_graph = arg_lit0 (NULL, "state-space", "output state space graph");
-  struct arg_lit *switch_implicit_choose = arg_lit0 (NULL, "implicit-choose", "allow implicit choose events (useful for few runs)");
-  struct arg_lit *switch_choose_first = arg_lit0 (NULL, "choose-first", "priority to any choose events");
-  struct arg_lit *switch_enable_read_symmetries = arg_lit0 (NULL, "read-symm", "enable read symmetry reductions");
-  struct arg_lit *switch_disable_agent_symmetries = arg_lit0 (NULL, "no-agent-symm", "disable agent symmetry reductions");
-  struct arg_lit *switch_enable_symmetry_order = arg_lit0 (NULL, "symm-order", "enable ordering symmetry reductions");
-  struct arg_lit *switch_disable_noclaims_reductions = arg_lit0 (NULL, "no-noclaims-red", "disable no more claims reductions");
-  struct arg_lit *switch_disable_endgame_reductions = arg_lit0 (NULL, "no-endgame-red", "disable endgame reductions");
-  struct arg_lit *switch_summary = arg_lit0 (NULL, "summary", "show summary on stdout instead of stderr");
-  struct arg_lit *switch_echo = arg_lit0 ("E", "echo", "echo command line to stdout");
+  struct arg_lit *switch_progress_bar =
+    arg_lit0 ("b", "progress-bar", "show progress bar");
+  struct arg_lit *switch_state_space_graph =
+    arg_lit0 (NULL, "state-space", "output state space graph");
+  struct arg_lit *switch_implicit_choose = arg_lit0 (NULL, "implicit-choose",
+						     "allow implicit choose events (useful for few runs)");
+  struct arg_lit *switch_choose_first =
+    arg_lit0 (NULL, "choose-first", "priority to any choose events");
+  struct arg_lit *switch_enable_read_symmetries =
+    arg_lit0 (NULL, "read-symm", "enable read symmetry reductions");
+  struct arg_lit *switch_disable_agent_symmetries =
+    arg_lit0 (NULL, "no-agent-symm",
+	      "disable agent symmetry reductions");
+  struct arg_lit *switch_enable_symmetry_order = arg_lit0 (NULL, "symm-order",
+							   "enable ordering symmetry reductions");
+  struct arg_lit *switch_disable_noclaims_reductions =
+    arg_lit0 (NULL, "no-noclaims-red",
+	      "disable no more claims reductions");
+  struct arg_lit *switch_disable_endgame_reductions =
+    arg_lit0 (NULL, "no-endgame-red", "disable endgame reductions");
+  struct arg_lit *switch_summary = arg_lit0 (NULL, "summary",
+					     "show summary on stdout instead of stderr");
+  struct arg_lit *switch_echo =
+    arg_lit0 ("E", "echo", "echo command line to stdout");
 #ifdef DEBUG
-  struct arg_int *switch_por_parameter = arg_int0 (NULL, "pp", NULL, "POR parameter");
+  struct arg_int *switch_por_parameter =
+    arg_int0 (NULL, "pp", NULL, "POR parameter");
   struct arg_lit *switch_debug_indent = arg_lit0 ("I", "debug-indent",
-				      "indent the debug output using trace length");
+						  "indent the debug output using trace length");
   struct arg_int *switch_debug_level =
     arg_int0 ("D", "debug", NULL, "set debug level (default is 0)");
 #endif
@@ -131,7 +151,7 @@ main (int argc, char **argv)
     arg_lit0 (NULL, "version", "print version information and exit");
   struct arg_end *end = arg_end (30);
   void *argtable[] = {
-    infile, 
+    infile,
     outfile,
     switch_empty,
     switch_state_space_graph,
@@ -140,13 +160,13 @@ main (int argc, char **argv)
     switch_latex_output,
     switch_summary,
     switch_echo,
-    switch_progress_bar, 
+    switch_progress_bar,
 
     switch_check,
-    switch_traversal_method, 
-    switch_match_method, 
+    switch_traversal_method,
+    switch_match_method,
     switch_clp,
-    switch_pruning_method, 
+    switch_pruning_method,
     switch_prune_trace_length, switch_incremental_trace_length,
     switch_maximum_runs, switch_incremental_runs,
 
@@ -212,7 +232,8 @@ main (int argc, char **argv)
     {
       printf ("'%s' model checker for security protocols.\n", progname);
       printf ("%s release.\n", releasetag);
-      printf ("$Rev$ $Date$\n");
+      printf
+	("$Rev$ $Date$\n");
 #ifdef DEBUG
       printf ("Compiled with debugging support.\n");
 #endif
@@ -232,12 +253,12 @@ main (int argc, char **argv)
     }
 
   /* special case: uname with no command line options induces brief help */
-  if (argc==1)
-   {
-     printf("Try '%s --help' for more information.\n",progname);
-     exitcode=0;
-     goto exit;
-   }
+  if (argc == 1)
+    {
+      printf ("Try '%s --help' for more information.\n", progname);
+      exitcode = 0;
+      goto exit;
+    }
 
   /*
    * Arguments have been parsed by argtable,
@@ -247,11 +268,13 @@ main (int argc, char **argv)
   /* Lutger-tries-to-test-with-broken-methods detector */
   if (switch_clp->count > 0)
     {
-      fprintf (stderr, "For the time being, this method is not supported, \n");
+      fprintf (stderr,
+	       "For the time being, this method is not supported, \n");
       fprintf (stderr, "as too many changes have been made to the normal \n");
-      fprintf (stderr, "matching logic, and CL simply isn't reliable in \nmany ");
+      fprintf (stderr,
+	       "matching logic, and CL simply isn't reliable in \nmany ");
       fprintf (stderr, "ways. Try again in a few weeks.\n");
-      exit(0);
+      exit (0);
     }
 
   /* redirect in- and output according to supplied filenames */
@@ -260,21 +283,23 @@ main (int argc, char **argv)
     {
       /* try to open */
       if (!freopen (outfile->filename[0], "w", stdout))
-        {
-          fprintf(stderr, "Could not create output file '%s'.\n", outfile->filename[0]);
-          exit(1);
-        }
+	{
+	  fprintf (stderr, "Could not create output file '%s'.\n",
+		   outfile->filename[0]);
+	  exit (1);
+	}
     }
   /* input */
   if (infile->count > 0)
     {
       /* check for the single dash */
-      if (strcmp(infile->filename[0],"-"))
+      if (strcmp (infile->filename[0], "-"))
 	{
-          if (!freopen (infile->filename[0], "r", stdin))
+	  if (!freopen (infile->filename[0], "r", stdin))
 	    {
-	      fprintf(stderr, "Could not open input file '%s'.\n", infile->filename[0]);
-	      exit(1);
+	      fprintf (stderr, "Could not open input file '%s'.\n",
+		       infile->filename[0]);
+	      exit (1);
 	    }
 	}
     }
@@ -298,7 +323,7 @@ main (int argc, char **argv)
 
   /*
    * ------------------------------------------------
-   *	 generate system 
+   *     generate system 
    * ------------------------------------------------
    */
 
@@ -321,32 +346,33 @@ main (int argc, char **argv)
   /* handle switches */
 
   if (switch_implicit_choose->count > 0)
-      /* allow implicit chooses */
-      sys->switchForceChoose = 0;
+    /* allow implicit chooses */
+    sys->switchForceChoose = 0;
   if (switch_choose_first->count > 0)
-      sys->switchChooseFirst = 1;	/* priority to chooses */
+    sys->switchChooseFirst = 1;	/* priority to chooses */
   if (switch_enable_read_symmetries->count > 0)
     {
       if (switch_enable_symmetry_order->count > 0)
-	  error ("--read-symm and --symm-order cannot be used at the same time.");
+	error
+	  ("--read-symm and --symm-order cannot be used at the same time.");
       sys->switchReadSymm = 1;
     }
   if (switch_enable_symmetry_order->count > 0)
-      sys->switchSymmOrder = 1;		/* enable symmetry order */
+    sys->switchSymmOrder = 1;	/* enable symmetry order */
   if (switch_disable_agent_symmetries->count > 0)
-      sys->switchAgentSymm = 0;		/* disable agent symmetry order */
+    sys->switchAgentSymm = 0;	/* disable agent symmetry order */
   if (switch_disable_noclaims_reductions->count > 0)
-      sys->switchNomoreClaims = 0;	/* disable no more claims cutter */
+    sys->switchNomoreClaims = 0;	/* disable no more claims cutter */
   if (switch_disable_endgame_reductions->count > 0)
-      sys->switchReduceEndgame = 0;	/* disable endgame cutter */
+    sys->switchReduceEndgame = 0;	/* disable endgame cutter */
   if (switch_summary->count > 0)
-      sys->output = SUMMARY;		/* report summary on stdout */
+    sys->output = SUMMARY;	/* report summary on stdout */
 
   /*
    * The scenario selector has an important side effect; when it is non-null,
    * any scenario traversing selects chooses first.
    */
-  sys->switchScenario = switch_scenario->ival[0];		/* scenario selector */
+  sys->switchScenario = switch_scenario->ival[0];	/* scenario selector */
   sys->switchScenarioSize = switch_scenario_size->ival[0];	/* scenario size */
   if (sys->switchScenario == 0 && sys->switchScenarioSize > 0)
     {
@@ -363,11 +389,11 @@ main (int argc, char **argv)
   if (sys->switchScenario != 0 && sys->switchScenarioSize == 0)
     {
 #ifdef DEBUG
-      warning ("Scenario selection without trace prefix length implies --choose-first.");
+      warning
+	("Scenario selection without trace prefix length implies --choose-first.");
 #endif
       sys->switchChooseFirst = 1;
     }
-
 #ifdef DEBUG
   sys->porparam = switch_por_parameter->ival[0];
 #endif
@@ -381,7 +407,7 @@ main (int argc, char **argv)
       Term claim;
 
 #ifdef DEBUG
-      if (lookup(switch_check->sval[0]) == NULL)
+      if (lookup (switch_check->sval[0]) == NULL)
 	{
 	  globalError++;
 	  warning ("Could not find this string at all in:");
@@ -392,11 +418,11 @@ main (int argc, char **argv)
 #endif
       claim = findGlobalConstant (switch_check->sval[0]);
       if (claim == NULL)
-	  error ("Unknown claim type to check.");
+	error ("Unknown claim type to check.");
       if (inTermlist (claim->stype, TERM_Claim))
-	  sys->switchClaimToCheck = claim;
+	sys->switchClaimToCheck = claim;
       else
-	  error ("Claim type to check is not a claim.");
+	error ("Claim type to check is not a claim.");
     }
 
   /* parse input */
@@ -446,15 +472,15 @@ main (int argc, char **argv)
   sys->match = switch_match_method->ival[0];
   sys->prune = switch_pruning_method->ival[0];
   if (switch_progress_bar->count > 0)
-      /* enable progress display */
-      sys->switchS = 50000;
+    /* enable progress display */
+    sys->switchS = 50000;
   else
-      /* disable progress display */
-      sys->switchS = 0;
+    /* disable progress display */
+    sys->switchS = 0;
   if (switch_state_space_graph->count > 0)
     {
       /* enable state space graph output */
-      sys->output = STATESPACE;		//!< New method
+      sys->output = STATESPACE;	//!< New method
     }
   if (switch_empty->count > 0)
     sys->output = EMPTY;
@@ -486,8 +512,7 @@ main (int argc, char **argv)
   if (switch_incremental_runs->count > 0 ||
       switch_incremental_trace_length->count > 0)
     {
-      if (sys->output != ATTACK &&
-	  sys->output != EMPTY)
+      if (sys->output != ATTACK && sys->output != EMPTY)
 	{
 	  error ("Incremental traversal only for empty or attack output.");
 	}
@@ -497,7 +522,6 @@ main (int argc, char **argv)
     {
       warning ("-m2 is only supported for constraint logic programming.");
     }
-
 #ifdef DEBUG
   warning ("Selected output method is %i", sys->output);
 #endif
@@ -531,14 +555,14 @@ main (int argc, char **argv)
 	  MC_single (sys);
 	}
     }
-  
+
   /* Display shortest attack, if any */
 
   if (sys->attack != NULL && sys->attack->length != 0)
     {
       if (sys->output == ATTACK)
 	{
-      	  attackDisplay(sys);
+	  attackDisplay (sys);
 	}
       /* mark exit code */
       exitcode = 3;
@@ -551,9 +575,9 @@ main (int argc, char **argv)
       cl_scan = sys->claimlist;
       while (cl_scan != NULL)
 	{
-          if (cl_scan->failed == STATES0)
+	  if (cl_scan->failed == STATES0)
 	    {
-              /* mark exit code */
+	      /* mark exit code */
 	      exitcode = 2;
 	    }
 	  cl_scan = cl_scan->next;
@@ -625,7 +649,7 @@ timersPrint (const System sys)
   eprintf ("\n");
 
   /* scenario info */
-  
+
   if (sys->switchScenario > 0)
     {
       eprintf ("scen_st\t");
@@ -648,7 +672,7 @@ timersPrint (const System sys)
   else
     {
       if (sys->failed != STATES0)
-	eprintf ("L:%i\n", attackLength(sys->attack));
+	eprintf ("L:%i\n", attackLength (sys->attack));
       else
 	eprintf ("None\n");
     }
@@ -740,7 +764,8 @@ MC_incRuns (const System sys)
       systemReset (sys);
       sys->maxruns = runs;
       systemRuns (sys);
-      fprintf (stderr, "%i of %i runs in incremental runs search.\n", runs, maxruns);
+      fprintf (stderr, "%i of %i runs in incremental runs search.\n",
+	       runs, maxruns);
       res = modelCheck (sys);
       fprintf (stderr, "\n");
       if (res)
@@ -794,8 +819,9 @@ MC_incTraces (const System sys)
       systemReset (sys);
       sys->maxtracelength = tracelen;
       systemRuns (sys);
-      fprintf (stderr, "%i of %i trace length in incremental trace length search.\n",
-	      tracelen, maxtracelen);
+      fprintf (stderr,
+	       "%i of %i trace length in incremental trace length search.\n",
+	       tracelen, maxtracelen);
       res = modelCheck (sys);
       fprintf (stderr, "\n");
       if (res)
@@ -873,5 +899,3 @@ modelCheck (const System sys)
     }
   return (sys->failed != STATES0);
 }
-
-
diff --git a/src/match_basic.c b/src/match_basic.c
index d4afafa..47a0dd9 100644
--- a/src/match_basic.c
+++ b/src/match_basic.c
@@ -4,7 +4,7 @@
  * The match function here is integrated here with an enabled() function.
  *  It is also the basic match, so not suited for Constraint Logic Programming. 
  */
- 
+
 #include <stdlib.h>
 #include <stdio.h>
 #include "memory.h"
@@ -22,7 +22,7 @@ candidates (const Knowledge know)
 
 struct fvpass
 {
-  int (*solution)();
+  int (*solution) ();
 
   System sys;
   int run;
diff --git a/src/match_clp.c b/src/match_clp.c
index 8039732..36d183a 100644
--- a/src/match_clp.c
+++ b/src/match_clp.c
@@ -21,7 +21,7 @@
 
 struct solvepass
 {
-  int (*solution)();
+  int (*solution) ();
 
   System sys;
   int run;
@@ -384,7 +384,8 @@ sendAdd_clp (const System sys, const int run, const Termlist tl)
 	      /* simple case: no variable inside */
 	      knowledgeAddTerm (sys->know, t);
 	      tl2 = termlistShallow (tl->next);
-	      if (inKnowledge (sys->know, invkey) && hasTermVariable (t->left.op))
+	      if (inKnowledge (sys->know, invkey)
+		  && hasTermVariable (t->left.op))
 		tl2 = termlistAdd (tl2, t->left.op);
 	      sendAdd_clp (sys, run, tl2);
 	      termlistDelete (tl2);
diff --git a/src/modelchecker.c b/src/modelchecker.c
index d37acdd..9e8089f 100644
--- a/src/modelchecker.c
+++ b/src/modelchecker.c
@@ -88,12 +88,12 @@ traverse_chooses_first (const System sys)
       Roledef rd_scan;
 
       rd_scan = runPointerGet (sys, run_scan);
-      if (rd_scan != NULL &&				// Not empty run
+      if (rd_scan != NULL &&	// Not empty run
 	  rd_scan == sys->runs[run_scan].start &&	// First event
-	  rd_scan->type == READ)			// Read
+	  rd_scan->type == READ)	// Read
 	{
 	  if (executeTry (sys, run_scan))
-	      return 1;
+	    return 1;
 	}
     }
   return 0;
@@ -110,9 +110,9 @@ traverse (const System sys)
   if (sys->switchChooseFirst)
     {
       if (traverse_chooses_first (sys))
-	  return 1;
+	return 1;
     }
-  
+
   /* branch for traversal methods */
   switch (sys->traverse)
     {
@@ -203,7 +203,7 @@ executeStep (const System sys, const int run)
   sys->states = statesIncrease (sys->states);
 
   /* what about scenario exploration? */
-  if (sys->switchScenario && sys->step+1 > sys->switchScenarioSize)
+  if (sys->switchScenario && sys->step + 1 > sys->switchScenarioSize)
     {
       /* count states within scenario */
       sys->statesScenario = statesIncrease (sys->statesScenario);
@@ -213,7 +213,8 @@ executeStep (const System sys, const int run)
   if (sys->switchS > 0)
     {
       sys->interval = statesIncrease (sys->interval);
-      if (!statesSmallerThan (sys->interval, (unsigned long int) sys->switchS))
+      if (!statesSmallerThan
+	  (sys->interval, (unsigned long int) sys->switchS))
 	{
 	  globalError++;
 	  sys->interval = STATES0;
@@ -227,7 +228,8 @@ executeStep (const System sys, const int run)
   /* store new node numbder */
   sys->traceNode[sys->step] = sys->states;
   /* the construction below always assumes MAX_GRAPH_STATES to be smaller than the unsigned long it, which seems realistic. */
-  if (sys->output == STATESPACE && statesSmallerThan (sys->states, MAX_GRAPH_STATES))
+  if (sys->output == STATESPACE
+      && statesSmallerThan (sys->states, MAX_GRAPH_STATES))
     {
       /* display graph */
       graphNode (sys);
@@ -240,38 +242,39 @@ executeStep (const System sys, const int run)
  *
  *@todo "What is interesting" relies on the fact that there are only secrecy, sychnr and agreement properties.
  */
-Roledef removeIrrelevant (const System sys, const int run, Roledef rd)
+Roledef
+removeIrrelevant (const System sys, const int run, Roledef rd)
 {
   Roledef rdkill;
   int killclaims;
-  
+
   if (untrustedAgent (sys, sys->runs[run].agents))
-      killclaims = 1;
+    killclaims = 1;
   else
-      killclaims = 0;
+    killclaims = 0;
 
   rdkill = rd;
   while (rd != NULL)
     {
       if (rd->type == SEND || (!killclaims && rd->type == CLAIM))
-	  rdkill = rd;
+	rdkill = rd;
       rd = rd->next;
     }
   /* report part */
   /*
-  rd = rdkill->next;
-  killclaims = 0;
-  while (rd != NULL)
-    {
-      killclaims++;
-      rd = rd->next;
-    }
-  if (killclaims > 1)
-    {
-      warning ("%i events stripped from run %i.", killclaims, run);
-      runPrint (rdkill->next);
-    }
-  */
+     rd = rdkill->next;
+     killclaims = 0;
+     while (rd != NULL)
+     {
+     killclaims++;
+     rd = rd->next;
+     }
+     if (killclaims > 1)
+     {
+     warning ("%i events stripped from run %i.", killclaims, run);
+     runPrint (rdkill->next);
+     }
+   */
 
   /* remove after rdkill */
   return rdkill;
@@ -284,12 +287,13 @@ Roledef removeIrrelevant (const System sys, const int run, Roledef rd)
  *\sa tryChoiceSend()
  */
 void
-unblock_synchronising_labels (const System sys, const int run, const Roledef rd)
+unblock_synchronising_labels (const System sys, const int run,
+			      const Roledef rd)
 {
   if (rd->type != READ || rd->internal)
-      return;
+    return;
   if (!inTermlist (sys->synchronising_labels, rd->label))
-      return;
+    return;
 
   // This read possibly unblocks other sends
   int run_scan;
@@ -298,7 +302,7 @@ unblock_synchronising_labels (const System sys, const int run, const Roledef rd)
     {
       if (run_scan != run)
 	{
-  	  Roledef rd_scan;
+	  Roledef rd_scan;
 
 	  rd_scan = sys->runs[run_scan].index;
 	  if (rd_scan != NULL &&
@@ -357,7 +361,7 @@ explorify (const System sys, const int run)
    * instantiation related determinings.
    * --------------------------------------------
    */
-   
+
   /*
    * Special checks after (implicit) choose events; always first in run reads.
    */
@@ -367,8 +371,8 @@ explorify (const System sys, const int run)
 
       if (inTermlist (sys->untrusted, agentOfRun (sys, run)))
 	{
-          /* this run is executed by an untrusted agent, do not explore */
-          return 0;
+	  /* this run is executed by an untrusted agent, do not explore */
+	  return 0;
 	}
       /* executed by trusted agent */
 
@@ -378,7 +382,7 @@ explorify (const System sys, const int run)
        */
       //!@todo This implementation relies on the fact that there are only secrecy, synchr and agreement properties.
       if (sys->switchNomoreClaims && sys->secrets == NULL)
-	{ /* there are no remaining secrecy claims to be checked */
+	{			/* there are no remaining secrecy claims to be checked */
 	  Roledef rdscan;
 	  int validclaim;
 
@@ -386,11 +390,11 @@ explorify (const System sys, const int run)
 	  validclaim = 0;
 	  /* check for each run */
 	  while (rid < sys->maxruns)
-	    { 
+	    {
 	      /* are claims in this run evaluated anyway? */
 	      if (!untrustedAgent (sys, sys->runs[rid].agents))
-		{ /* possibly claims to be checked in this run */
-		  rdscan = runPointerGet(sys, rid);
+		{		/* possibly claims to be checked in this run */
+		  rdscan = runPointerGet (sys, rid);
 		  while (rdscan != NULL)
 		    {
 		      if (rdscan->type == CLAIM)
@@ -409,7 +413,7 @@ explorify (const System sys, const int run)
 	      rid++;
 	    }
 	  if (validclaim == 0)
-	    { /* no valid claims, abort */
+	    {			/* no valid claims, abort */
 	      return 0;
 	    }
 	}
@@ -435,7 +439,7 @@ explorify (const System sys, const int run)
 	    {
 	      /* dependent run has chosen, so we can compare */
 	      if (termlistOrder (sys->runs[run].agents,
-				   sys->runs[ridSymm].agents) < 0)
+				 sys->runs[ridSymm].agents) < 0)
 		{
 		  /* we only explore the other half */
 		  return 0;
@@ -447,7 +451,7 @@ explorify (const System sys, const int run)
        */
 
       if (sys->switchReduceEndgame)
-       	  roleCap = removeIrrelevant (sys, run, rd);
+	roleCap = removeIrrelevant (sys, run, rd);
 
       /* Special check x: if all agents in each run send only encrypted stuff, and all agents are trusted,
        * there is no way for the intruder to learn anything else than encrypted terms, so secrecy claims will not
@@ -456,15 +460,15 @@ explorify (const System sys, const int run)
       //!@todo For now, there is no check that the runs only send publicly encrypted stuff! Just an assumption to be made true using static analysis.
 
       /*
-      rid = 0;
-      while (rid < sys->maxruns)
-	{
-	  if (!untrustedAgent (sys, sys->runs[rid].agents))
-	    {
-	    }
-	  rid++;
-	}
-	*/
+         rid = 0;
+         while (rid < sys->maxruns)
+         {
+         if (!untrustedAgent (sys, sys->runs[rid].agents))
+         {
+         }
+         rid++;
+         }
+       */
     }
 
   /* 
@@ -479,13 +483,14 @@ explorify (const System sys, const int run)
 	   * Check if it has progressed enough, and has the same agents.
 	   */
 	  int ridSymm;
-     
+
 	  if (rd->type != READ)
 	    {
 	      error ("firstNonAgentRead is not a read?!");
 	    }
 	  ridSymm = sys->runs[run].prevSymmRun;
-	  if (isTermlistEqual (sys->runs[run].agents, sys->runs[ridSymm].agents))
+	  if (isTermlistEqual
+	      (sys->runs[run].agents, sys->runs[ridSymm].agents))
 	    {
 	      /* same agents, so relevant */
 	      if (myStep > 0 && sys->runs[ridSymm].step < myStep)
@@ -540,7 +545,8 @@ explorify (const System sys, const int run)
 	  ridSymm = sys->runs[run].prevSymmRun;
 	  /* equal runs? */
 
-	  if (isTermlistEqual (sys->runs[run].agents, sys->runs[ridSymm].agents))
+	  if (isTermlistEqual
+	      (sys->runs[run].agents, sys->runs[ridSymm].agents))
 	    {
 	      /* so, we have an identical partner */
 	      /* is our partner there already? */
@@ -567,8 +573,7 @@ explorify (const System sys, const int run)
       if (sys->switchScenarioSize == 0)
 	{
 	  /* only after chooses */
-	  if (myStep == 0 &&
-	      rd->type == READ)
+	  if (myStep == 0 && rd->type == READ)
 	    {
 	      if (run == sys->lastChooseRun)
 		{
@@ -605,10 +610,10 @@ explorify (const System sys, const int run)
 	  /* scenario size is not zero */
 
 	  //!@todo Optimization: if the good scenario is already traversed, other trace prefixes need not be explored any further.
-	  if (sys->step+1 == sys->switchScenarioSize)
+	  if (sys->step + 1 == sys->switchScenarioSize)
 	    {
 	      /* Now, the prefix has been set. Count it */
-    	      if (sys->countScenario < INT_MAX)
+	      if (sys->countScenario < INT_MAX)
 		{
 		  sys->countScenario++;
 		}
@@ -679,7 +684,7 @@ explorify (const System sys, const int run)
     {
       roleCap->next = roleCapPart;
     }
-  return 1;	// The event was indeed enabled (irrespective of traverse!)
+  return 1;			// The event was indeed enabled (irrespective of traverse!)
 }
 
 
@@ -806,7 +811,7 @@ __inline__ int
 tryChoiceRead (const System sys, const int run, const Roledef rd)
 {
   int flag;
-  
+
   flag = 0;
 
   /* the sendsdone check only prevent
@@ -853,9 +858,9 @@ tryChoiceRoledef (const System sys, const int run, const Roledef rd)
 
 #ifdef DEBUG
   if (rd == NULL)
-      error ("tryChoiceRoledef should not be called with a NULL rd pointer");
+    error ("tryChoiceRoledef should not be called with a NULL rd pointer");
 #endif
-  
+
   flag = 0;
   switch (rd->type)
     {
@@ -886,9 +891,9 @@ tryChoiceRun (const System sys, const int run)
 
   rd = runPointerGet (sys, run);
   if (rd != NULL)
-      return tryChoiceRoledef (sys, run, rd);
+    return tryChoiceRoledef (sys, run, rd);
   else
-      return 0;
+    return 0;
 }
 
 //! Yield the last active run in the partial trace, or 0 if there is none.
@@ -905,7 +910,7 @@ lastActiveRun (const System sys)
       /* there was a previous action, start scan from there */
 #ifdef DEBUG
       if (sys->porparam < 100)
-          return sys->traceRun[sys->step - 1] + sys->porparam;
+	return sys->traceRun[sys->step - 1] + sys->porparam;
 #endif
       return sys->traceRun[sys->step - 1];
     }
@@ -915,9 +920,7 @@ lastActiveRun (const System sys)
 __inline__ int
 isChooseRoledef (const System sys, const int run, const Roledef rd)
 {
-  return (rd == sys->runs[run].start &&
-	  rd->type == READ && 
-	  rd->internal);
+  return (rd == sys->runs[run].start && rd->type == READ && rd->internal);
 }
 
 //! Explore possible chooses first
@@ -933,7 +936,7 @@ tryChoosesFirst (const System sys)
     {
       rd = runPointerGet (sys, run);
       if (isChooseRoledef (sys, run, rd))
-	  flag = tryChoiceRoledef (sys, run, rd);
+	flag = tryChoiceRoledef (sys, run, rd);
     }
   return flag;
 }
@@ -980,7 +983,7 @@ __inline__ int
 traversePOR5 (const System sys)
 {
   if (tryChoosesFirst (sys))
-      return 1;
+    return 1;
   return tryEventsOffset (sys, lastActiveRun (sys));
 }
 
@@ -1006,7 +1009,7 @@ __inline__ int
 traversePOR7 (const System sys)
 {
   if (tryChoosesFirst (sys))
-      return 1;
+    return 1;
   tryEventsOffset (sys, 0);
 }
 
@@ -1028,7 +1031,7 @@ traversePOR8 (const System sys)
   for (run = 0; run < sys->maxruns && !flag; run++)
     {
       if (run != last)
-          flag = tryChoiceRun (sys, run);
+	flag = tryChoiceRun (sys, run);
     }
   return flag;
 }
@@ -1043,7 +1046,7 @@ traversePOR8 (const System sys)
 int
 propertyCheck (const System sys)
 {
-  int flag = 1;	// default: properties are true, no attack 
+  int flag = 1;			// default: properties are true, no attack 
 
   /* for now, we only check secrecy */
   if (sys->secrets != NULL)
@@ -1065,13 +1068,13 @@ propertyCheck (const System sys)
 		{
 		  if (sys->traceEvent[i]->type == CLAIM &&
 		      sys->traceEvent[i]->to == CLAIM_Secret)
-	 	    {
-		      Termlist tl = secrecyUnfolding(scan->term, sys->know);
+		    {
+		      Termlist tl = secrecyUnfolding (scan->term, sys->know);
 		      if (tl != NULL)
-		        {
-		          /* This was indeed a violated claim */
+			{
+			  /* This was indeed a violated claim */
 			  claimev = i;
-		        }
+			}
 		    }
 		  i++;
 		}
@@ -1079,17 +1082,18 @@ propertyCheck (const System sys)
 	      if (claimev == -1)
 		{
 		  /* weird, should not occur */
-		  fprintf(stderr, "Violation, but cannot locate claim.\n");
-		  printf("A secrecy claim was supposed to be violated on term ");
-		  termPrint(scan->term);
-		  printf(" but we couldn't find the corresponding claim.\n");
-		  exit(1);
+		  fprintf (stderr, "Violation, but cannot locate claim.\n");
+		  printf
+		    ("A secrecy claim was supposed to be violated on term ");
+		  termPrint (scan->term);
+		  printf (" but we couldn't find the corresponding claim.\n");
+		  exit (1);
 		}
 	      else
 		{
 		  /* fine. so it's violated */
-		  violateClaim(sys, sys->step, claimev, tl);
-		  termlistDelete(tl);
+		  violateClaim (sys, sys->step, claimev, tl);
+		  termlistDelete (tl);
 		  flag = 0;
 		}
 	    }
@@ -1163,15 +1167,14 @@ secrecyUnfolding (Term t, const Knowledge know)
 {
   t = deVar (t);
   if (isTermTuple (t))
-    return termlistConcat (secrecyUnfolding(t->left.op1,know),
-			   secrecyUnfolding(t->right.op2,know)
-			  );
+    return termlistConcat (secrecyUnfolding (t->left.op1, know),
+			   secrecyUnfolding (t->right.op2, know));
   else
     {
-      if (inKnowledge(know, t))
-	  return termlistAdd(NULL, t);
+      if (inKnowledge (know, t))
+	return termlistAdd (NULL, t);
       else
-	  return NULL;
+	return NULL;
     }
 }
 
@@ -1187,28 +1190,30 @@ secrecyUnfolding (Term t, const Knowledge know)
  */
 
 Termlist
-claimViolationDetails (const System sys, const int run, const Roledef rd, const Knowledge know)
+claimViolationDetails (const System sys, const int run, const Roledef rd,
+		       const Knowledge know)
 {
   if (rd->type != CLAIM)
     {
-      fprintf(stderr, "Trying to determine details of something other than a claim!\n");
-      exit(-1);
+      fprintf (stderr,
+	       "Trying to determine details of something other than a claim!\n");
+      exit (-1);
     }
 
   /* cases */
   if (rd->to == CLAIM_Secret)
     {
       /* secrecy claim */
-      
+
       if (untrustedAgent (sys, sys->runs[run].agents))
 	{
 	  /* claim was skipped */
-	  return (Termlist) -1;
+	  return (Termlist) - 1;
 	}
       else
 	{
 	  /* construct violating subterms list */
-          return secrecyUnfolding(rd->message, know);
+	  return secrecyUnfolding (rd->message, know);
 	}
     }
   return NULL;
@@ -1240,8 +1245,8 @@ violateClaim (const System sys, int length, int claimev, Termlist reqt)
   /* Copy the current trace to the buffer, if the new one is shorter than the previous one. */
   if (sys->attack == NULL || length < sys->attack->reallength)
     {
-      tracebufDone(sys->attack);
-      sys->attack = tracebufSet(sys, length, claimev);
+      tracebufDone (sys->attack);
+      sys->attack = tracebufSet (sys, length, claimev);
       attackMinimize (sys, sys->attack);
       sys->shortestattack = sys->attack->reallength;
 
@@ -1257,7 +1262,7 @@ violateClaim (const System sys, int length, int claimev, Termlist reqt)
 	case 2:
 	  sys->maxtracelength = sys->shortestattack - 1;
 	  break;
-	} 
+	}
     }
   return flag;
 }
@@ -1275,7 +1280,7 @@ executeTry (const System sys, int run)
 
   runPoint = runPointerGet (sys, run);
   sys->traceEvent[sys->step] = runPoint;	// store for later usage, problem: variables are substituted later...
-  sys->traceRun[sys->step] = run;		// same
+  sys->traceRun[sys->step] = run;	// same
 
   if (runPoint == NULL)
     {
@@ -1367,7 +1372,7 @@ executeTry (const System sys, int run)
 	      sys->secrets =
 		termlistAdd (termlistShallow (oldsecrets), runPoint->message);
 	      flag = claimSecrecy (sys, runPoint->message);
-              runPoint->claiminfo->count++;
+	      runPoint->claiminfo->count++;
 
 	      /* now check whether the claim failed for further actions */
 	      if (!flag)
@@ -1375,11 +1380,11 @@ executeTry (const System sys, int run)
 		  /* violation */
 		  Termlist tl;
 
-                  runPoint->claiminfo->failed++;
-		  tl = claimViolationDetails(sys,run,runPoint,sys->know);
-		  if (violateClaim (sys,sys->step+1, sys->step, tl ))
-		      flag = explorify (sys, run);
-		  termlistDelete(tl);
+		  runPoint->claiminfo->failed++;
+		  tl = claimViolationDetails (sys, run, runPoint, sys->know);
+		  if (violateClaim (sys, sys->step + 1, sys->step, tl))
+		    flag = explorify (sys, run);
+		  termlistDelete (tl);
 		}
 	      else
 		{
@@ -1396,12 +1401,12 @@ executeTry (const System sys, int run)
 	      /*
 	       * NISYNCH
 	       */
-              flag = check_claim_nisynch (sys, sys->step);
+	      flag = check_claim_nisynch (sys, sys->step);
 	      if (!flag)
 		{
 		  /* violation */
-		  if (violateClaim (sys,sys->step+1, sys->step, NULL ))
-		      flag = explorify (sys, run);
+		  if (violateClaim (sys, sys->step + 1, sys->step, NULL))
+		    flag = explorify (sys, run);
 		}
 	      else
 		{
@@ -1414,12 +1419,12 @@ executeTry (const System sys, int run)
 	      /*
 	       * NIAGREE
 	       */
-              flag = check_claim_niagree (sys, sys->step);
+	      flag = check_claim_niagree (sys, sys->step);
 	      if (!flag)
 		{
 		  /* violation */
-		  if (violateClaim (sys,sys->step+1, sys->step, NULL ))
-		      flag = explorify (sys, run);
+		  if (violateClaim (sys, sys->step + 1, sys->step, NULL))
+		    flag = explorify (sys, run);
 		}
 	      else
 		{
@@ -1433,4 +1438,3 @@ executeTry (const System sys, int run)
     }
   return flag;
 }
-
diff --git a/src/modelchecker.h b/src/modelchecker.h
index 77e0f16..d2fb81d 100644
--- a/src/modelchecker.h
+++ b/src/modelchecker.h
@@ -4,4 +4,4 @@ int explorify (const System sys, const int run);
 int executeStep (const System sys, const int run);
 int propertyCheck (const System sys);
 Termlist claimViolationDetails (const System sys, const int run, const Roledef
-		rd, const Knowledge know);
+				rd, const Knowledge know);
diff --git a/src/output.c b/src/output.c
index 9dc95bb..0a0954d 100644
--- a/src/output.c
+++ b/src/output.c
@@ -497,7 +497,8 @@ attackDisplay (const System sys)
  *-------------------------------------------
  */
 
-void graphInit (const System sys)
+void
+graphInit (const System sys)
 {
   Termlist tl;
 
@@ -524,7 +525,8 @@ void graphInit (const System sys)
   printf ("\tconcentrate=true;\n");
 
   /* node/edge defaults */
-  printf ("\tnode [shape=\"point\",fontsize=\"4\",fontname=\"Helvetica\"];\n");
+  printf
+    ("\tnode [shape=\"point\",fontsize=\"4\",fontname=\"Helvetica\"];\n");
   printf ("\tedge [fontsize=\"4\",fontname=\"Helvetica\"];\n");
 
   /* start with initial node 0 */
@@ -537,13 +539,15 @@ void graphInit (const System sys)
   printf ("\"];\n");
 }
 
-void graphDone (const System sys)
+void
+graphDone (const System sys)
 {
   /* drawing state space. close up. */
   printf ("}\n");
 }
 
-void graphNode (const System sys)
+void
+graphNode (const System sys)
 {
   Termlist newtl;
   states_t thisNode, parentNode;
@@ -562,8 +566,8 @@ void graphNode (const System sys)
   printf ("\tn");
   statesFormat (thisNode);
   printf (" [");
-  
-  newtl = knowledgeNew (sys->traceKnow[index], sys->traceKnow[index+1]);
+
+  newtl = knowledgeNew (sys->traceKnow[index], sys->traceKnow[index + 1]);
   if (newtl != NULL)
     {
       /* knowledge added */
@@ -578,17 +582,17 @@ void graphNode (const System sys)
       if (sys->switchScenario != 0 &&
 	  rd != NULL &&
 	  rd == sys->runs[run].start &&
-	  rd->type == READ &&
-	  run == sys->lastChooseRun)
+	  rd->type == READ && run == sys->lastChooseRun)
 	{
 	  /* last choose; scenario selected */
-	  printf ("shape=box,height=0.2,label=\"Scenario %i: ", sys->countScenario);
+	  printf ("shape=box,height=0.2,label=\"Scenario %i: ",
+		  sys->countScenario);
 	  scenarioPrint (sys);
 	  printf ("\"");
 	}
       else
 	{
-      	  printf ("label=\"\"");
+	  printf ("label=\"\"");
 	}
     }
   printf ("];\n");
@@ -602,7 +606,7 @@ void graphNode (const System sys)
   printf (" [label=\"");
 
   // Print step 
-  printf ("%i:",sys->runs[run].step-1);
+  printf ("%i:", sys->runs[run].step - 1);
 
   if (rd->type == CLAIM && untrustedAgent (sys, sys->runs[run].agents))
     {
@@ -615,7 +619,7 @@ void graphNode (const System sys)
       printf ("#%i\"", run);
       if (rd->type == CLAIM)
 	{
-          printf (",shape=house,color=green");
+	  printf (",shape=house,color=green");
 	}
     }
   /* a choose? */
@@ -628,7 +632,8 @@ void graphNode (const System sys)
   printf (";\n");
 }
 
-void graphNodePath (const System sys, const int length, const char* nodepar)
+void
+graphNodePath (const System sys, const int length, const char *nodepar)
 {
   int i;
   states_t thisNode;
@@ -647,7 +652,8 @@ void graphNodePath (const System sys, const int length, const char* nodepar)
     }
 }
 
-void graphEdgePath (const System sys, const int length, const char* edgepar)
+void
+graphEdgePath (const System sys, const int length, const char *edgepar)
 {
   int i;
   states_t thisNode, prevNode;
@@ -657,7 +663,7 @@ void graphEdgePath (const System sys, const int length, const char* edgepar)
   while (i < length)
     {
       /* determine node number */
-      thisNode = sys->traceNode[i+1];
+      thisNode = sys->traceNode[i + 1];
 
       /* color edge */
       printf ("\tn");
@@ -670,10 +676,11 @@ void graphEdgePath (const System sys, const int length, const char* edgepar)
     }
 }
 
-void graphPath (const System sys, int length)
+void
+graphPath (const System sys, int length)
 {
-  graphNodePath (sys,length,"style=bold,color=red");
-  graphEdgePath (sys,length-1,"style=bold,color=red");
+  graphNodePath (sys, length, "style=bold,color=red");
+  graphEdgePath (sys, length - 1, "style=bold,color=red");
 }
 
 //! Scenario for graph; bit of a hack
@@ -682,17 +689,14 @@ graphScenario (const System sys, const int run, const Roledef rd)
 {
   /* Add scenario node */
   printf ("\ts%i [shape=box,height=0.2,label=\"Scenario %i: ",
-	  sys->countScenario,
-	  sys->countScenario);
+	  sys->countScenario, sys->countScenario);
   scenarioPrint (sys);
   printf ("\"];\n");
 
   /* draw edge */
-  printf ("\tn%i -> s%i",
-	  sys->traceNode[sys->step],
-	  sys->countScenario);
+  printf ("\tn%i -> s%i", sys->traceNode[sys->step], sys->countScenario);
   printf (" [color=blue,label=\"");
-  printf ("%i:",sys->runs[run].step);
+  printf ("%i:", sys->runs[run].step);
   roledefPrint (rd);
   printf ("#%i", run);
   printf ("\"];\n");
diff --git a/src/output.h b/src/output.h
index 72a3d7e..7864492 100644
--- a/src/output.h
+++ b/src/output.h
@@ -3,15 +3,13 @@
 
 #include "system.h"
 
-void tracePrint(const System sys);
-void attackDisplay(const System sys);
+void tracePrint (const System sys);
+void attackDisplay (const System sys);
 void graphInit (const System sys);
 void graphDone (const System sys);
 void graphNode (const System sys);
-void graphNodePath (const System sys, const int length, const char*
-		nodepar);
-void graphEdgePath (const System sys, const int length, const char*
-		edgepar);
+void graphNodePath (const System sys, const int length, const char *nodepar);
+void graphEdgePath (const System sys, const int length, const char *edgepar);
 void graphPath (const System sys, int length);
 void graphScenario (const System sys, const int run, const Roledef rd);
 
diff --git a/src/report.c b/src/report.c
index d0cf969..de701d8 100644
--- a/src/report.c
+++ b/src/report.c
@@ -39,7 +39,7 @@ reportMid (const System sys)
   indent ();
   printf ("Trace length %i.\n", 1 + sys->step);
   if (globalLatex)
-      printf("\n");
+    printf ("\n");
   tracePrint (sys);
 }
 
@@ -69,7 +69,7 @@ reportSecrecy (const System sys, Term t)
   termPrint (t);
   printf ("$\n");
   if (globalLatex)
-      printf("\n");
+    printf ("\n");
   reportMid (sys);
   reportEnd (sys);
 }
diff --git a/src/role.c b/src/role.c
index 6f60604..2e3e5e9 100644
--- a/src/role.c
+++ b/src/role.c
@@ -93,7 +93,7 @@ roledefDuplicate1 (const Roledef rd)
   newrd->next = NULL;
   return newrd;
 }
-    
+
 //! Duplicate a role event list.
 /**
  *\sa roledefDelete()
@@ -166,7 +166,8 @@ roledefInit (int type, Term label, Term from, Term to, Term msg, Claimlist cl)
  *\sa roledefInit()
  */
 Roledef
-roledefAdd (Roledef rd, int type, Term label, Term from, Term to, Term msg, Claimlist cl)
+roledefAdd (Roledef rd, int type, Term label, Term from, Term to, Term msg,
+	    Claimlist cl)
 {
   Roledef scan;
 
@@ -235,5 +236,3 @@ rolesPrint (Role r)
 	}
     }
 }
-
-
diff --git a/src/role.h b/src/role.h
index 5244c25..1c579de 100644
--- a/src/role.h
+++ b/src/role.h
@@ -8,7 +8,8 @@
 #include "constraint.h"
 #include "states.h"
 
-enum eventtype { READ, SEND, CLAIM };
+enum eventtype
+{ READ, SEND, CLAIM };
 
 //! The container for the claim info list
 struct claimlist
@@ -23,8 +24,8 @@ struct claimlist
   states_t count;
   //! Number of occurrences that failed.
   states_t failed;
-  int r;	//!< role number for mapping
-  int ev;	//!< event index in role
+  int r;			//!< role number for mapping
+  int ev;			//!< event index in role
   //! Preceding label list
   Termlist prec;
   //! Next node pointer or NULL for the last element of the function.
@@ -110,11 +111,12 @@ Roledef roledefDuplicate1 (const Roledef rd);
 Roledef roledefDuplicate (Roledef rd);
 void roledefDelete (Roledef rd);
 void roledefDestroy (Roledef rd);
-Roledef roledefInit (int type, Term label, Term from, Term to, Term msg, Claimlist cl);
-Roledef roledefAdd (Roledef rd, int type, Term label, Term from, Term to, Term msg, Claimlist cl);
+Roledef roledefInit (int type, Term label, Term from, Term to, Term msg,
+		     Claimlist cl);
+Roledef roledefAdd (Roledef rd, int type, Term label, Term from, Term to,
+		    Term msg, Claimlist cl);
 Role roleCreate (Term nameterm);
 void rolePrint (Role r);
 void rolesPrint (Role r);
 
 #endif
-
diff --git a/src/states.c b/src/states.c
index a5400d9..aaa2219 100644
--- a/src/states.c
+++ b/src/states.c
@@ -8,7 +8,7 @@
 __inline__ states_t
 statesIncrease (const states_t states)
 {
-  return states+1;
+  return states + 1;
 }
 
 __inline__ double
@@ -21,9 +21,9 @@ __inline__ int
 statesSmallerThan (const states_t states, unsigned long int reflint)
 {
   if (states < (states_t) reflint)
-      return 1;
+    return 1;
   else
-      return 0;
+    return 0;
 }
 
 //! Sensible output for number of states/claims
@@ -34,7 +34,7 @@ __inline__ void
 statesFormat (const states_t states)
 {
   if (states < 1000000)
-      eprintf ("%lu", states);
+    eprintf ("%lu", states);
   else
-      eprintf ("%.3e", statesDouble (states));
+    eprintf ("%.3e", statesDouble (states));
 }
diff --git a/src/states.h b/src/states.h
index 1e79cd1..062054f 100644
--- a/src/states.h
+++ b/src/states.h
@@ -14,7 +14,8 @@ typedef unsigned long int states_t;
 
 __inline__ states_t statesIncrease (const states_t states);
 __inline__ double statesDouble (const states_t states);
-__inline__ int statesSmallerThan (const states_t states, unsigned long int reflint);
+__inline__ int statesSmallerThan (const states_t states,
+				  unsigned long int reflint);
 __inline__ void statesFormat (const states_t states);
 
 #endif
diff --git a/src/symbol.c b/src/symbol.c
index 98a18cb..7abd442 100644
--- a/src/symbol.c
+++ b/src/symbol.c
@@ -212,14 +212,14 @@ symbolSysConst (const char *str)
  *\sa globalError
  */
 void
-eprintf (char *fmt, ... )
+eprintf (char *fmt, ...)
 {
   va_list args;
 
   va_start (args, fmt);
   if (globalError == 0)
-  	vfprintf (stdout, fmt, args);
+    vfprintf (stdout, fmt, args);
   else
-  	vfprintf (stderr, fmt, args);
+    vfprintf (stderr, fmt, args);
   va_end (args);
 }
diff --git a/src/symbol.h b/src/symbol.h
index 88bb505..cbcb090 100644
--- a/src/symbol.h
+++ b/src/symbol.h
@@ -6,7 +6,8 @@
  */
 #define HASHSIZE 997
 
-enum symboltypes { T_UNDEF = -1, T_PROTOCOL, T_CONST, T_VAR, T_SYSCONST };
+enum symboltypes
+{ T_UNDEF = -1, T_PROTOCOL, T_CONST, T_VAR, T_SYSCONST };
 
 #define EOS 0
 
@@ -41,7 +42,7 @@ void symbolPrint (const Symbol s);
 void symbolPrintAll (void);
 Symbol symbolSysConst (const char *str);
 
-void eprintf (char *fmt, ... );
+void eprintf (char *fmt, ...);
 
 extern int globalError;
 
diff --git a/src/system.c b/src/system.c
index 92c5622..4a2078c 100644
--- a/src/system.c
+++ b/src/system.c
@@ -51,7 +51,7 @@ systemInit ()
   /* initially, no trace ofcourse */
   sys->step = 0;
   sys->shortestattack = INT_MAX;
-  sys->attack = tracebufInit();
+  sys->attack = tracebufInit ();
 
   /* switches */
   sys->output = ATTACK;		// default is to show the attacks
@@ -113,7 +113,7 @@ systemReset (const System sys)
   /* some initial counters */
   sys->states = statesIncrease (STATES0);	//!< Initial state is not explored, so start counting at 1
   sys->statesScenario = STATES0;
-  sys->interval = sys->states;			//!< To keep in line with the states
+  sys->interval = sys->states;	//!< To keep in line with the states
   sys->claims = STATES0;
   sys->failed = STATES0;
   sys->countScenario = 0;
@@ -125,7 +125,7 @@ systemReset (const System sys)
       cl->failed = STATES0;
       cl = cl->next;
     }
-  
+
   sys->knowPhase = 0;		// knowledge transition id
 
   termlistDestroy (sys->secrets);	// remove old secrets list
@@ -157,9 +157,7 @@ systemRuns (const System sys)
       Roledef rd;
 
       rd = runPointerGet (sys, run);
-      if (rd != NULL &&
-	  rd->internal &&
-	  rd->type == READ)
+      if (rd != NULL && rd->internal && rd->type == READ)
 	{
 	  /* increasing run traversal, so this yields max */
 	  sys->lastChooseRun = run;
@@ -168,7 +166,7 @@ systemRuns (const System sys)
 #ifdef DEBUG
   if (sys->switchScenario < 0)
     {
-      warning ("Last run with a choose: %i",sys->lastChooseRun);
+      warning ("Last run with a choose: %i", sys->lastChooseRun);
     }
 #endif
 }
@@ -217,7 +215,7 @@ statesPrint (const System sys)
   statesFormat (sys->states);
   eprintf (" states traversed.\n");
   if (globalLatex)
-      eprintf("\n");
+    eprintf ("\n");
 }
 
 //! Destroy a system memory block and system::runs
@@ -318,13 +316,13 @@ Term
 agentOfRunRole (const System sys, const int run, const Term role)
 {
   Termlist roles = sys->runs[run].protocol->rolenames;
-  Termlist agents= sys->runs[run].agents;
+  Termlist agents = sys->runs[run].agents;
 
   /* TODO stupid reversed order, lose that soon */
-  agents = termlistForward(agents);
+  agents = termlistForward (agents);
   while (agents != NULL && roles != NULL)
     {
-      if (isTermEqual(roles->term, role))
+      if (isTermEqual (roles->term, role))
 	{
 	  return agents->term;
 	}
@@ -342,7 +340,7 @@ agentOfRunRole (const System sys, const int run, const Term role)
 Term
 agentOfRun (const System sys, const int run)
 {
-  return agentOfRunRole(sys,run,sys->runs[run].role->nameterm);
+  return agentOfRunRole (sys, run, sys->runs[run].role->nameterm);
 }
 
 /**
@@ -353,31 +351,32 @@ agentOfRun (const System sys, const int run)
  *
  * Return -1 if there is no such symmetry.
  */
-int staticRunSymmetry (const System sys,const int rid)
+int
+staticRunSymmetry (const System sys, const int rid)
 {
-  int ridSymm;		// previous symmetrical run
-  Termlist agents;	// list of agents for rid
-  Run runs;		// shortcut usage
+  int ridSymm;			// previous symmetrical run
+  Termlist agents;		// list of agents for rid
+  Run runs;			// shortcut usage
 
   ridSymm = -1;
   runs = sys->runs;
   agents = runs[rid].agents;
   while (agents != NULL)
     {
-      if (isTermVariable(agents->term))
-          ridSymm = rid - 1;
+      if (isTermVariable (agents->term))
+	ridSymm = rid - 1;
       agents = agents->next;
     }
   /* there is no variable in this roledef, abort */
   if (ridSymm == -1)
-      return -1;
+    return -1;
 
   agents = runs[rid].agents;
   while (ridSymm >= 0)
     {
       /* compare protocol name, role name */
       if (runs[ridSymm].protocol == runs[rid].protocol &&
-	  runs[ridSymm].role     == runs[rid].role)
+	  runs[ridSymm].role == runs[rid].role)
 	{
 	  /* same stuff */
 	  int isEqual;
@@ -394,8 +393,9 @@ int staticRunSymmetry (const System sys,const int rid)
 		  /* case 1: variable, should match type */
 		  if (isTermVariable (alSymm->term))
 		    {
-		      if (!isTermlistEqual (al->term->stype, alSymm->term->stype))
-			  isEqual = 0;
+		      if (!isTermlistEqual
+			  (al->term->stype, alSymm->term->stype))
+			isEqual = 0;
 		    }
 		  else
 		    {
@@ -406,7 +406,7 @@ int staticRunSymmetry (const System sys,const int rid)
 		{
 		  /* case 2: constant, should match */
 		  if (!isTermEqual (al->term, alSymm->term))
-		      isEqual = 0;
+		    isEqual = 0;
 		}
 	      alSymm = alSymm->next;
 	      al = al->next;
@@ -415,21 +415,23 @@ int staticRunSymmetry (const System sys,const int rid)
 	    {
 	      /* this candidate is allright */
 #ifdef DEBUG
-  	      warning ("Symmetry detection. #%i can depend on #%i.",rid,ridSymm);
+	      warning ("Symmetry detection. #%i can depend on #%i.", rid,
+		       ridSymm);
 #endif
 	      return ridSymm;
 	    }
 	}
       ridSymm--;
     }
-  return -1;	// signal that no symmetrical run was found
+  return -1;			// signal that no symmetrical run was found
 }
 
 //! Determine first read with variables besides agents
 /**
  *@todo For now, we assume it is simply the first read after the choose, if there is one.
  */
-int firstNonAgentRead (const System sys, int rid)
+int
+firstNonAgentRead (const System sys, int rid)
 {
   int step;
   Roledef rd;
@@ -446,10 +448,12 @@ int firstNonAgentRead (const System sys, int rid)
       rd = rd->next;
       step++;
     }
-  if (rd != NULL && !rd->internal && rd->type == READ)		// assumes lazy LR eval
+  if (rd != NULL && !rd->internal && rd->type == READ)	// assumes lazy LR eval
     {
 #ifdef DEBUG
-      warning ("First read %i with dependency on symmetrical found in run %i.", step, rid);
+      warning
+	("First read %i with dependency on symmetrical found in run %i.",
+	 step, rid);
 #endif
       return step;
     }
@@ -505,7 +509,9 @@ roleInstance (const System sys, const Protocol protocol, const Role role,
 	  /* newvar is apparently new, but it might occur
 	   * in the first event if it's a read, in which
 	   * case we forget it */
-	  if (sys->switchForceChoose || !(rd->type == READ && termOccurs (rd->message, scanfrom->term)))
+	  if (sys->switchForceChoose
+	      || !(rd->type == READ
+		   && termOccurs (rd->message, scanfrom->term)))
 	    {
 	      /* this term is forced as a choose, or it does not occur in the (first) read event */
 	      /* TODO scan might be more complex, but
@@ -561,7 +567,7 @@ roleInstance (const System sys, const Protocol protocol, const Role role,
 	      Term newt = makeTermType (t->type, t->left.symb, rid);
 	      if (realTermVariable (newt))
 		{
-	          sys->variables = termlistAdd (sys->variables, newt);
+		  sys->variables = termlistAdd (sys->variables, newt);
 		}
 	      newt->stype = t->stype;
 	      fromlist = termlistAdd (fromlist, t);
@@ -590,7 +596,7 @@ roleInstance (const System sys, const Protocol protocol, const Role role,
   runs[rid].locals = tolist;
 
   /* Determine symmetric run */
-  runs[rid].prevSymmRun = staticRunSymmetry (sys, rid);		// symmetry reduction static analysis
+  runs[rid].prevSymmRun = staticRunSymmetry (sys, rid);	// symmetry reduction static analysis
 
   /* Determine first read with variables besides agents */
   runs[rid].firstNonAgentRead = firstNonAgentRead (sys, rid);	// symmetry reduction type II
@@ -809,18 +815,18 @@ agentsOfRunPrint (const System sys, const int run)
   Term role = sys->runs[run].role->nameterm;
   Termlist roles = sys->runs[run].protocol->rolenames;
 
-  termPrint(role);
-  printf("(");
+  termPrint (role);
+  printf ("(");
   while (roles != NULL)
     {
-      termPrint(agentOfRunRole(sys,run,roles->term));
+      termPrint (agentOfRunRole (sys, run, roles->term));
       roles = roles->next;
       if (roles != NULL)
 	{
-	  printf(",");
+	  printf (",");
 	}
     }
-  printf(")");
+  printf (")");
 }
 
 //! Explain a violated claim at point i in the trace.
@@ -828,7 +834,7 @@ agentsOfRunPrint (const System sys, const int run)
 void
 violatedClaimPrint (const System sys, const int i)
 {
-  printf("Claim stuk");
+  printf ("Claim stuk");
 }
 
 //! Yield the real length of an attack.
@@ -837,30 +843,31 @@ violatedClaimPrint (const System sys, const int i)
  * the redundant events but also the choose events.
  */
 
-int attackLength(struct tracebuf* tb)
+int
+attackLength (struct tracebuf *tb)
 {
-    int len,i;
+  int len, i;
 
-    len = 0;
-    i = 0;
-    while (i < tb->length)
+  len = 0;
+  i = 0;
+  while (i < tb->length)
     {
-        if (tb->status[i] != S_RED)
+      if (tb->status[i] != S_RED)
 	{
-	    /* apparently not redundant */
-	    if (!(tb->event[i]->type == READ && tb->event[i]->internal))
+	  /* apparently not redundant */
+	  if (!(tb->event[i]->type == READ && tb->event[i]->internal))
 	    {
-	        /* and no internal read, so it counts */
-	        len++;
+	      /* and no internal read, so it counts */
+	      len++;
 	    }
 	}
-	i++;
+      i++;
     }
-    return len;
+  return len;
 }
 
 void
-commandlinePrint (FILE *stream, const System sys)
+commandlinePrint (FILE * stream, const System sys)
 {
   /* print command line */
   int i;
@@ -870,7 +877,8 @@ commandlinePrint (FILE *stream, const System sys)
 }
 
 //! Get the number of roles in the system.
-int compute_rolecount (const System sys)
+int
+compute_rolecount (const System sys)
 {
   Protocol pr;
   int n;
@@ -879,14 +887,15 @@ int compute_rolecount (const System sys)
   pr = sys->protocols;
   while (pr != NULL)
     {
-      n = n + termlistLength(pr->rolenames);
+      n = n + termlistLength (pr->rolenames);
       pr = pr->next;
     }
   return n;
 }
 
 //! Compute the maximum number of events in a single role in the system.
-int compute_roleeventmax (const System sys)
+int
+compute_roleeventmax (const System sys)
 {
   Protocol pr;
   int maxev;
@@ -910,7 +919,8 @@ int compute_roleeventmax (const System sys)
 	      n++;
 	      rd = rd->next;
 	    }
-	  if (n > maxev) maxev = n;
+	  if (n > maxev)
+	    maxev = n;
 	  r = r->next;
 	}
       pr = pr->next;
@@ -937,7 +947,7 @@ scenarioPrint (const System sys)
       runInstancePrint (sys, run);
       if (run < sys->maxruns - 1)
 	{
-          printf ("\t");
+	  printf ("\t");
 	}
     }
 }
diff --git a/src/system.h b/src/system.h
index 95827a4..97a3935 100644
--- a/src/system.h
+++ b/src/system.h
@@ -12,7 +12,8 @@
 #define runPointerGet(sys,run)		sys->runs[run].index
 #define runPointerSet(sys,run,newp)	sys->runs[run].index = newp
 
-enum outputs { EMPTY, ATTACK, STATESPACE, SCENARIOS, SUMMARY };
+enum outputs
+{ EMPTY, ATTACK, STATESPACE, SCENARIOS, SUMMARY };
 
 //! Protocol definition.
 struct protocol
@@ -35,17 +36,17 @@ typedef struct protocol *Protocol;
 //! Run container.
 struct run
 {
-  Protocol protocol;	//!< Protocol of this run.
-  Role role;		//!< Role of this run.
-  Termlist agents; 	//!< Agents involved in this run.
-  int step;		//!< Current execution point in the run (integer)
-  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.
-  int prevSymmRun;	//!< Used for symmetry reduction. Either -1, or the previous run with the same role def and at least a single parameter.
-  int firstNonAgentRead; //!< Used for symmetry reductions for equal agents runs; -1 if there is no candidate.
-  int firstReal;	//!< 1 if a choose was inserted, otherwise 0
+  Protocol protocol;		//!< Protocol of this run.
+  Role role;			//!< Role of this run.
+  Termlist agents;		//!< Agents involved in this run.
+  int step;			//!< Current execution point in the run (integer)
+  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.
+  int prevSymmRun;		//!< Used for symmetry reduction. Either -1, or the previous run with the same role def and at least a single parameter.
+  int firstNonAgentRead;	//!< Used for symmetry reductions for equal agents runs; -1 if there is no candidate.
+  int firstReal;		//!< 1 if a choose was inserted, otherwise 0
 };
 
 //! Shorthand for run pointer.
@@ -55,11 +56,11 @@ typedef struct run *Run;
 struct varbuf
 {
   //! List of closed variables.
-  Termlist	from;
+  Termlist from;
   //! List of terms to which the closed variables are bound.
-  Termlist	to;
+  Termlist to;
   //! List of open variables.
-  Termlist	empty;
+  Termlist empty;
 };
 
 //! Shorthand for varbuf pointer.
@@ -69,28 +70,28 @@ typedef struct varbuf *Varbuf;
 struct tracebuf
 {
   //! Length of trace.
-  int		length;
+  int length;
   //! Length of trace minus the redundant events.
-  int		reallength;
+  int reallength;
   //! Array of events.
-  Roledef	*event;
+  Roledef *event;
   //! Array of run identifiers for each event.
-  int		*run;
+  int *run;
   //! Array of status flags for each event.
   /**
    *\sa S_OKE, S_RED, S_TOD, S_UNK
    */
-  int		*status;
+  int *status;
   //! Array for matching sends to reads.
-  int		*link;
+  int *link;
   //! Index of violated claim in trace.
-  int		violatedclaim;	
+  int violatedclaim;
   //! Array of knowledge sets for each event.
-  Knowledge	*know;
+  Knowledge *know;
   //! List of terms required to be in the final knowledge.
-  Termlist	requiredterms;
+  Termlist requiredterms;
   //! List of variables in the system.
-  Varbuf	variables;
+  Varbuf variables;
 };
 
 //! The main state structure.
@@ -107,7 +108,7 @@ struct system
 
   /* properties */
   Termlist secrets;		//!< Integrate secrets list into system.
-  Termlist synchronising_labels; //!< List of labels that might synchronise.
+  Termlist synchronising_labels;	//!< List of labels that might synchronise.
   int shortestattack;		//!< Length of shortest attack trace.
 
   /* switches */
@@ -137,7 +138,7 @@ struct system
    * Obsolete. Use globalLatex instead.
    *\sa globalLatex
    */
-  int latex;			
+  int latex;
 
   /* traversal */
   int traverse;			//!< Traversal method.
@@ -180,7 +181,7 @@ struct system
   Constraintlist constraints;	//!< Only needed for CLP match
 
   //! Shortest attack storage.
-  struct tracebuf* attack;
+  struct tracebuf *attack;
 
   //! Command line arguments
   int argc;
@@ -217,8 +218,8 @@ int untrustedAgent (const System sys, Termlist agents);
 int getMaxTraceLength (const System sys);
 void agentsOfRunPrint (const System sys, const int run);
 void violatedClaimPrint (const System sys, int i);
-int attackLength(struct tracebuf* tb);
-void commandlinePrint (FILE *stream, const System sys);
+int attackLength (struct tracebuf *tb);
+void commandlinePrint (FILE * stream, const System sys);
 
 int compute_rolecount (const System sys);
 int compute_roleeventmax (const System sys);
diff --git a/src/tac.h b/src/tac.h
index d9f3a36..7a7ca07 100644
--- a/src/tac.h
+++ b/src/tac.h
@@ -7,7 +7,8 @@
  * TAC instructions
  */
 
-enum tactypes {
+enum tactypes
+{
   TAC_UNDEF,
   TAC_SYM,
   TAC_TUPLE,
@@ -43,7 +44,7 @@ struct tacnode
     struct tacnode *tac;
     char *str;
   } t1;
-  union 
+  union
   {
     Symbol sym;
     struct tacnode *tac;
diff --git a/src/term.c b/src/term.c
index 5c0da7b..32b1e24 100644
--- a/src/term.c
+++ b/src/term.c
@@ -159,22 +159,25 @@ hasTermVariable (Term term)
   else
     {
       if (realTermTuple (term))
-	return (hasTermVariable (term->left.op1) || hasTermVariable (term->right.op2));
+	return (hasTermVariable (term->left.op1)
+		|| hasTermVariable (term->right.op2));
       else
-	return (hasTermVariable (term->left.op) || hasTermVariable (term->right.key));
+	return (hasTermVariable (term->left.op)
+		|| hasTermVariable (term->right.key));
     }
 }
 
 //! Safe wrapper for isTermEqual
 
-int isTermEqualDebug (Term t1, Term t2)
+int
+isTermEqualDebug (Term t1, Term t2)
 {
   int test1, test2;
 
   t1 = deVar (t1);
   t2 = deVar (t2);
 
-  test1 = isTermEqualFn (t1,t2);
+  test1 = isTermEqualFn (t1, t2);
   if (!(realTermLeaf (t1) && realTermLeaf (t2)))
     {
       return test1;
@@ -218,7 +221,8 @@ isTermEqualFn (Term term1, Term term2)
 #ifdef DEBUG
       int test;
 
-      test = (term1->left.symb == term2->left.symb && term1->right.runid == term2->right.runid);
+      test = (term1->left.symb == term2->left.symb
+	      && term1->right.runid == term2->right.runid);
       if (test)
 	{
 	  error ("Strange node equality detected, should not occur.");
@@ -267,7 +271,8 @@ termOccurs (Term t, Term tsub)
   if (realTermLeaf (t))
     return 0;
   if (realTermTuple (t))
-    return (termOccurs (t->left.op1, tsub) || termOccurs (t->right.op2, tsub));
+    return (termOccurs (t->left.op1, tsub)
+	    || termOccurs (t->right.op2, tsub));
   else
     return (termOccurs (t->left.op, tsub) || termOccurs (t->right.key, tsub));
 }
@@ -319,7 +324,7 @@ termPrint (Term term)
   if (realTermTuple (term))
     {
       eprintf ("(");
-      termTuplePrint(term);
+      termTuplePrint (term);
       eprintf (")");
       return;
     }
@@ -370,15 +375,15 @@ termTuplePrint (Term term)
       eprintf ("Empty term");
       return;
     }
-  term = deVar(term);
+  term = deVar (term);
   while (realTermTuple (term))
     {
       // To remove any brackets, change this into termTuplePrint.
       termPrint (term->left.op1);
       eprintf (",");
-      term = deVar(term->right.op2);
+      term = deVar (term->right.op2);
     }
-  termPrint(term);
+  termPrint (term);
   return;
 }
 
@@ -709,27 +714,27 @@ tupleProject (Term tt, int n)
  */
 
 int
-termSize(Term t)
+termSize (Term t)
 {
   if (t == NULL)
     {
       return 0;
     }
 
-  t = deVar(t);
-  if (realTermLeaf(t))
+  t = deVar (t);
+  if (realTermLeaf (t))
     {
       return 1;
     }
   else
     {
-      if (realTermEncrypt(t))
+      if (realTermEncrypt (t))
 	{
-	  return 1 + termSize(t->left.op) + termSize(t->right.key);
+	  return 1 + termSize (t->left.op) + termSize (t->right.key);
 	}
       else
 	{
-	  return termSize(t->left.op1) + termSize(t->right.op2);
+	  return termSize (t->left.op1) + termSize (t->right.op2);
 	}
     }
 }
@@ -741,20 +746,20 @@ termSize(Term t)
  */
 
 float
-termDistance(Term t1, Term t2)
+termDistance (Term t1, Term t2)
 {
   int t1s;
   int t2s;
 
   /* First the special cases: no equal subterms, completely equal */
-  if (isTermEqual(t1,t2))
-      return 1;
+  if (isTermEqual (t1, t2))
+    return 1;
 
-  t1 = deVar(t1);
-  t2 = deVar(t2);
+  t1 = deVar (t1);
+  t2 = deVar (t2);
 
-  t1s = termSize(t1);
-  t2s = termSize(t2);
+  t1s = termSize (t1);
+  t2s = termSize (t2);
 
   if (t1 == NULL || t2 == NULL)
     {
@@ -763,11 +768,11 @@ termDistance(Term t1, Term t2)
   if (t1->type != t2->type)
     {
       /* unequal type, maybe one is a subterm of the other? */
-      if (t1s > t2s && termOccurs(t1,t2))
+      if (t1s > t2s && termOccurs (t1, t2))
 	{
 	  return (float) t2s / t1s;
 	}
-      if (t2s > t1s && termOccurs(t2,t1))
+      if (t2s > t1s && termOccurs (t2, t1))
 	{
 	  return (float) t1s / t2s;
 	}
@@ -776,7 +781,7 @@ termDistance(Term t1, Term t2)
   else
     {
       /* equal types */
-      if (isTermLeaf(t1))
+      if (isTermLeaf (t1))
 	{
 	  /* we had established before that they are not equal */
 	  return 0;
@@ -784,14 +789,16 @@ termDistance(Term t1, Term t2)
       else
 	{
 	  /* non-leaf recurse */
-	  if (isTermEncrypt(t1))
+	  if (isTermEncrypt (t1))
 	    {
 	      /* encryption */
-	      return (termDistance(t1->left.op, t2->left.op) + termDistance(t1->right.key, t2->right.key)) / 2;
+	      return (termDistance (t1->left.op, t2->left.op) +
+		      termDistance (t1->right.key, t2->right.key)) / 2;
 	    }
 	  else
 	    {
-	      return (termDistance(t1->left.op1, t2->left.op1) + termDistance(t1->right.op2, t2->right.op2)) / 2;
+	      return (termDistance (t1->left.op1, t2->left.op1) +
+		      termDistance (t1->right.op2, t2->right.op2)) / 2;
 	    }
 	}
     }
@@ -801,14 +808,15 @@ termDistance(Term t1, Term t2)
  * Enforce a (arbitrary) ordering on terms
  * <0 means a<b, 0 means a=b, >0 means a>b.
  */
-int termOrder (Term t1, Term t2)
+int
+termOrder (Term t1, Term t2)
 {
-  char* name1;
-  char* name2;
+  char *name1;
+  char *name2;
 
   t1 = deVar (t1);
   t2 = deVar (t2);
-  if (isTermEqual (t1,t2))
+  if (isTermEqual (t1, t2))
     {
       /* equal terms */
       return 0;
@@ -819,9 +827,9 @@ int termOrder (Term t1, Term t2)
     {
       /* different types, so ordering on types first */
       if (t1->type < t2->type)
-	  return -1;
+	return -1;
       else
-	  return 1;
+	return 1;
     }
 
   /* same type
@@ -832,9 +840,7 @@ int termOrder (Term t1, Term t2)
       /* compare names */
       int comp;
 
-      comp = strcmp (t1->left.symb->text,
-      		     t2->left.symb->text
-		     );
+      comp = strcmp (t1->left.symb->text, t2->left.symb->text);
       if (comp != 0)
 	{
 	  /* names differ */
@@ -845,35 +851,36 @@ int termOrder (Term t1, Term t2)
 	  /* equal names, compare run identifiers */
 	  if (t1->right.runid == t2->right.runid)
 	    {
-	      error ("termOrder: two terms seem to be identical although local precondition says they aren't.");
+	      error
+		("termOrder: two terms seem to be identical although local precondition says they aren't.");
 	    }
 	  else
 	    {
 	      if (t1->right.runid < t2->right.runid)
-		  return -1;
+		return -1;
 	      else
-		  return 1;
+		return 1;
 	    }
 	}
     }
   else
     {
       /* non-leaf */
-      int compL,compR;
+      int compL, compR;
 
       if (isTermEncrypt (t1))
 	{
-	  compL = termOrder (t1->left.op,   t2->left.op);
+	  compL = termOrder (t1->left.op, t2->left.op);
 	  compR = termOrder (t1->right.key, t2->right.key);
 	}
       else
 	{
-	  compL = termOrder (t1->left.op1,  t2->left.op1);
+	  compL = termOrder (t1->left.op1, t2->left.op1);
 	  compR = termOrder (t1->right.op2, t2->right.op2);
 	}
       if (compL != 0)
-	  return compL;
+	return compL;
       else
-	  return compR;
+	return compR;
     }
 }
diff --git a/src/term.h b/src/term.h
index 8cd64d6..ef367f3 100644
--- a/src/term.h
+++ b/src/term.h
@@ -4,7 +4,8 @@
 #include "symbol.h"
 
 // type <= LEAF means it's a leaf, nkay?
-enum termtypes { GLOBAL, VARIABLE, LEAF, ENCRYPT, TUPLE };
+enum termtypes
+{ GLOBAL, VARIABLE, LEAF, ENCRYPT, TUPLE };
 
 //! The most basic datatype in the modelchecker.
 /**
@@ -25,7 +26,7 @@ struct term
   int type;
   //! Data Type termlist (e.g. agent or nonce)
   /** Only for leaves. */
-  void *stype;			
+  void *stype;
   //! Substitution term.
   /**
    * If this is non-NULL, this leaf term is apparently substituted by
@@ -33,7 +34,7 @@ struct term
    */
   struct term *subst;		// only for variable/leaf, substitution term
 
-  union 
+  union
   {
     Symbol symb;
     //! Encrypted subterm.
@@ -160,8 +161,8 @@ void termNormalize (Term term);
 Term termRunid (Term term, int runid);
 int tupleCount (Term tt);
 Term tupleProject (Term tt, int n);
-int termSize(Term t);
-float termDistance(Term t1, Term t2);
+int termSize (Term t);
+float termDistance (Term t1, Term t2);
 int termOrder (Term t1, Term t2);
 
 #endif
diff --git a/src/termlist.c b/src/termlist.c
index 8500891..1a71286 100644
--- a/src/termlist.c
+++ b/src/termlist.c
@@ -223,9 +223,9 @@ Termlist
 termlistAddNew (const Termlist tl, const Term t)
 {
   if (inTermlist (tl, t))
-      return tl;
+    return tl;
   else
-      return termlistAdd (tl, t);
+    return termlistAdd (tl, t);
 }
 
 //! Concatenates two termlists.
@@ -361,7 +361,7 @@ termlistPrint (Termlist tl)
       termPrint (tl->term);
       tl = tl->next;
       if (tl != NULL)
-	  eprintf(", ");
+	eprintf (", ");
     }
   eprintf ("]");
 }
@@ -394,10 +394,11 @@ termlistAddVariables (Termlist tl, Term t)
 				     t->right.key);
       else
 	return
-	  termlistAddVariables (termlistAddVariables (tl, t->left.op1), t->right.op2);
+	  termlistAddVariables (termlistAddVariables (tl, t->left.op1),
+				t->right.op2);
     }
 }
-    
+
 //! Append all variables in a term to a list.
 /**
  *@param tl The list to which to append to.
@@ -417,12 +418,12 @@ termlistAddRealVariables (Termlist tl, Term t)
 	{
 	  Term tbuf = t->subst;
 	  t->subst = NULL;
-	  if (!inTermlist (tl,t))
+	  if (!inTermlist (tl, t))
 	    {
-	      tl = termlistAdd (tl,t);
+	      tl = termlistAdd (tl, t);
 	    }
 	  t->subst = tbuf;
-	  return termlistAddRealVariables (tl,t->subst);
+	  return termlistAddRealVariables (tl, t->subst);
 	}
       else
 	{
@@ -436,7 +437,8 @@ termlistAddRealVariables (Termlist tl, Term t)
 				     t->right.key);
       else
 	return
-	  termlistAddVariables (termlistAddVariables (tl, t->left.op1), t->right.op2);
+	  termlistAddVariables (termlistAddVariables (tl, t->left.op1),
+				t->right.op2);
     }
 }
 
@@ -455,9 +457,11 @@ termlistAddBasic (Termlist tl, Term t)
   if (!isTermLeaf (t))
     {
       if (isTermEncrypt (t))
-	return termlistAddBasic (termlistAddBasic (tl, t->left.op), t->right.key);
+	return termlistAddBasic (termlistAddBasic (tl, t->left.op),
+				 t->right.key);
       else
-	return termlistAddBasic (termlistAddBasic (tl, t->left.op1), t->right.op2);
+	return termlistAddBasic (termlistAddBasic (tl, t->left.op1),
+				 t->right.op2);
     }
   else
     {
@@ -622,13 +626,17 @@ termLocal (const Term t, Termlist fromlist, Termlist tolist,
       Term newt = termDuplicate (t);
       if (realTermTuple (t))
 	{
-	  newt->left.op1 = termLocal (t->left.op1, fromlist, tolist, locals, runid);
-	  newt->right.op2 = termLocal (t->right.op2, fromlist, tolist, locals, runid);
+	  newt->left.op1 =
+	    termLocal (t->left.op1, fromlist, tolist, locals, runid);
+	  newt->right.op2 =
+	    termLocal (t->right.op2, fromlist, tolist, locals, runid);
 	}
       else
 	{
-	  newt->left.op = termLocal (t->left.op, fromlist, tolist, locals, runid);
-	  newt->right.key = termLocal (t->right.key, fromlist, tolist, locals, runid);
+	  newt->left.op =
+	    termLocal (t->left.op, fromlist, tolist, locals, runid);
+	  newt->right.key =
+	    termLocal (t->right.key, fromlist, tolist, locals, runid);
 	}
       return newt;
     }
@@ -755,7 +763,8 @@ termlistForward (Termlist tl)
 /**
  * Compare two termlists containing only basic terms, and yield ordering.
  */
-int termlistOrder (Termlist tl1, Termlist tl2)
+int
+termlistOrder (Termlist tl1, Termlist tl2)
 {
   int order;
 
@@ -767,13 +776,11 @@ int termlistOrder (Termlist tl1, Termlist tl2)
       tl2 = tl2->next;
     }
   if (order != 0)
-      return order;
-  if (tl1 == NULL && tl2 == NULL) 
-      return order;
+    return order;
+  if (tl1 == NULL && tl2 == NULL)
+    return order;
   if (tl1 == NULL)
-      return -1;
+    return -1;
   else
-      return 1;
+    return 1;
 }
-
-
diff --git a/src/termmap.c b/src/termmap.c
index 5f9ca4e..d5ca93e 100644
--- a/src/termmap.c
+++ b/src/termmap.c
@@ -39,7 +39,7 @@ termmapGet (Termmap f, const Term x)
   while (f != NULL)
     {
       if (isTermEqual (x, f->term))
-	  return f->result;
+	return f->result;
       f = f->next;
     }
   return -1;
@@ -62,8 +62,8 @@ termmapSet (const Termmap f, const Term x, const int y)
 	{
 	  //! Is the result correct already?
 	  if (fscan->result != y)
-	      fscan->result = y;
-          return f;
+	    fscan->result = y;
+	  return f;
 	}
       fscan = fscan->next;
     }
@@ -107,7 +107,8 @@ termmapDelete (const Termmap f)
 }
 
 //! Print a function
-void termmapPrint (Termmap f)
+void
+termmapPrint (Termmap f)
 {
   if (f != NULL)
     {
diff --git a/src/tracebuf.c b/src/tracebuf.c
index eb4b217..f3ad697 100644
--- a/src/tracebuf.c
+++ b/src/tracebuf.c
@@ -16,7 +16,7 @@
  */
 
 int
-tracebufRebuildKnow(struct tracebuf *tb)
+tracebufRebuildKnow (struct tracebuf *tb)
 {
   Knowledge k;
   Roledef rd;
@@ -31,7 +31,7 @@ tracebufRebuildKnow(struct tracebuf *tb)
     }
 
   flag = -1;
-  k = knowledgeDuplicate(tb->know[0]);
+  k = knowledgeDuplicate (tb->know[0]);
   i = 0;
   while (i < tb->length)
     {
@@ -60,8 +60,8 @@ tracebufRebuildKnow(struct tracebuf *tb)
 	    }
 	}
       /* write the new knowledge, overwriting old stuff */
-      knowledgeDelete (tb->know[i+1]);
-      tb->know[i+1] = knowledgeDuplicate (k);
+      knowledgeDelete (tb->know[i + 1]);
+      tb->know[i + 1] = knowledgeDuplicate (k);
 
       i++;
     }
@@ -69,12 +69,12 @@ tracebufRebuildKnow(struct tracebuf *tb)
   while (tl != NULL)
     {
       if (!inKnowledge (k, tl->term))
-        {
-          flag = tb->length;
-        }
+	{
+	  flag = tb->length;
+	}
       tl = tl->next;
     }
-  knowledgeDelete(k);
+  knowledgeDelete (k);
   return flag;
 }
 
@@ -84,10 +84,11 @@ tracebufRebuildKnow(struct tracebuf *tb)
  * initializes the trace buffer.
  */
 
-struct tracebuf*
+struct tracebuf *
 tracebufInit (void)
 {
-  struct tracebuf *tb = (struct tracebuf *) memAlloc(sizeof(struct tracebuf));
+  struct tracebuf *tb =
+    (struct tracebuf *) memAlloc (sizeof (struct tracebuf));
   tb->length = 0;
   tb->reallength = 0;
   tb->event = NULL;
@@ -118,28 +119,28 @@ tracebufDone (struct tracebuf *tb)
 
       i = 0;
       /* note: knowledge domain is length+1 */
-      knowledgeDelete(tb->know[0]);
+      knowledgeDelete (tb->know[0]);
       while (i < tb->length)
 	{
-      	  rd = tb->event[i];
+	  rd = tb->event[i];
 	  termDelete (rd->from);
 	  termDelete (rd->to);
 	  termDelete (rd->message);
-          roledefDelete(rd);
-	  knowledgeDelete(tb->know[i+1]);
+	  roledefDelete (rd);
+	  knowledgeDelete (tb->know[i + 1]);
 	  i++;
 	}
 
-      memFree(tb->know, (i+1) * sizeof (struct knowledge*));
-      memFree(tb->event, i * sizeof (struct roledef*));
-      memFree(tb->run, i * sizeof(int));
-      memFree(tb->status, i * sizeof(int));
-      memFree(tb->link, i * sizeof(int));
+      memFree (tb->know, (i + 1) * sizeof (struct knowledge *));
+      memFree (tb->event, i * sizeof (struct roledef *));
+      memFree (tb->run, i * sizeof (int));
+      memFree (tb->status, i * sizeof (int));
+      memFree (tb->link, i * sizeof (int));
     }
-  memFree(tb, sizeof(tracebuf));
+  memFree (tb, sizeof (tracebuf));
 }
 
-struct tracebuf*
+struct tracebuf *
 tracebufSet (const System sys, int length, int claimev)
 {
   struct tracebuf *tb;
@@ -150,7 +151,7 @@ tracebufSet (const System sys, int length, int claimev)
    * any constant from the constraint for a variable.
    */
 
-  tb = tracebufInit();
+  tb = tracebufInit ();
   if (length == 0)
     {
       return tb;
@@ -158,11 +159,12 @@ tracebufSet (const System sys, int length, int claimev)
   tb->length = length;
   tb->reallength = length;
   tb->variables = (Varbuf) varbufInit (sys);
-  tb->event = (Roledef *) memAlloc(length * sizeof(struct roledef*));
-  tb->status = (int *) memAlloc(length * sizeof(int));
-  tb->link = (int *) memAlloc(length * sizeof(int));
-  tb->run = (int *) memAlloc(length * sizeof(int));
-  tb->know = (Knowledge *) memAlloc((length + 1) * sizeof (struct knowledge*));
+  tb->event = (Roledef *) memAlloc (length * sizeof (struct roledef *));
+  tb->status = (int *) memAlloc (length * sizeof (int));
+  tb->link = (int *) memAlloc (length * sizeof (int));
+  tb->run = (int *) memAlloc (length * sizeof (int));
+  tb->know =
+    (Knowledge *) memAlloc ((length + 1) * sizeof (struct knowledge *));
 
   /* when duplicating the knowledge, we want to instantiate the variables as well
    */
@@ -175,20 +177,20 @@ tracebufSet (const System sys, int length, int claimev)
       rd = roledefDuplicate1 (sys->traceEvent[i]);
       if (rd == NULL)
 	{
-	  printf("Empty event in trace at %i of %i?\n",i,length);
-	  exit(1);
+	  printf ("Empty event in trace at %i of %i?\n", i, length);
+	  exit (1);
 	}
 
-      /* make a copy without variables */ 
-      rd->to      = termDuplicateUV (rd->to);
-      rd->from    = termDuplicateUV (rd->from);
+      /* make a copy without variables */
+      rd->to = termDuplicateUV (rd->to);
+      rd->from = termDuplicateUV (rd->from);
       rd->message = termDuplicateUV (rd->message);
 
       tb->event[i] = rd;
       tb->link[i] = -1;
       tb->status[i] = S_UNK;
       tb->run[i] = sys->traceRun[i];
-      tb->know[i+1] = NULL;
+      tb->know[i + 1] = NULL;
       i++;
     }
 
diff --git a/src/tracebuf.h b/src/tracebuf.h
index f7aa71e..a057076 100644
--- a/src/tracebuf.h
+++ b/src/tracebuf.h
@@ -7,11 +7,12 @@
 #include "system.h"
 
 /* STATUS symbols */
-enum statussymbols {
-  S_UNK,	// UNKnown   : unprocessed.
-  S_OKE,	// OKE       : done, but required for the attack.
-  S_RED,	// REDundant : is not needed for attack, we're sure.
-  S_TOD 	// TODo      : The previous suggestion REQ was too similar to RED. This is reserved for reads.
+enum statussymbols
+{
+  S_UNK,			// UNKnown   : unprocessed.
+  S_OKE,			// OKE       : done, but required for the attack.
+  S_RED,			// REDundant : is not needed for attack, we're sure.
+  S_TOD				// TODo      : The previous suggestion REQ was too similar to RED. This is reserved for reads.
 };
 
 
@@ -19,10 +20,10 @@ enum statussymbols {
  * tracebuf struct is defined in system.h to avoid loops.
  */
 
-int tracebufRebuildKnow(struct tracebuf *tb);
-struct tracebuf* tracebufInit (void);
+int tracebufRebuildKnow (struct tracebuf *tb);
+struct tracebuf *tracebufInit (void);
 void tracebufDone (struct tracebuf *tb);
-struct tracebuf* tracebufSet (const System sys, int length, int claimev);
+struct tracebuf *tracebufSet (const System sys, int length, int claimev);
 
 
 #endif
diff --git a/src/varbuf.c b/src/varbuf.c
index c6f5f20..ee8fa0c 100644
--- a/src/varbuf.c
+++ b/src/varbuf.c
@@ -18,15 +18,15 @@ varbufInit (const System sys)
   Varbuf vb;
   Termlist tl;
   Term termfrom, termto;
-  
-  vb = (Varbuf) memAlloc(sizeof(struct varbuf));
+
+  vb = (Varbuf) memAlloc (sizeof (struct varbuf));
   vb->from = NULL;
   vb->to = NULL;
   vb->empty = NULL;
   tl = sys->variables;
   while (tl != NULL)
     {
-      if (realTermVariable(tl->term))
+      if (realTermVariable (tl->term))
 	{
 	  /* this is actually a variable */
 	  if (tl->term->subst == NULL)
@@ -87,8 +87,6 @@ varbufDone (Varbuf vb)
       termlistDelete (vb->from);
       termlistDelete (vb->to);
       termlistDelete (vb->empty);
-      memFree(vb, sizeof(struct varbuf));
+      memFree (vb, sizeof (struct varbuf));
     }
 }
-
-