From 1c81b04aa28af417f5e88444d7400590b0ea80ab Mon Sep 17 00:00:00 2001
From: Cas Cremers <cas.cremers@gmail.com>
Date: Sun, 21 Oct 2018 18:52:20 +0200
Subject: [PATCH] Removed another simple trampoline.

---
 src/prune_theorems.c | 115 ++++++++++++++++++++++---------------------
 1 file changed, 58 insertions(+), 57 deletions(-)

diff --git a/src/prune_theorems.c b/src/prune_theorems.c
index f85372d..546f45d 100644
--- a/src/prune_theorems.c
+++ b/src/prune_theorems.c
@@ -49,68 +49,69 @@ extern int max_encryption_level;
 int
 correctLocalOrder (const System sys)
 {
-  int flag;
+  int r1;
 
-  int checkRun (int r1)
+  int checkTerm (Term t)
   {
-    int checkTerm (Term t)
-    {
-      if (!isTermVariable (t))
-	{
-	  int r2;
-	  int e1, e2;
+    if (!isTermVariable (t))
+      {
+	int r2;
+	int e1, e2;
 
-	  // t is a term from r2 that occurs in r1
-	  r2 = TermRunid (t);
-	  e1 = firstOccurrence (sys, r1, t, ANYEVENT);
-	  if (e1 >= 0)
-	    {
-	      if (roledef_shift (sys->runs[r1].start, e1)->type == RECV)
-		{
-		  e2 = firstOccurrence (sys, r2, t, SEND);
-		  if (e2 >= 0)
-		    {
-		      // thus, it should not be the case that e1 occurs before e2
-		      if (isDependEvent (r1, e1, r2, e2))
-			{
-			  // That's not good!
-			  if (switches.output == PROOF)
-			    {
-			      indentPrint ();
-			      eprintf ("Pruned because ordering for term ");
-			      termSubstPrint (t);
-			      eprintf
-				(" cannot be correct: the first send r%ii%i occurs after the receive r%ii%i.\n",
-				 r2, e2, r1, e1);
-			    }
-			  flag = false;
-			  return false;
-			}
-		    }
-		}
-	    }
-	  else
-	    {
-	      globalError++;
-	      eprintf ("error: term ");
-	      termSubstPrint (t);
-	      eprintf
-		(" from run %i should occur in run %i, but it doesn't.\n", r2,
-		 r1);
-	      globalError--;
-	      error ("Abort");
-	    }
-	}
-      return true;
-    }
-
-    return iterateLocalToOther (sys, r1, checkTerm);
+	// t is a term from r2 that occurs in r1
+	r2 = TermRunid (t);
+	e1 = firstOccurrence (sys, r1, t, ANYEVENT);
+	if (e1 >= 0)
+	  {
+	    if (roledef_shift (sys->runs[r1].start, e1)->type == RECV)
+	      {
+		e2 = firstOccurrence (sys, r2, t, SEND);
+		if (e2 >= 0)
+		  {
+		    // thus, it should not be the case that e1 occurs before e2
+		    if (isDependEvent (r1, e1, r2, e2))
+		      {
+			// That's not good!
+			if (switches.output == PROOF)
+			  {
+			    indentPrint ();
+			    eprintf ("Pruned because ordering for term ");
+			    termSubstPrint (t);
+			    eprintf
+			      (" cannot be correct: the first send r%ii%i occurs after the receive r%ii%i.\n",
+			       r2, e2, r1, e1);
+			  }
+			return false;
+		      }
+		  }
+	      }
+	  }
+	else
+	  {
+	    globalError++;
+	    eprintf ("error: term ");
+	    termSubstPrint (t);
+	    eprintf
+	      (" from run %i should occur in run %i, but it doesn't.\n", r2,
+	       r1);
+	    globalError--;
+	    error ("Abort");
+	  }
+      }
+    return true;
   }
 
-  flag = true;
-  iterateRegularRuns (sys, checkRun);
-
-  return flag;
+  for (r1 = 0; r1 < sys->maxruns; r1++)
+    {
+      if (sys->runs[r1].protocol != INTRUDER)
+	{
+	  if (!iterateLocalToOther (sys, r1, checkTerm))
+	    {
+	      return false;
+	    }
+	}
+    }
+  return true;
 }
 
 //! Check all runs