From 4832e9116c622ab0161df08bb731d9986d69e7ff Mon Sep 17 00:00:00 2001
From: ccremers <ccremers@4f7d145f-a0d4-0310-ae10-d96cc04433c1>
Date: Mon, 30 Aug 2004 21:07:45 +0000
Subject: [PATCH] - Added pruning theorem for untrusted actors.

---
 src/arachne.c | 22 +++++++++++++++++++++-
 1 file changed, 21 insertions(+), 1 deletion(-)

diff --git a/src/arachne.c b/src/arachne.c
index d6c616b..3a7b663 100644
--- a/src/arachne.c
+++ b/src/arachne.c
@@ -1461,7 +1461,7 @@ prune_theorems ()
   Termlist tl;
   List bl;
 
-  // Check if all agents are valid
+  // Check if all agents of the main run are valid
   tl = sys->runs[0].agents;
   while (tl != NULL)
     {
@@ -1499,6 +1499,26 @@ prune_theorems ()
       tl = tl->next;
     }
 
+  // Check if the actors of all other runs are not untrusted
+  if (sys->untrusted != NULL)
+    {
+      int run;
+
+      run = 1;
+      while (run < sys->maxruns)
+	{
+	  if (inTermlist (sys->untrusted, agentOfRun (sys, run)))
+	    {
+	      if (sys->output == PROOF)
+		{
+		  indentPrint ();
+		  eprintf ("Pruned because the actor of run %i is untrusted.\n", run);
+		}
+	    }
+	  run++;
+	}
+    }
+
   // Check for c-minimality
   if (!bindings_c_minimal ())
     {